a-cforma.adb, [...] (=): Generic parameter removed to allow the use of regular…

a-cforma.adb, [...] (=): Generic parameter removed to allow the use of regular equality over elements in...

2017-04-27  Claire Dross  <dross@adacore.com>

	* a-cforma.adb, a-cforma.ads (=): Generic parameter removed to
	allow the use of regular equality over elements in contracts.
	(Formal_Model): Ghost package containing model functions that
	are used in subprogram contracts.
	(Current_To_Last): Removed, model functions should be used instead.
	(First_To_Previous): Removed, model functions should be used instead.
	(Strict_Equal): Removed, model functions should be used instead.
	(No_Overlap): Removed, model functions should be used instead.
	* a-cofuma.adb, a-cofuma.ads (Enable_Handling_Of_Equivalence)
	Boolean generic parameter to disable contracts for equivalence
	between keys.
	(Witness): Create a witness of a key that is used for handling of
	equivalence between keys.
	(Has_Witness): Check whether a witness is contained in a map.
	(W_Get): Get the element associated to a witness.
	(Lift_Equivalent_Keys): Removed, equivalence between keys is handled
	directly.
	* a-cofuse.adb, a-cofuse.ads (Enable_Handling_Of_Equivalence)
	Boolean generic parameter to disable contracts for equivalence
	between keys.
	* a-cfhama.adb, a-cfhama.ads (Formal_Model.P) Disable handling
	of equivalence on functional maps.
	* a-cfdlli.adb, a-cfdlli.ads (Formal_Model.P) Disable handling
	of equivalence on functional maps.

From-SVN: r247328

gcc/ada/ChangeLog

+2017-04-27  Claire Dross  <dross@adacore.com>
+
+	* a-cforma.adb, a-cforma.ads (=): Generic parameter removed to
+	allow the use of regular equality over elements in contracts.
+	(Formal_Model): Ghost package containing model functions that
+	are used in subprogram contracts.
+	(Current_To_Last): Removed, model functions should be used instead.
+	(First_To_Previous): Removed, model functions should be used instead.
+	(Strict_Equal): Removed, model functions should be used instead.
+	(No_Overlap): Removed, model functions should be used instead.
+	* a-cofuma.adb, a-cofuma.ads (Enable_Handling_Of_Equivalence)
+	Boolean generic parameter to disable contracts for equivalence
+	between keys.
+	(Witness): Create a witness of a key that is used for handling of
+	equivalence between keys.
+	(Has_Witness): Check whether a witness is contained in a map.
+	(W_Get): Get the element associated to a witness.
+	(Lift_Equivalent_Keys): Removed, equivalence between keys is handled
+	directly.
+	* a-cofuse.adb, a-cofuse.ads (Enable_Handling_Of_Equivalence)
+	Boolean generic parameter to disable contracts for equivalence
+	between keys.
+	* a-cfhama.adb, a-cfhama.ads (Formal_Model.P) Disable handling
+	of equivalence on functional maps.
+	* a-cfdlli.adb, a-cfdlli.ads (Formal_Model.P) Disable handling
+	of equivalence on functional maps.
+
 2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch9.adb (Expand_Entry_Barrier): Code

gcc/ada/a-cfdlli.ads

@@ -153,7 +153,8 @@ is
       package P is new Ada.Containers.Functional_Maps
         (Key_Type                       => Cursor,
          Element_Type                   => Positive_Count_Type,
-         Equivalent_Keys => "=");
+         Equivalent_Keys                => "=",
+         Enable_Handling_Of_Equivalence => False);
 
       function "="
         (Left  : P.Map;

gcc/ada/a-cfhama.ads

@@ -68,7 +68,7 @@ is
                   Next        => Next,
                   Has_Element => Has_Element,
                   Element     => Key),
-     Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0;
+     Default_Initial_Condition => Is_Empty (Map);
    pragma Preelaborable_Initialization (Map);
 
    Empty_Map : constant Map;
@@ -120,7 +120,8 @@ is
       package P is new Ada.Containers.Functional_Maps
         (Key_Type                       => Cursor,
          Element_Type                   => Positive_Count_Type,
-         Equivalent_Keys => "=");
+         Equivalent_Keys                => "=",
+         Enable_Handling_Of_Equivalence => False);
 
       function "="
         (Left  : P.Map;
@@ -262,7 +263,7 @@ is
 
    function Is_Empty (Container : Map) return Boolean with
      Global => null,
-     Post   => Is_Empty'Result = M.Is_Empty (Model (Container));
+     Post   => Is_Empty'Result = (Length (Container) = 0);
 
    procedure Clear (Container : in out Map) with
      Global => null,
@@ -503,6 +504,12 @@ is
                    Model (Container)'Old,
                    Key)
 
+            --  Key is inserted in Container
+
+            and K.Get (Keys (Container),
+                       P.Get (Positions (Container), Find (Container, Key))) =
+                Key
+
             --  Mapping from cursors to keys is preserved
 
             and Mapping_Preserved

gcc/ada/a-cofuma.adb

@@ -148,6 +148,13 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       return Find (Container.Keys, Key) > 0;
    end Has_Key;
 
+   -----------------
+   -- Has_Witness --
+   -----------------
+
+   function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
+   is (Witness in 1 .. Length (Container.Keys));
+
    --------------
    -- Is_Empty --
    --------------
@@ -233,16 +240,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       return Length (Container.Elements);
    end Length;
 
-   --------------------------
-   -- Lift_Equivalent_Keys --
-   --------------------------
-
-   procedure Lift_Equivalent_Keys
-     (Container : Map;
-      Left      : Key_Type;
-      Right     : Key_Type)
-   is null;
-
    ---------------
    -- Same_Keys --
    ---------------
@@ -264,4 +261,19 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
       Elements =>
         Set (Container.Elements, Find (Container.Keys, Key), New_Item));
 
+   -----------
+   -- W_Get --
+   -----------
+
+   function W_Get (Container : Map; Witness : Count_Type) return Element_Type
+   is
+     (Get (Container.Elements, Witness));
+
+   -------------
+   -- Witness --
+   -------------
+
+   function Witness (Container : Map; Key : Key_Type) return Count_Type is
+     (Find (Container.Keys, Key));
+
 end Ada.Containers.Functional_Maps;

gcc/ada/a-cofuma.ads

@@ -36,6 +36,10 @@ generic
    type Key_Type (<>) is private;
    type Element_Type (<>)  is private;
    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+   Enable_Handling_Of_Equivalence : Boolean := True;
+   --  This constant should only be set to False when no particular handling
+   --  of equivalence over keys is needed, that is, Equivalent_Keys defines a
+   --  key uniquely.
 
 package Ada.Containers.Functional_Maps with SPARK_Mode is
 
@@ -57,38 +61,40 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
    -----------------------
 
    --  Maps are axiomatized using Has_Key and Get, encoding respectively the
-   --  presence of a key in a map and an accessor to elements associated to its
-   --  keys. The length of a map is also added to protect Add against overflows
-   --  but it is not actually modeled.
+   --  presence of a key in a map and an accessor to elements associated with
+   --  its keys. The length of a map is also added to protect Add against
+   --  overflows but it is not actually modeled.
 
    function Has_Key (Container : Map; Key : Key_Type) return Boolean with
-     Global => null;
    --  Return True if Key is present in Container
 
-   function Get (Container : Map; Key : Key_Type) return Element_Type with
      Global => null,
-     Pre    => Has_Key (Container, Key);
-   --  Return the element associated to Key is present in Container
+     Post   =>
+       (if Enable_Handling_Of_Equivalence then
 
-   function Length (Container : Map) return Count_Type with
-     Global => null;
-   --  Return the number of mappings in Container
+          --  Has_Key returns the same result on all equivalent keys
 
-   procedure Lift_Equivalent_Keys
-     (Container : Map;
-      Left      : Key_Type;
-      Right     : Key_Type)
-   --  Lemma function which can be called manually to allow GNATprove to deduce
-   --  that Has_Key and Get always return the same result on equivalent keys.
+          (if (for some K of Container => Equivalent_Keys (K, Key)) then
+             Has_Key'Result));
+
+   function Get (Container : Map; Key : Key_Type) return Element_Type with
+   --  Return the element associated with Key in Container
 
-   with
-     Ghost,
      Global => null,
-     Pre    => Equivalent_Keys (Left, Right),
+     Pre    => Has_Key (Container, Key),
      Post   =>
-       Has_Key (Container, Left) = Has_Key (Container, Right)
-         and (if Has_Key (Container, Left) then
-                 Get (Container, Left) = Get (Container, Right));
+       (if Enable_Handling_Of_Equivalence then
+
+          --  Get returns the same result on all equivalent keys
+
+          Get'Result = W_Get (Container, Witness (Container, Key))
+          and (for all K of Container =>
+                 (if Equivalent_Keys (K, Key) then
+                    Witness (Container, Key) = Witness (Container, K))));
+
+   function Length (Container : Map) return Count_Type with
+     Global => null;
+   --  Return the number of mappings in Container
 
    ------------------------
    -- Property Functions --
@@ -236,8 +242,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
      (Container : Map;
       Key       : Key_Type;
       New_Item  : Element_Type) return Map
-   --  Returns Container, where the element associated to Key has been replaced
-   --  by New_Item.
+   --  Returns Container, where the element associated with Key has been
+   --  replaced by New_Item.
 
    with
      Global => null,
@@ -248,6 +254,35 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
          and Same_Keys (Container, Set'Result)
          and Elements_Equal_Except (Container, Set'Result, Key);
 
+   ------------------------------
+   --  Handling of Equivalence --
+   ------------------------------
+
+   --  These functions are used to specify that Get returns the same value on
+   --  equivalent keys. They should not be used directly in user code.
+
+   function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
+   with
+     Ghost,
+     Global => null;
+   --  Returns True if there is a key with witness Witness in Container
+
+   function Witness (Container : Map; Key : Key_Type) return Count_Type with
+   --  Returns the witness of Key in Container
+
+     Ghost,
+     Global => null,
+     Pre    => Has_Key (Container, Key),
+     Post   => Has_Witness (Container, Witness'Result);
+
+   function W_Get (Container : Map; Witness : Count_Type) return Element_Type
+   with
+   --  Returns the element associated with a witness in Container
+
+     Ghost,
+     Global => null,
+     Pre    => Has_Witness (Container, Witness);
+
    ---------------------------
    --  Iteration Primitives --
    ---------------------------

gcc/ada/a-cofuse.ads

@@ -37,6 +37,10 @@ generic
    with function Equivalent_Elements
      (Left  : Element_Type;
       Right : Element_Type) return Boolean;
+   Enable_Handling_Of_Equivalence : Boolean := True;
+   --  This constant should only be set to False when no particular handling
+   --  of equivalence over elements is needed, that is, Equivalent_Elements
+   --  defines an element uniquely.
 
 package Ada.Containers.Functional_Sets with SPARK_Mode is
 
@@ -49,6 +53,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
    --  Sets are empty when default initialized.
    --  "For in" quantification over sets should not be used.
    --  "For of" quantification over sets iterates over elements.
+   --  Note that, for proof, "for of" quantification is understood modulo
+   --  equivalence (quantification includes elements equivalent to elements of
+   --  the map).
 
    -----------------------
    --  Basic operations --
@@ -59,9 +66,17 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
    --  against overflows but it is not actually modeled.
 
    function Contains (Container : Set; Item : Element_Type) return Boolean with
-     Global => null;
    --  Return True if Item is contained in Container
 
+     Global => null,
+     Post   =>
+       (if Enable_Handling_Of_Equivalence then
+
+          --  Contains returns the same result on all equivalent elements
+
+          (if (for some E of Container => Equivalent_Elements (E, Item)) then
+             Contains'Result));
+
    function Length (Container : Set) return Count_Type with
      Global => null;
    --  Return the number of elements in Container