+2017-04-27 Eric Botcazou <ebotcazou@adacore.com>
+
+ * fe.h (Warn_On_Questionable_Layout): Declare.
+ * warnsw.ads (Warn_On_Record_Holes): Move down.
+ (Warn_On_Questionable_Layout): New boolean variable.
+ (Warning_Record): Add Warn_On_Questionable_Layout field.
+ * warnsw.adb (All_Warnings): Set Warn_On_Questionable_Layout.
+ (Restore_Warnings): Likewise.
+ (Save_Warnings): Likewise.
+ (Set_Dot_Warning_Switch): Handle 'q' and 'Q' letters.
+ * gcc-interface/decl.c (gnat_to_gnu_entity): Adjust call to
+ components_to_record.
+ (gnu_field_to_gnat): New function.
+ (warn_on_field_placement): Likewise.
+ (components_to_record): Add GNAT_RECORD_TYPE and remove REORDER
+ parameters. Rename local variables and adjust recursive call.
+ Rework final scan of the field list and implement warnings on the
+ problematic placement of specific sorts of fields.
+
+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * errout.adb, exp_aggr.adb, exp_attr.adb, exp_code.adb, fname.adb,
+ * fname.ads, freeze.adb, inline.adb, lib.adb, lib.ads, lib-list.adb,
+ * lib-load.adb, lib-writ.adb, par.adb, restrict.adb, rtsfind.adb,
+ * sem.adb, sem_cat.adb, sem_ch10.adb, sem_ch12.adb, sem_ch3.adb,
+ * sem_ch4.adb, sem_ch6.adb, sem_ch8.adb, sem_ch9.adb, sem_elab.adb,
+ * sem_intr.adb, sem_res.adb, sem_util.adb, sem_warn.adb, sprint.adb:
+ For efficiency, cache results of Is_Internal_File_Name and
+ Is_Predefined_File_Name in the Units table. This avoids a lot
+ of repeated text processing.
+
+2017-04-27 Emmanuel Briot <briot@adacore.com>
+
+ * g-comlin.adb (Sort_Sections): remove useless test.
+
+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cfhase.adb, a-cfhase.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.
+ (Equivalent_Keys): Functions over cursors are removed. They were
+ awkward with explicit container parameters.
+ * a-cforse.adb, a-cforse.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.
+
+2017-04-27 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb: Code cleanup.
+
+2017-04-27 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_util.adb (Replace_Entity): The prefix of a 'Result
+ attribute reference in a post- condition is the subprogram to
+ which the condition applies. If the condition is inherited
+ by a type extension, the prefix becomes a reference to the
+ inherited operation, but there is no need to create a wrapper
+ for this operation, because 'Result is expanded independently
+ when elaborating the postconditions.
+
2017-04-27 Bob Duff <duff@adacore.com>
* sinput.adb: Minor code cleanup.
package body Generic_Sorting with SPARK_Mode => Off is
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
+ begin
+ if M.Length (Container) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (Container, 1);
+
+ begin
+ for I in 2 .. M.Length (Container) loop
+ declare
+ E2 : constant Element_Type := Element (Container, I);
+
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+
+ E1 := E2;
+ end;
+ end loop;
+ end;
+
+ return True;
+ end M_Elements_Sorted;
+
+ end Formal_Model;
+
---------------
-- Is_Sorted --
---------------
return True;
end Is_Sorted;
- -----------------------
- -- M_Elements_Sorted --
- -----------------------
-
- function M_Elements_Sorted (Container : M.Sequence) return Boolean is
- begin
- if M.Length (Container) = 0 then
- return True;
- end if;
-
- declare
- E1 : Element_Type := Element (Container, 1);
-
- begin
- for I in 2 .. M.Length (Container) loop
- declare
- E2 : constant Element_Type := Element (Container, I);
-
- begin
- if E2 < E1 then
- return False;
- end if;
-
- E1 := E2;
- end;
- end loop;
- end;
-
- return True;
- end M_Elements_Sorted;
-
-----------
-- Merge --
-----------
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
- -- If Item is not is not contained in Container after Position, Find
- -- returns No_Element.
+ -- If Item is not contained in Container after Position, Find returns
+ -- No_Element.
(not M.Contains
(Container => Model (Container),
=>
Find'Result = No_Element,
- -- Otherwise, Find returns a valid cusror in Container
+ -- Otherwise, Find returns a valid cursor in Container
others =>
P.Has_Key (Positions (Container), Find'Result)
Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases =>
- -- If Item is not is not contained in Container before Position, Find
- -- returns No_Element.
+ -- If Item is not contained in Container before Position, Find returns
+ -- No_Element.
(not M.Contains
(Container => Model (Container),
=>
Reverse_Find'Result = No_Element,
- -- Otherwise, Find returns a valid cusror in Container
+ -- Otherwise, Find returns a valid cursor in Container
others =>
P.Has_Key (Positions (Container), Reverse_Find'Result)
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode is
- function M_Elements_Sorted (Container : M.Sequence) return Boolean with
- Ghost,
- Global => null,
- Post =>
- M_Elements_Sorted'Result =
- (for all I in 1 .. M.Length (Container) =>
- (for all J in I .. M.Length (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ package Formal_Model with Ghost is
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Elements_Sorted'Result =
+ (for all I in 1 .. M.Length (Container) =>
+ (for all J in I .. M.Length (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ end Formal_Model;
+ use Formal_Model;
function Is_Sorted (Container : List) return Boolean with
Global => null,
package body Formal_Model is
+ ----------
+ -- Find --
+ ----------
+
+ function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ is
+ begin
+ for I in 1 .. K.Length (Container) loop
+ if Equivalent_Keys (Key, K.Get (Container, I)) then
+ return I;
+ end if;
+ end loop;
+ return 0;
+ end Find;
+
+ ---------------------
+ -- K_Keys_Included --
+ ---------------------
+
+ function K_Keys_Included (Left : K.Sequence;
+ Right : K.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. K.Length (Left) loop
+ if not K.Contains (Right, 1, K.Length (Right), K.Get (Left, I))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end K_Keys_Included;
+
----------
-- Keys --
----------
type Element_Type is private;
with function Hash (Key : Key_Type) return Hash_Type;
- with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+ with function Equivalent_Keys
+ (Left : Key_Type;
+ Right : Key_Type) return Boolean is "=";
package Ada.Containers.Formal_Hashed_Maps with
SPARK_Mode
(Left : K.Sequence;
Right : K.Sequence) return Boolean renames K."<=";
+ function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ -- Search for Key in Container
+
+ with
+ Global => null,
+ Post =>
+ (if Find'Result > 0 then
+ Find'Result <= K.Length (Container)
+ and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+
+ function K_Keys_Included
+ (Left : K.Sequence;
+ Right : K.Sequence) return Boolean
+ -- Return True if Right contains all the keys of Left
+
+ with
+ Global => null,
+ Post =>
+ K_Keys_Included'Result =
+ (for all I in 1 .. K.Length (Left) =>
+ Find (Right, K.Get (Left, I)) > 0
+ and then K.Get (Right, Find (Right, K.Get (Left, I))) =
+ K.Get (Left, I));
+
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
Element_Type => Positive_Count_Type,
P_Left : P.Map;
P_Right : P.Map) return Boolean
with
- Ghost,
Global => null,
Post =>
(if Mapping_Preserved'Result then
P.Keys_Included (P_Left, P_Right)
+ -- Right contains all the keys of Left
+
+ and K_Keys_Included (K_Left, K_Right)
+
-- Mappings from cursors to elements induced by K_Left, P_Left
-- and K_Right, P_Right are the same.
-- It contains all the keys contained in Model
and (for all Key of Model (Container) =>
- (for some L of Keys'Result => Equivalent_Keys (L, Key)))
+ (Find (Keys'Result, Key) > 0
+ and then Equivalent_Keys
+ (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
-- It has no duplicate
+ and (for all I in 1 .. Length (Container) =>
+ Find (Keys'Result, K.Get (Keys'Result, I)) = I)
+
and (for all I in 1 .. Length (Container) =>
(for all J in 1 .. Length (Container) =>
(if Equivalent_Keys
with
Global => null,
Pre => Capacity <= Container.Capacity,
- Post => Model (Container) = Model (Container)'Old;
+ Post =>
+ Model (Container) = Model (Container)'Old
+ and Length (Container)'Old = Length (Container)
+
+ -- Actual keys are preserved
+
+ and K_Keys_Included (Keys (Container), Keys (Container)'Old)
+ and K_Keys_Included (Keys (Container)'Old, Keys (Container));
function Is_Empty (Container : Map) return Boolean with
Global => null,
-- Actual keys are preserved
- and (for all Key of Keys (Source) =>
- Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
+ and K_Keys_Included (Keys (Target), Keys (Source))
+ and K_Keys_Included (Keys (Source), Keys (Target));
function Copy
(Source : Map;
-- Actual keys are preserved
- and (for all Key of Keys (Source)'Old =>
- Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
+ and K_Keys_Included (Keys (Target), Keys (Source)'Old)
+ and K_Keys_Included (Keys (Source)'Old, Keys (Target));
procedure Insert
(Container : in out Map;
Global => null,
Contract_Cases =>
- -- If Key is not is not contained in Container, Find returns No_Element
+ -- If Key is not contained in Container, Find returns No_Element
(not Contains (Model (Container), Key) =>
Find'Result = No_Element,
others =>
P.Has_Key (Positions (Container), Find'Result)
+ and P.Get (Positions (Container), Find'Result) =
+ Find (Keys (Container), Key)
-- The key designated by the result of Find is Key
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
return Target;
end Copy;
- ---------------------
- -- Current_To_Last --
- ---------------------
-
- function Current_To_Last (Container : Set; Current : Cursor) return Set is
- Curs : Cursor := First (Container);
- C : Set (Container.Capacity, Container.Modulus) :=
- Copy (Container, Container.Capacity);
- Node : Count_Type;
-
- begin
- if Curs = No_Element then
- Clear (C);
- return C;
-
- elsif Current /= No_Element and not Has_Element (Container, Current) then
- raise Constraint_Error;
-
- else
- while Curs.Node /= Current.Node loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
- end loop;
-
- return C;
- end if;
- end Current_To_Last;
-
---------------------
-- Default_Modulus --
---------------------
return Is_Equivalent (Left, Right);
end Equivalent_Sets;
- -------------------------
- -- Equivalent_Elements --
- -------------------------
-
- function Equivalent_Elements
- (Left : Set;
- CLeft : Cursor;
- Right : Set;
- CRight : Cursor) return Boolean
- is
- begin
- if not Has_Element (Left, CLeft) then
- raise Constraint_Error with
- "Left cursor of Equivalent_Elements has no element";
- end if;
-
- if not Has_Element (Right, CRight) then
- raise Constraint_Error with
- "Right cursor of Equivalent_Elements has no element";
- end if;
-
- pragma Assert (Vet (Left, CLeft),
- "bad Left cursor in Equivalent_Elements");
- pragma Assert (Vet (Right, CRight),
- "bad Right cursor in Equivalent_Elements");
-
- declare
- LN : Node_Type renames Left.Nodes (CLeft.Node);
- RN : Node_Type renames Right.Nodes (CRight.Node);
- begin
- return Equivalent_Elements (LN.Element, RN.Element);
- end;
- end Equivalent_Elements;
-
- function Equivalent_Elements
- (Left : Set;
- CLeft : Cursor;
- Right : Element_Type) return Boolean
- is
- begin
- if not Has_Element (Left, CLeft) then
- raise Constraint_Error with
- "Left cursor of Equivalent_Elements has no element";
- end if;
-
- pragma Assert (Vet (Left, CLeft),
- "Left cursor in Equivalent_Elements is bad");
-
- declare
- LN : Node_Type renames Left.Nodes (CLeft.Node);
- begin
- return Equivalent_Elements (LN.Element, Right);
- end;
- end Equivalent_Elements;
-
- function Equivalent_Elements
- (Left : Element_Type;
- Right : Set;
- CRight : Cursor) return Boolean
- is
- begin
- if not Has_Element (Right, CRight) then
- raise Constraint_Error with
- "Right cursor of Equivalent_Elements has no element";
- end if;
-
- pragma Assert
- (Vet (Right, CRight),
- "Right cursor of Equivalent_Elements is bad");
-
- declare
- RN : Node_Type renames Right.Nodes (CRight.Node);
- begin
- return Equivalent_Elements (Left, RN.Element);
- end;
- end Equivalent_Elements;
-
---------------------
-- Equivalent_Keys --
---------------------
return (Node => Node);
end First;
- -----------------------
- -- First_To_Previous --
- -----------------------
+ ------------------
+ -- Formal_Model --
+ ------------------
- function First_To_Previous
- (Container : Set;
- Current : Cursor) return Set
- is
- Curs : Cursor := Current;
- C : Set (Container.Capacity, Container.Modulus) :=
- Copy (Container, Container.Capacity);
- Node : Count_Type;
+ package body Formal_Model is
- begin
- if Curs = No_Element then
- return C;
+ -------------------------
+ -- E_Elements_Included --
+ -------------------------
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Left) loop
+ if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
+ then
+ return False;
+ end if;
+ end loop;
- elsif not Has_Element (Container, Curs) then
- raise Constraint_Error;
+ return True;
+ end E_Elements_Included;
- else
- while Curs.Node /= 0 loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Model : M.Set;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Left) loop
+ declare
+ Item : constant Element_Type := E.Get (Left, I);
+ begin
+ if M.Contains (Model, Item) then
+ if not E.Contains (Right, 1, E.Length (Right), Item) then
+ return False;
+ end if;
+ end if;
+ end;
end loop;
- return C;
- end if;
- end First_To_Previous;
+ return True;
+ end E_Elements_Included;
+
+ function E_Elements_Included
+ (Container : E.Sequence;
+ Model : M.Set;
+ Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Container) loop
+ declare
+ Item : constant Element_Type := E.Get (Container, I);
+ begin
+ if M.Contains (Model, Item) then
+ if not E.Contains (Left, 1, E.Length (Left), Item) then
+ return False;
+ end if;
+ else
+ if not E.Contains (Right, 1, E.Length (Right), Item) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end E_Elements_Included;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : E.Sequence;
+ Item : Element_Type) return Count_Type
+ is
+ begin
+ for I in 1 .. E.Length (Container) loop
+ if Equivalent_Elements (Item, E.Get (Container, I)) then
+ return I;
+ end if;
+ end loop;
+ return 0;
+ end Find;
+
+ --------------
+ -- Elements --
+ --------------
+
+ function Elements (Container : Set) return E.Sequence is
+ Position : Count_Type := HT_Ops.First (Container);
+ R : E.Sequence;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := E.Add (R, Container.Nodes (Position).Element);
+ Position := HT_Ops.Next (Container, Position);
+ end loop;
+
+ return R;
+ end Elements;
+
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
+
+ procedure Lift_Abstraction_Level (Container : Set) is null;
+
+ -----------------------
+ -- Mapping_Preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > E.Length (E_Left)
+ or else P.Get (P_Right, C) > E.Length (E_Right)
+ or else E.Get (E_Left, P.Get (P_Left, C)) /=
+ E.Get (E_Right, P.Get (P_Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved;
+
+ ------------------------------
+ -- Mapping_Preserved_Except --
+ ------------------------------
+
+ function Mapping_Preserved_Except
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map;
+ Position : Cursor) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if C /= Position
+ and (not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > E.Length (E_Left)
+ or else P.Get (P_Right, C) > E.Length (E_Right)
+ or else E.Get (E_Left, P.Get (P_Left, C)) /=
+ E.Get (E_Right, P.Get (P_Right, C)))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved_Except;
+
+ -----------
+ -- Model --
+ -----------
+
+ function Model (Container : Set) return M.Set is
+ Position : Count_Type := HT_Ops.First (Container);
+ R : M.Set;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R :=
+ M.Add
+ (Container => R,
+ Item => Container.Nodes (Position).Element);
+
+ Position := HT_Ops.Next (Container, Position);
+ end loop;
+
+ return R;
+ end Model;
+
+ ---------------
+ -- Positions --
+ ---------------
+
+ function Positions (Container : Set) return P.Map is
+ I : Count_Type := 1;
+ Position : Count_Type := HT_Ops.First (Container);
+ R : P.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := P.Add (R, (Node => Position), I);
+ pragma Assert (P.Length (R) = I);
+ Position := HT_Ops.Next (Container, Position);
+ I := I + 1;
+ end loop;
+
+ return R;
+ end Positions;
+
+ end Formal_Model;
----------
-- Free --
HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
+ package body Generic_Keys with SPARK_Mode => Off is
+
+ -----------------------
+ -- Local Subprograms --
+ -----------------------
+
+ function Equivalent_Key_Node
+ (Key : Key_Type;
+ Node : Node_Type) return Boolean;
+ pragma Inline (Equivalent_Key_Node);
+
+ --------------------------
+ -- Local Instantiations --
+ --------------------------
+
+ package Key_Keys is
+ new Hash_Tables.Generic_Bounded_Keys
+ (HT_Types => HT_Types,
+ Next => Next,
+ Set_Next => Set_Next,
+ Key_Type => Key_Type,
+ Hash => Hash,
+ Equivalent_Keys => Equivalent_Key_Node);
+
+ --------------
+ -- Contains --
+ --------------
+
+ function Contains
+ (Container : Set;
+ Key : Key_Type) return Boolean
+ is
+ begin
+ return Find (Container, Key) /= No_Element;
+ end Contains;
+
+ ------------
+ -- Delete --
+ ------------
+
+ procedure Delete
+ (Container : in out Set;
+ Key : Key_Type)
+ is
+ X : Count_Type;
+
+ begin
+ Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+
+ if X = 0 then
+ raise Constraint_Error with "attempt to delete key not in set";
+ end if;
+
+ Free (Container, X);
+ end Delete;
+
+ -------------
+ -- Element --
+ -------------
+
+ function Element
+ (Container : Set;
+ Key : Key_Type) return Element_Type
+ is
+ Node : constant Count_Type := Find (Container, Key).Node;
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with "key not in map";
+ end if;
+
+ return Container.Nodes (Node).Element;
+ end Element;
+
+ -------------------------
+ -- Equivalent_Key_Node --
+ -------------------------
+
+ function Equivalent_Key_Node
+ (Key : Key_Type;
+ Node : Node_Type) return Boolean
+ is
+ begin
+ return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element));
+ end Equivalent_Key_Node;
+
+ -------------
+ -- Exclude --
+ -------------
+
+ procedure Exclude
+ (Container : in out Set;
+ Key : Key_Type)
+ is
+ X : Count_Type;
+ begin
+ Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
+ Free (Container, X);
+ end Exclude;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : Set;
+ Key : Key_Type) return Cursor
+ is
+ Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ begin
+ return (if Node = 0 then No_Element else (Node => Node));
+ end Find;
+
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Included_Except --
+ -----------------------
+
+ function M_Included_Except
+ (Left : M.Set;
+ Right : M.Set;
+ Key : Key_Type) return Boolean
+ is
+ begin
+ for E of Left loop
+ if not Contains (Right, E)
+ and not Equivalent_Keys (Generic_Keys.Key (E), Key)
+ then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end M_Included_Except;
+
+ end Formal_Model;
+
+ ---------
+ -- Key --
+ ---------
+
+ function Key (Container : Set; Position : Cursor) return Key_Type is
+ begin
+ if not Has_Element (Container, Position) then
+ raise Constraint_Error with
+ "Position cursor has no element";
+ end if;
+
+ pragma Assert
+ (Vet (Container, Position), "bad cursor in function Key");
+
+ declare
+ N : Node_Type renames Container.Nodes (Position.Node);
+ begin
+ return Key (N.Element);
+ end;
+ end Key;
+
+ -------------
+ -- Replace --
+ -------------
+
+ procedure Replace
+ (Container : in out Set;
+ Key : Key_Type;
+ New_Item : Element_Type)
+ is
+ Node : constant Count_Type := Key_Keys.Find (Container, Key);
+
+ begin
+ if Node = 0 then
+ raise Constraint_Error with
+ "attempt to replace key not in set";
+ end if;
+
+ Replace_Element (Container, Node, New_Item);
+ end Replace;
+
+ end Generic_Keys;
+
-----------------
-- Has_Element --
-----------------
Node.Next := Next;
end Set_Next;
- ------------------
- -- Strict_Equal --
- ------------------
-
- function Strict_Equal (Left, Right : Set) return Boolean is
- CuL : Cursor := First (Left);
- CuR : Cursor := First (Right);
-
- begin
- if Length (Left) /= Length (Right) then
- return False;
- end if;
-
- while CuL.Node /= 0 or CuR.Node /= 0 loop
- if CuL.Node /= CuR.Node
- or else Left.Nodes (CuL.Node).Element /=
- Right.Nodes (CuR.Node).Element
- then
- return False;
- end if;
-
- CuL := Next (Left, CuL);
- CuR := Next (Right, CuR);
- end loop;
-
- return True;
- end Strict_Equal;
-
--------------------------
-- Symmetric_Difference --
--------------------------
end;
end Vet;
- package body Generic_Keys with SPARK_Mode => Off is
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- function Equivalent_Key_Node
- (Key : Key_Type;
- Node : Node_Type) return Boolean;
- pragma Inline (Equivalent_Key_Node);
-
- --------------------------
- -- Local Instantiations --
- --------------------------
-
- package Key_Keys is
- new Hash_Tables.Generic_Bounded_Keys
- (HT_Types => HT_Types,
- Next => Next,
- Set_Next => Set_Next,
- Key_Type => Key_Type,
- Hash => Hash,
- Equivalent_Keys => Equivalent_Key_Node);
-
- --------------
- -- Contains --
- --------------
-
- function Contains
- (Container : Set;
- Key : Key_Type) return Boolean
- is
- begin
- return Find (Container, Key) /= No_Element;
- end Contains;
-
- ------------
- -- Delete --
- ------------
-
- procedure Delete
- (Container : in out Set;
- Key : Key_Type)
- is
- X : Count_Type;
-
- begin
- Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
-
- if X = 0 then
- raise Constraint_Error with "attempt to delete key not in set";
- end if;
-
- Free (Container, X);
- end Delete;
-
- -------------
- -- Element --
- -------------
-
- function Element
- (Container : Set;
- Key : Key_Type) return Element_Type
- is
- Node : constant Count_Type := Find (Container, Key).Node;
-
- begin
- if Node = 0 then
- raise Constraint_Error with "key not in map";
- end if;
-
- return Container.Nodes (Node).Element;
- end Element;
-
- -------------------------
- -- Equivalent_Key_Node --
- -------------------------
-
- function Equivalent_Key_Node
- (Key : Key_Type;
- Node : Node_Type) return Boolean
- is
- begin
- return Equivalent_Keys (Key, Generic_Keys.Key (Node.Element));
- end Equivalent_Key_Node;
-
- -------------
- -- Exclude --
- -------------
-
- procedure Exclude
- (Container : in out Set;
- Key : Key_Type)
- is
- X : Count_Type;
- begin
- Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
- Free (Container, X);
- end Exclude;
-
- ----------
- -- Find --
- ----------
-
- function Find
- (Container : Set;
- Key : Key_Type) return Cursor
- is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
- begin
- return (if Node = 0 then No_Element else (Node => Node));
- end Find;
-
- ---------
- -- Key --
- ---------
-
- function Key (Container : Set; Position : Cursor) return Key_Type is
- begin
- if not Has_Element (Container, Position) then
- raise Constraint_Error with
- "Position cursor has no element";
- end if;
-
- pragma Assert
- (Vet (Container, Position), "bad cursor in function Key");
-
- declare
- N : Node_Type renames Container.Nodes (Position.Node);
- begin
- return Key (N.Element);
- end;
- end Key;
-
- -------------
- -- Replace --
- -------------
-
- procedure Replace
- (Container : in out Set;
- Key : Key_Type;
- New_Item : Element_Type)
- is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
-
- begin
- if Node = 0 then
- raise Constraint_Error with
- "attempt to replace key not in set";
- end if;
-
- Replace_Element (Container, Node, New_Item);
- end Replace;
-
- end Generic_Keys;
-
end Ada.Containers.Formal_Hashed_Sets;
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2017, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- which is not possible if cursors encapsulate an access to the underlying
-- container.
--- There are three new functions:
-
--- function Strict_Equal (Left, Right : Set) return Boolean;
--- function First_To_Previous (Container : Set; Current : Cursor)
--- return Set;
--- function Current_To_Last (Container : Set; Current : Cursor)
--- return Set;
-
--- See detailed specifications for these subprograms
-
+with Ada.Containers.Functional_Maps;
+with Ada.Containers.Functional_Sets;
+with Ada.Containers.Functional_Vectors;
private with Ada.Containers.Hash_Tables;
generic
with function Hash (Element : Element_Type) return Hash_Type;
with function Equivalent_Elements (Left, Right : Element_Type)
- return Boolean;
-
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
-
+ return Boolean is "=";
package Ada.Containers.Formal_Hashed_Sets with
- Pure,
SPARK_Mode
is
- pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis);
type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
Default_Initial_Condition => Is_Empty (Set);
pragma Preelaborable_Initialization (Set);
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
+ type Cursor is record
+ Node : Count_Type;
+ end record;
- Empty_Set : constant Set;
+ No_Element : constant Cursor := (Node => 0);
+
+ function Length (Container : Set) return Count_Type with
+ Global => null,
+ Post => Length'Result <= Container.Capacity;
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ package Formal_Model with Ghost is
+ subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+ package M is new Ada.Containers.Functional_Sets
+ (Element_Type => Element_Type,
+ Equivalent_Elements => Equivalent_Elements);
+
+ function "="
+ (Left : M.Set;
+ Right : M.Set) return Boolean renames M."=";
+
+ function "<="
+ (Left : M.Set;
+ Right : M.Set) return Boolean renames M."<=";
+
+ package E is new Ada.Containers.Functional_Vectors
+ (Element_Type => Element_Type,
+ Index_Type => Positive_Count_Type);
+
+ function "="
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."=";
+
+ function "<"
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."<";
+
+ function "<="
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."<=";
+
+ function Find
+ (Container : E.Sequence;
+ Item : Element_Type) return Count_Type
+ -- Search for Item in Container
+
+ with
+ Global => null,
+ Post =>
+ (if Find'Result > 0 then
+ Find'Result <= E.Length (Container)
+ and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ -- The elements of Left are contained in Right
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Left) =>
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Model : M.Set;
+ Right : E.Sequence) return Boolean
+ -- The elements of Container contained in Model are in Right
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Left) =>
+ (if M.Contains (Model, E.Get (Left, I)) then
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ function E_Elements_Included
+ (Container : E.Sequence;
+ Model : M.Set;
+ Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ -- The elements of Container contained in Model are in Left and others
+ -- are in Right.
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Container) =>
+ (if M.Contains (Model, E.Get (Container, I)) then
+ Find (Left, E.Get (Container, I)) > 0
+ and then E.Get (Left, Find (Left, E.Get (Container, I))) =
+ E.Get (Container, I)
+ else
+ Find (Right, E.Get (Container, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Container, I))) =
+ E.Get (Container, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ package P is new Ada.Containers.Functional_Maps
+ (Key_Type => Cursor,
+ Element_Type => Positive_Count_Type,
+ Equivalent_Keys => "=",
+ Enable_Handling_Of_Equivalence => False);
+
+ function "="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."=";
+
+ function "<="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."<=";
+
+ function Mapping_Preserved
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved'Result then
+
+ -- Right contains all the cursors of Left
+
+ P.Keys_Included (P_Left, P_Right)
+
+ -- Right contains all the elements of Left
+
+ and E_Elements_Included (E_Left, E_Right)
- No_Element : constant Cursor;
+ -- Mappings from cursors to elements induced by E_Left, P_Left
+ -- and E_Right, P_Right are the same.
+
+ and (for all C of P_Left =>
+ E.Get (E_Left, P.Get (P_Left, C)) =
+ E.Get (E_Right, P.Get (P_Right, C))));
+
+ function Mapping_Preserved_Except
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map;
+ Position : Cursor) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved_Except'Result then
+
+ -- Right contains all the cursors of Left
+
+ P.Keys_Included (P_Left, P_Right)
+
+ -- Mappings from cursors to elements induced by E_Left, P_Left
+ -- and E_Right, P_Right are the same except for Position.
+
+ and (for all C of P_Left =>
+ (if C /= Position then
+ E.Get (E_Left, P.Get (P_Left, C)) =
+ E.Get (E_Right, P.Get (P_Right, C)))));
+
+ function Model (Container : Set) return M.Set with
+ -- The high-level model of a set is a set of elements. Neither cursors
+ -- nor order of elements are represented in this model. Elements are
+ -- modeled up to equivalence.
+
+ Ghost,
+ Global => null,
+ Post => M.Length (Model'Result) = Length (Container);
+
+ function Elements (Container : Set) return E.Sequence with
+ -- The Elements sequence represents the underlying list structure of
+ -- sets that is used for iteration. It stores the actual values of
+ -- elements in the set. It does not model cursors.
+
+ Ghost,
+ Global => null,
+ Post =>
+ E.Length (Elements'Result) = Length (Container)
+
+ -- It only contains keys contained in Model
+
+ and (for all Item of Elements'Result =>
+ M.Contains (Model (Container), Item))
+
+ -- It contains all the elements contained in Model
+
+ and (for all Item of Model (Container) =>
+ (Find (Elements'Result, Item) > 0
+ and then Equivalent_Elements
+ (E.Get (Elements'Result, Find (Elements'Result, Item)),
+ Item)))
+
+ -- It has no duplicate
+
+ and (for all I in 1 .. Length (Container) =>
+ Find (Elements'Result, E.Get (Elements'Result, I)) = I)
+
+ and (for all I in 1 .. Length (Container) =>
+ (for all J in 1 .. Length (Container) =>
+ (if Equivalent_Elements
+ (E.Get (Elements'Result, I),
+ E.Get (Elements'Result, J))
+ then I = J)));
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
+
+ function Positions (Container : Set) return P.Map with
+ -- The Positions map is used to model cursors. It only contains valid
+ -- cursors and maps them to their position in the container.
+
+ Ghost,
+ Global => null,
+ Post =>
+ not P.Has_Key (Positions'Result, No_Element)
+
+ -- Positions of cursors are smaller than the container's length
+
+ and then
+ (for all I of Positions'Result =>
+ P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+ -- No two cursors have the same position. Note that we do not
+ -- state that there is a cursor in the map for each position, as
+ -- it is rarely needed.
+
+ and then
+ (for all J of Positions'Result =>
+ (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
+ then I = J)));
+
+ procedure Lift_Abstraction_Level (Container : Set) with
+ -- Lift_Abstraction_Level is a ghost procedure that does nothing but
+ -- assume that we can access the same elements by iterating over
+ -- positions or cursors.
+ -- This information is not generally useful except when switching from
+ -- a low-level, cursor-aware view of a container, to a high-level,
+ -- position-based view.
+
+ Ghost,
+ Global => null,
+ Post =>
+ (for all Item of Elements (Container) =>
+ (for some I of Positions (Container) =>
+ E.Get (Elements (Container), P.Get (Positions (Container), I)) =
+ Item));
+
+ function Contains
+ (C : M.Set;
+ K : Element_Type) return Boolean renames M.Contains;
+ -- To improve readability of contracts, we rename the function used to
+ -- search for an element in the model to Contains.
+
+ end Formal_Model;
+ use Formal_Model;
+
+ Empty_Set : constant Set;
function "=" (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+ "="'Result =
+ (Length (Left) = Length (Right)
+ and E_Elements_Included (Elements (Left), Elements (Right)))
+ and
+ "="'Result =
+ (E_Elements_Included (Elements (Left), Elements (Right))
+ and E_Elements_Included (Elements (Right), Elements (Left)));
function Equivalent_Sets (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
function To_Set (New_Item : Element_Type) return Set with
- Global => null;
+ Global => null,
+ Post =>
+ M.Is_Singleton (Model (To_Set'Result), New_Item)
+ and Length (To_Set'Result) = 1
+ and E.Get (Elements (To_Set'Result), 1) = New_Item;
function Capacity (Container : Set) return Count_Type with
- Global => null;
+ Global => null,
+ Post => Capacity'Result = Container.Capacity;
procedure Reserve_Capacity
(Container : in out Set;
Capacity : Count_Type)
with
Global => null,
- Pre => Capacity <= Container.Capacity;
+ Pre => Capacity <= Container.Capacity,
+ Post =>
+ Model (Container) = Model (Container)'Old
+ and Length (Container)'Old = Length (Container)
- function Length (Container : Set) return Count_Type with
- Global => null;
+ -- Actual elements are preserved
+
+ and
+ E_Elements_Included
+ (Elements (Container), Elements (Container)'Old)
+ and
+ E_Elements_Included
+ (Elements (Container)'Old, Elements (Container));
function Is_Empty (Container : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Set) with
- Global => null;
+ Global => null,
+ Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
procedure Assign (Target : in out Set; Source : Set) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Model (Target) = Model (Source)
+ and Length (Target) = Length (Source)
+
+ -- Actual elements are preserved
+
+ and
+ E_Elements_Included (Elements (Target), Elements (Source))
+ and
+ E_Elements_Included (Elements (Source), Elements (Target));
function Copy
(Source : Set;
Capacity : Count_Type := 0) return Set
with
Global => null,
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity,
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Elements (Copy'Result) = Elements (Source)
+ and Positions (Copy'Result) = Positions (Source)
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Source.Capacity
+ else
+ Copy'Result.Capacity = Capacity);
function Element
(Container : Set;
Position : Cursor) return Element_Type
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Element'Result =
+ E.Get (Elements (Container), P.Get (Positions (Container), Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Set;
New_Item : Element_Type)
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Position now maps to New_Item
+
+ and Element (Container, Position) = New_Item
+
+ -- New_Item is contained in Container
+
+ and Contains (Model (Container), New_Item)
+
+ -- Other elements are preserved
+
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Element (Container, Position)'Old)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved_Except
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container),
+ Position => Position)
+ and Positions (Container) = Positions (Container)'Old;
procedure Move (Target : in out Set; Source : in out Set) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Length (Source) = 0
+ and Model (Target) = Model (Source)'Old
+ and Length (Target) = Length (Source)'Old
+
+ -- Actual elements are preserved
+
+ and
+ E_Elements_Included (Elements (Target), Elements (Source)'Old)
+ and
+ E_Elements_Included (Elements (Source)'Old, Elements (Target));
procedure Insert
(Container : in out Set;
Position : out Cursor;
Inserted : out Boolean)
with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity
+ or Contains (Container, New_Item),
+ Post =>
+ Contains (Container, New_Item)
+ and Has_Element (Container, Position)
+ and Equivalent_Elements (Element (Container, Position), New_Item),
+ Contract_Cases =>
+
+ -- If New_Item is already in Container, it is not modified and Inserted
+ -- is set to False.
+
+ (Contains (Container, New_Item) =>
+ not Inserted
+ and Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, New_Item is inserted in Container and Inserted is set to
+ -- True.
+
+ others =>
+ Inserted
+ and Length (Container) = Length (Container)'Old + 1
+
+ -- Position now maps to New_Item
+
+ and Element (Container, Position) = New_Item
+
+ -- Other elements are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Position));
procedure Insert (Container : in out Set; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, New_Item));
+ and then (not Contains (Container, New_Item)),
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+ and Contains (Container, New_Item)
+ and Element (Container, Find (Container, New_Item)) = New_Item
+
+ -- Other elements are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Find (Container, New_Item));
procedure Include (Container : in out Set; New_Item : Element_Type) with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity
+ or Contains (Container, New_Item),
+ Post =>
+ Contains (Container, New_Item)
+ and Element (Container, Find (Container, New_Item)) = New_Item,
+ Contract_Cases =>
+
+ -- If an element equivalent to New_Item is already in Container, it is
+ -- replaced by New_Item.
+
+ (Contains (Container, New_Item) =>
+
+ -- Elements are preserved modulo equivalence
+
+ Model (Container) = Model (Container)'Old
+
+ -- Cursors are preserved
+
+ and Positions (Container) = Positions (Container)'Old
+
+ -- The actual value of other elements is preserved
+
+ and E.Equal_Except
+ (Elements (Container)'Old,
+ Elements (Container),
+ P.Get (Positions (Container), Find (Container, New_Item))),
+
+ -- Otherwise, New_Item is inserted in Container
+
+ others =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Other elements are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Find (Container, New_Item)));
procedure Replace (Container : in out Set; New_Item : Element_Type) with
Global => null,
- Pre => Contains (Container, New_Item);
+ Pre => Contains (Container, New_Item),
+ Post =>
- procedure Exclude (Container : in out Set; Item : Element_Type) with
- Global => null;
+ -- Elements are preserved modulo equivalence
+
+ Model (Container) = Model (Container)'Old
+ and Contains (Container, New_Item)
- procedure Delete (Container : in out Set; Item : Element_Type) with
+ -- Cursors are preserved
+
+ and Positions (Container) = Positions (Container)'Old
+
+ -- The element equivalent to New_Item in Container is replaced by
+ -- New_Item.
+
+ and Element (Container, Find (Container, New_Item)) = New_Item
+ and E.Equal_Except
+ (Elements (Container)'Old,
+ Elements (Container),
+ P.Get (Positions (Container), Find (Container, New_Item)));
+
+ procedure Exclude (Container : in out Set; Item : Element_Type) with
+ Global => null,
+ Post => not Contains (Container, Item),
+ Contract_Cases =>
+
+ -- If Item is not in Container, nothing is changed
+
+ (not Contains (Container, Item) =>
+ Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Item is removed from Container
+
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container),
+ E_Right => Elements (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Item)'Old));
+
+ procedure Delete (Container : in out Set; Item : Element_Type) with
Global => null,
- Pre => Contains (Container, Item);
+ Pre => Contains (Container, Item),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Item is no longer in Container
+
+ and not Contains (Container, Item)
- procedure Delete (Container : in out Set; Position : in out Cursor) with
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container),
+ E_Right => Elements (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Item)'Old);
+
+ procedure Delete (Container : in out Set; Position : in out Cursor) with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Position = No_Element
+ and Length (Container) = Length (Container)'Old - 1
+
+ -- The element at position Position is no longer in Container
+
+ and not Contains (Container, Element (Container, Position)'Old)
+ and not P.Has_Key (Positions (Container), Position'Old)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Element (Container, Position)'Old)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container),
+ E_Right => Elements (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Position'Old);
procedure Union (Target : in out Set; Source : Set) with
Global => null,
- Pre => Length (Target) + Length (Source) -
- Length (Intersection (Target, Source)) <= Target.Capacity;
+ Pre =>
+ Length (Source) - Length (Target and Source) <=
+ Target.Capacity - Length (Target),
+ Post =>
+ Length (Target) = Length (Target)'Old
+ - M.Num_Overlaps (Model (Target)'Old, Model (Source))
+ + Length (Source)
+
+ -- Elements already in Target are still in Target
+
+ and Model (Target)'Old <= Model (Target)
+
+ -- Elements of Source are included in Target
+
+ and Model (Source) <= Model (Target)
+
+ -- Elements of Target come from either Source or Target
+
+ and
+ M.Included_In_Union
+ (Model (Target), Model (Source), Model (Target)'Old)
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
+ and
+ E_Elements_Included
+ (Elements (Source),
+ Model (Target)'Old,
+ Elements (Source),
+ Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target)'Old,
+ E_Right => Elements (Target),
+ P_Left => Positions (Target)'Old,
+ P_Right => Positions (Target));
function Union (Left, Right : Set) return Set with
Global => null,
- Pre => Length (Left) + Length (Right) -
- Length (Intersection (Left, Right)) <= Count_Type'Last;
+ Pre => Length (Left) <= Count_Type'Last - Length (Right),
+ Post =>
+ Length (Union'Result) = Length (Left)
+ - M.Num_Overlaps (Model (Left), Model (Right))
+ + Length (Right)
+
+ -- Elements of Left and Right are in the result of Union
+
+ and Model (Left) <= Model (Union'Result)
+ and Model (Right) <= Model (Union'Result)
+
+ -- Elements of the result of union come from either Left or Right
+
+ and
+ M.Included_In_Union
+ (Model (Union'Result), Model (Left), Model (Right))
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Union'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+ and
+ E_Elements_Included
+ (Elements (Left), Model (Left), Elements (Union'Result))
+ and
+ E_Elements_Included
+ (Elements (Right),
+ Model (Left),
+ Elements (Right),
+ Elements (Union'Result));
function "or" (Left, Right : Set) return Set renames Union;
procedure Intersection (Target : in out Set; Source : Set) with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Target) =
+ M.Num_Overlaps (Model (Target)'Old, Model (Source))
+
+ -- Elements of Target were already in Target
+
+ and Model (Target) <= Model (Target)'Old
+
+ -- Elements of Target are in Source
+
+ and Model (Target) <= Model (Source)
+
+ -- Elements both in Source and Target are in the intersection
+
+ and
+ M.Includes_Intersection
+ (Model (Target), Model (Source), Model (Target)'Old)
+
+ -- Actual value of elements of Target is preserved
+
+ and E_Elements_Included (Elements (Target), Elements (Target)'Old)
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Source), Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target),
+ E_Right => Elements (Target)'Old,
+ P_Left => Positions (Target),
+ P_Right => Positions (Target)'Old);
function Intersection (Left, Right : Set) return Set with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Intersection'Result) =
+ M.Num_Overlaps (Model (Left), Model (Right))
+
+ -- Elements in the result of Intersection are in Left and Right
+
+ and Model (Intersection'Result) <= Model (Left)
+ and Model (Intersection'Result) <= Model (Right)
+
+ -- Elements both in Left and Right are in the result of Intersection
+
+ and
+ M.Includes_Intersection
+ (Model (Intersection'Result), Model (Left), Model (Right))
+
+ -- Actual value of elements come from Left
+
+ and
+ E_Elements_Included
+ (Elements (Intersection'Result), Elements (Left))
+ and
+ E_Elements_Included
+ (Elements (Left), Model (Right), Elements (Intersection'Result));
function "and" (Left, Right : Set) return Set renames Intersection;
procedure Difference (Target : in out Set; Source : Set) with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Target) = Length (Target)'Old -
+ M.Num_Overlaps (Model (Target)'Old, Model (Source))
+
+ -- Elements of Target were already in Target
+
+ and Model (Target) <= Model (Target)'Old
+
+ -- Elements of Target are not in Source
+
+ and M.No_Overlap (Model (Target), Model (Source))
+
+ -- Elements in Target but not in Source are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
+
+ -- Actual value of elements of Target is preserved
+
+ and E_Elements_Included (Elements (Target), Elements (Target)'Old)
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target),
+ E_Right => Elements (Target)'Old,
+ P_Left => Positions (Target),
+ P_Right => Positions (Target)'Old);
function Difference (Left, Right : Set) return Set with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Difference'Result) = Length (Left) -
+ M.Num_Overlaps (Model (Left), Model (Right))
+
+ -- Elements of the result of Difference are in Left
+
+ and Model (Difference'Result) <= Model (Left)
+
+ -- Elements of the result of Difference are in Right
+
+ and M.No_Overlap (Model (Difference'Result), Model (Right))
+
+ -- Elements in Left but not in Right are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Left), Model (Difference'Result), Model (Right))
+
+ -- Actual value of elements come from Left
+
+ and
+ E_Elements_Included (Elements (Difference'Result), Elements (Left))
+ and
+ E_Elements_Included
+ (Elements (Left),
+ Model (Difference'Result),
+ Elements (Difference'Result));
function "-" (Left, Right : Set) return Set renames Difference;
procedure Symmetric_Difference (Target : in out Set; Source : Set) with
Global => null,
- Pre => Length (Target) + Length (Source) -
- 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
+ Pre =>
+ Length (Source) - Length (Target and Source) <=
+ Target.Capacity - Length (Target) + Length (Target and Source),
+ Post =>
+ Length (Target) = Length (Target)'Old -
+ 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
+ Length (Source)
+
+ -- Elements of the difference were not both in Source and in Target
+
+ and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
+
+ -- Elements in Target but not in Source are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
+
+ -- Elements in Source but not in Target are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Source), Model (Target), Model (Target)'Old)
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
+ and
+ E_Elements_Included
+ (Elements (Source), Model (Target), Elements (Target));
function Symmetric_Difference (Left, Right : Set) return Set with
Global => null,
- Pre => Length (Left) + Length (Right) -
- 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
+ Pre => Length (Left) <= Count_Type'Last - Length (Right),
+ Post =>
+ Length (Symmetric_Difference'Result) = Length (Left) -
+ 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
+ Length (Right)
+
+ -- Elements of the difference were not both in Left and Right
+
+ and
+ M.Not_In_Both
+ (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
+
+ -- Elements in Left but not in Right are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
+
+ -- Elements in Right but not in Left are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Symmetric_Difference'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+ and
+ E_Elements_Included
+ (Elements (Left),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result))
+ and
+ E_Elements_Included
+ (Elements (Right),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result));
function "xor" (Left, Right : Set) return Set
renames Symmetric_Difference;
function Overlap (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+ Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
function First (Container : Set) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ First'Result = No_Element,
+
+ others =>
+ Has_Element (Container, First'Result)
+ and P.Get (Positions (Container), First'Result) = 1);
function Next (Container : Set; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Next'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Next'Result)
+ and then P.Get (Positions (Container), Next'Result) =
+ P.Get (Positions (Container), Position) + 1);
procedure Next (Container : Set; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) + 1);
function Find
(Container : Set;
Item : Element_Type) return Cursor
with
- Global => null;
+ Global => null,
+ Contract_Cases =>
- function Contains (Container : Set; Item : Element_Type) return Boolean with
- Global => null;
+ -- If Item is not contained in Container, Find returns No_Element
- function Has_Element (Container : Set; Position : Cursor) return Boolean
- with
- Global => null;
+ (not Contains (Model (Container), Item) =>
+ Find'Result = No_Element,
- function Equivalent_Elements (Left : Set; CLeft : Cursor;
- Right : Set; CRight : Cursor) return Boolean
- with
- Global => null;
+ -- Otherwise, Find returns a valid cursor in Container
- function Equivalent_Elements
- (Left : Set; CLeft : Cursor;
- Right : Element_Type) return Boolean
- with
- Global => null;
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
+ and P.Get (Positions (Container), Find'Result) =
+ Find (Elements (Container), Item)
+
+ -- The element designated by the result of Find is Item
+
+ and Equivalent_Elements
+ (Element (Container, Find'Result), Item));
- function Equivalent_Elements
- (Left : Element_Type;
- Right : Set; CRight : Cursor) return Boolean
+ function Contains (Container : Set; Item : Element_Type) return Boolean with
+ Global => null,
+ Post => Contains'Result = Contains (Model (Container), Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, Contains);
+
+ function Has_Element (Container : Set; Position : Cursor) return Boolean
with
- Global => null;
+ Global => null,
+ Post =>
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
+ pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
function Default_Modulus (Capacity : Count_Type) return Hash_Type with
Global => null;
package Generic_Keys with SPARK_Mode is
+ package Formal_Model with Ghost is
+
+ function M_Included_Except
+ (Left : M.Set;
+ Right : M.Set;
+ Key : Key_Type) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Included_Except'Result =
+ (for all E of Left =>
+ Contains (Right, E)
+ or Equivalent_Keys (Generic_Keys.Key (E), Key));
+
+ end Formal_Model;
+ use Formal_Model;
+
function Key (Container : Set; Position : Cursor) return Key_Type with
- Global => null;
+ Global => null,
+ Post => Key'Result = Key (Element (Container, Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Key);
function Element (Container : Set; Key : Key_Type) return Element_Type
with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Element'Result = Element (Container, Find (Container, Key));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace
(Container : in out Set;
Key : Key_Type;
New_Item : Element_Type)
with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Key now maps to New_Item
+
+ and Element (Container, Key) = New_Item
+
+ -- New_Item is contained in Container
+
+ and Contains (Model (Container), New_Item)
+
+ -- Other elements are preserved
+
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved_Except
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container),
+ Position => Find (Container, Key))
+ and Positions (Container) = Positions (Container)'Old;
procedure Exclude (Container : in out Set; Key : Key_Type) with
- Global => null;
+ Global => null,
+ Post => not Contains (Container, Key),
+ Contract_Cases =>
+
+ -- If Key is not in Container, nothing is changed
+
+ (not Contains (Container, Key) =>
+ Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Key is removed from Container
+
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container),
+ E_Right => Elements (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Key)'Old));
procedure Delete (Container : in out Set; Key : Key_Type) with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Key is no longer in Container
+
+ and not Contains (Container, Key)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Container),
+ E_Right => Elements (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Key)'Old);
function Find (Container : Set; Key : Key_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
- function Contains (Container : Set; Key : Key_Type) return Boolean with
- Global => null;
+ -- If Key is not contained in Container, Find returns No_Element
- end Generic_Keys;
+ ((for all E of Model (Container) =>
+ not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
+ Find'Result = No_Element,
- function Strict_Equal (Left, Right : Set) return Boolean with
- Ghost,
- Global => null;
- -- Strict_Equal returns True if the containers are physically equal, i.e.
- -- they are structurally equal (function "=" returns True) and that they
- -- have the same set of cursors.
+ -- Otherwise, Find returns a valid cursor in Container
- function First_To_Previous (Container : Set; Current : Cursor) return Set
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
- function Current_To_Last (Container : Set; Current : Cursor) return Set
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
- -- First_To_Previous returns a container containing all elements preceding
- -- Current (excluded) in Container. Current_To_Last returns a container
- -- containing all elements following Current (included) in Container.
- -- These two new functions can be used to express invariant properties in
- -- loops which iterate over containers. First_To_Previous returns the part
- -- of the container already scanned and Current_To_Last the part not
- -- scanned yet.
+ -- The key designated by the result of Find is Key
+
+ and
+ Equivalent_Keys
+ (Generic_Keys.Key (Container, Find'Result), Key));
+
+ function Contains (Container : Set; Key : Key_Type) return Boolean with
+ Global => null,
+ Post =>
+ Contains'Result =
+ (for some E of Model (Container) =>
+ Equivalent_Keys (Key, Generic_Keys.Key (E)));
+
+ end Generic_Keys;
private
pragma SPARK_Mode (Off);
use HT_Types;
- type Cursor is record
- Node : Count_Type;
- end record;
-
- No_Element : constant Cursor := (Node => 0);
-
Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
end Ada.Containers.Formal_Hashed_Sets;
package body Generic_Sorting with SPARK_Mode => Off is
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
+ begin
+ if M.Length (Container) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (Container, Index_Type'First);
+
+ begin
+ for I in Index_Type'First + 1 .. M.Last (Container) loop
+ declare
+ E2 : constant Element_Type := Element (Container, I);
+
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+
+ E1 := E2;
+ end;
+ end loop;
+ end;
+
+ return True;
+ end M_Elements_Sorted;
+
+ end Formal_Model;
+
---------------
-- Is_Sorted --
---------------
return True;
end Is_Sorted;
- -----------------------
- -- M_Elements_Sorted --
- -----------------------
-
- function M_Elements_Sorted (Container : M.Sequence) return Boolean is
- begin
- if M.Length (Container) = 0 then
- return True;
- end if;
-
- declare
- E1 : Element_Type := Element (Container, Index_Type'First);
-
- begin
- for I in Index_Type'First + 1 .. M.Last (Container) loop
- declare
- E2 : constant Element_Type := Element (Container, I);
-
- begin
- if E2 < E1 then
- return False;
- end if;
-
- E1 := E2;
- end;
- end loop;
- end;
-
- return True;
- end M_Elements_Sorted;
-
----------
-- Sort --
----------
Global => null,
Contract_Cases =>
- -- If Item is not is not contained in Container after Index, Find_Index
+ -- If Item is not contained in Container after Index, Find_Index
-- returns No_Index.
(Index > Last_Index (Container)
Global => null,
Contract_Cases =>
- -- If Item is not is not contained in Container before Index,
+ -- If Item is not contained in Container before Index,
-- Reverse_Find_Index returns No_Index.
(not M.Contains
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode is
- function M_Elements_Sorted (Container : M.Sequence) return Boolean with
- Ghost,
- Global => null,
- Post =>
- M_Elements_Sorted'Result =
- (for all I in Index_Type'First .. M.Last (Container) =>
- (for all J in I .. M.Last (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ package Formal_Model with Ghost is
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Elements_Sorted'Result =
+ (for all I in Index_Type'First .. M.Last (Container) =>
+ (for all J in I .. M.Last (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ end Formal_Model;
+ use Formal_Model;
function Is_Sorted (Container : Vector) return Boolean with
Global => null,
package body Formal_Model is
+ ----------
+ -- Find --
+ ----------
+
+ function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ is
+ begin
+ for I in 1 .. K.Length (Container) loop
+ if Equivalent_Keys (Key, K.Get (Container, I)) then
+ return I;
+ elsif Key < K.Get (Container, I) then
+ return 0;
+ end if;
+ end loop;
+ return 0;
+ end Find;
+
-------------------------
-- K_Bigger_Than_Range --
-------------------------
Key)));
pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find);
+ function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ -- Search for Key in Container
+
+ with
+ Global => null,
+ Post =>
+ (if Find'Result > 0 then
+ Find'Result <= K.Length (Container)
+ and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
Element_Type => Positive_Count_Type,
-- It contains all the keys contained in Model
- and
- (for all Key of Model (Container) =>
- (for some L of Keys'Result => Equivalent_Keys (L, Key)))
+ and (for all Key of Model (Container) =>
+ (Find (Keys'Result, Key) > 0
+ and then Equivalent_Keys
+ (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
-- It is sorted in increasing order
- and
- (for all I in 1 .. Length (Container) =>
- (for all J in 1 .. Length (Container) =>
- (K.Get (Keys'Result, I) < K.Get (Keys'Result, J)) =
- (I < J)));
+ and (for all I in 1 .. Length (Container) =>
+ Find (Keys'Result, K.Get (Keys'Result, I)) = I
+ and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with
-- Key now maps to New_Item
- and Formal_Ordered_Maps.Key (Container, Find (Container, Key)) = Key
+ and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
and Element (Model (Container), Key) = New_Item
-- Other mappings are preserved
(Left => Keys (Container)'Old,
Right => Keys (Container),
Fst => 1,
- Lst =>
- P.Get (Positions (Container), Find (Container, Key)) - 1)
+ Lst => Find (Keys (Container), Key) - 1)
-- Other keys are shifted by 1
and K.Range_Shifted
(Left => Keys (Container)'Old,
Right => Keys (Container),
- Fst => P.Get (Positions (Container), Find (Container, Key)),
+ Fst => Find (Keys (Container), Key),
Lst => Length (Container)'Old,
Offset => 1)
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
- Cut => P.Get (Positions (Container), Find (Container, Key)));
+ Cut => Find (Keys (Container), Key));
procedure Include
(Container : in out Map;
-- The key equivalent to Key in Container is replaced by Key
and K.Get
- (Keys (Container),
- P.Get (Positions (Container), Find (Container, Key))) = Key
+ (Keys (Container), Find (Keys (Container), Key)) = Key
and K.Equal_Except
(Keys (Container)'Old,
Keys (Container),
- P.Get (Positions (Container), Find (Container, Key)))
+ Find (Keys (Container), Key))
-- Elements associated with other keys are preserved
-- Key is inserted in Container
and K.Get
- (Keys (Container),
- P.Get (Positions (Container), Find (Container, Key))) = Key
+ (Keys (Container), Find (Keys (Container), Key)) = Key
-- The keys of Container located before Key are preserved
(Left => Keys (Container)'Old,
Right => Keys (Container),
Fst => 1,
- Lst =>
- P.Get (Positions (Container), Find (Container, Key)) - 1)
+ Lst => Find (Keys (Container), Key) - 1)
-- Other keys are shifted by 1
and K.Range_Shifted
(Left => Keys (Container)'Old,
Right => Keys (Container),
- Fst =>
- P.Get (Positions (Container), Find (Container, Key)),
+ Fst => Find (Keys (Container), Key),
Lst => Length (Container)'Old,
Offset => 1)
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
- Cut =>
- P.Get (Positions (Container), Find (Container, Key))));
+ Cut => Find (Keys (Container), Key)));
procedure Replace
(Container : in out Map;
with
Global => null,
Pre => Contains (Container, Key),
- Post =>
+ Post =>
-- Cursors are preserved
-- The key equivalent to Key in Container is replaced by Key
- and K.Get (Keys (Container),
- P.Get (Positions (Container), Find (Container, Key))) = Key
+ and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
and K.Equal_Except
(Keys (Container)'Old,
Keys (Container),
- P.Get (Positions (Container), Find (Container, Key)))
+ Find (Keys (Container), Key))
-- New_Item is now associated with the Key in Container
(Left => Keys (Container)'Old,
Right => Keys (Container),
Fst => 1,
- Lst =>
- P.Get (Positions (Container), Find (Container, Key))'Old
- - 1)
+ Lst => Find (Keys (Container), Key)'Old - 1)
-- The keys located after Key are shifted by 1
and K.Range_Shifted
(Left => Keys (Container),
Right => Keys (Container)'Old,
- Fst =>
- P.Get (Positions (Container), Find (Container, Key))'Old,
+ Fst => Find (Keys (Container), Key)'Old,
Lst => Length (Container),
Offset => 1)
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
- Cut =>
- P.Get
- (Positions (Container), Find (Container, Key))'Old));
+ Cut => Find (Keys (Container), Key)'Old));
procedure Delete (Container : in out Map; Key : Key_Type) with
Global => null,
(Left => Keys (Container)'Old,
Right => Keys (Container),
Fst => 1,
- Lst =>
- P.Get (Positions (Container), Find (Container, Key))'Old - 1)
+ Lst => Find (Keys (Container), Key)'Old - 1)
-- The keys located after Key are shifted by 1
and K.Range_Shifted
(Left => Keys (Container),
Right => Keys (Container)'Old,
- Fst =>
- P.Get (Positions (Container), Find (Container, Key))'Old,
+ Fst => Find (Keys (Container), Key)'Old,
Lst => Length (Container),
Offset => 1)
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
- Cut =>
- P.Get (Positions (Container), Find (Container, Key))'Old);
+ Cut => Find (Keys (Container), Key)'Old);
procedure Delete (Container : in out Map; Position : in out Cursor) with
Global => null,
Global => null,
Contract_Cases =>
- -- If Key is not is not contained in Container, Find returns No_Element
+ -- If Key is not contained in Container, Find returns No_Element
(not Contains (Model (Container), Key) =>
not P.Has_Key (Positions (Container), Find'Result)
and Find'Result = No_Element,
- -- Otherwise, Find returns a valid cusror in Container
+ -- Otherwise, Find returns a valid cursor in Container
others =>
P.Has_Key (Positions (Container), Find'Result)
+ and P.Get (Positions (Container), Find'Result) =
+ Find (Keys (Container), Key)
-- The key designated by the result of Find is Key
and Equivalent_Keys
- (Formal_Ordered_Maps.Key (Container, Find'Result), Key)
-
- -- Keys of Container are ordered
-
- and K_Is_Find
- (Keys (Container),
- Key,
- P.Get (Positions (Container),
- Find'Result)));
+ (Formal_Ordered_Maps.Key (Container, Find'Result), Key));
function Element (Container : Map; Key : Key_Type) return Element_Type with
Global => null,
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
return Target;
end Copy;
- ---------------------
- -- Current_To_Last --
- ---------------------
-
- function Current_To_Last (Container : Set; Current : Cursor) return Set is
- Curs : Cursor := First (Container);
- C : Set (Container.Capacity) := Copy (Container, Container.Capacity);
- Node : Count_Type;
-
- begin
- if Curs = No_Element then
- Clear (C);
- return C;
- end if;
-
- if Current /= No_Element and not Has_Element (Container, Current) then
- raise Constraint_Error;
- end if;
-
- while Curs.Node /= Current.Node loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
- end loop;
-
- return C;
- end Current_To_Last;
-
------------
-- Delete --
------------
end;
end First_Element;
- -----------------------
- -- First_To_Previous --
- -----------------------
-
- function First_To_Previous
- (Container : Set;
- Current : Cursor) return Set
- is
- Curs : Cursor := Current;
- C : Set (Container.Capacity) := Copy (Container, Container.Capacity);
- Node : Count_Type;
-
- begin
- if Curs = No_Element then
- return C;
-
- elsif not Has_Element (Container, Curs) then
- raise Constraint_Error;
-
- else
- while Curs.Node /= 0 loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
- end loop;
-
- return C;
- end if;
- end First_To_Previous;
-
-----------
-- Floor --
-----------
end;
end Floor;
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -------------------------
+ -- E_Bigger_Than_Range --
+ -------------------------
+
+ function E_Bigger_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Item : Element_Type) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if not (E.Get (Container, I) < Item) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end E_Bigger_Than_Range;
+
+ -------------------------
+ -- E_Elements_Included --
+ -------------------------
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Left) loop
+ if not E.Contains (Right, 1, E.Length (Right), E.Get (Left, I))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end E_Elements_Included;
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Model : M.Set;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Left) loop
+ declare
+ Item : constant Element_Type := E.Get (Left, I);
+ begin
+ if M.Contains (Model, Item) then
+ if not E.Contains (Right, 1, E.Length (Right), Item) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end E_Elements_Included;
+
+ function E_Elements_Included
+ (Container : E.Sequence;
+ Model : M.Set;
+ Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ is
+ begin
+ for I in 1 .. E.Length (Container) loop
+ declare
+ Item : constant Element_Type := E.Get (Container, I);
+ begin
+ if M.Contains (Model, Item) then
+ if not E.Contains (Left, 1, E.Length (Left), Item) then
+ return False;
+ end if;
+ else
+ if not E.Contains (Right, 1, E.Length (Right), Item) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end E_Elements_Included;
+
+ ---------------
+ -- E_Is_Find --
+ ---------------
+
+ function E_Is_Find
+ (Container : E.Sequence;
+ Item : Element_Type;
+ Position : Count_Type) return Boolean
+ is
+ begin
+ for I in 1 .. Position - 1 loop
+ if Item < E.Get (Container, I) then
+ return False;
+ end if;
+ end loop;
+
+ if Position < E.Length (Container) then
+ for I in Position + 1 .. E.Length (Container) loop
+ if E.Get (Container, I) < Item then
+ return False;
+ end if;
+ end loop;
+ end if;
+ return True;
+ end E_Is_Find;
+
+ --------------------------
+ -- E_Smaller_Than_Range --
+ --------------------------
+
+ function E_Smaller_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Item : Element_Type) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if not (Item < E.Get (Container, I)) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end E_Smaller_Than_Range;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : E.Sequence;
+ Item : Element_Type) return Count_Type
+ is
+ begin
+ for I in 1 .. E.Length (Container) loop
+ if Equivalent_Elements (Item, E.Get (Container, I)) then
+ return I;
+ end if;
+ end loop;
+ return 0;
+ end Find;
+
+ --------------
+ -- Elements --
+ --------------
+
+ function Elements (Container : Set) return E.Sequence is
+ Position : Count_Type := Container.First;
+ R : E.Sequence;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := E.Add (R, Container.Nodes (Position).Element);
+ Position := Tree_Operations.Next (Container, Position);
+ end loop;
+
+ return R;
+ end Elements;
+
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
+
+ procedure Lift_Abstraction_Level (Container : Set) is null;
+
+ -----------------------
+ -- Mapping_Preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > E.Length (E_Left)
+ or else P.Get (P_Right, C) > E.Length (E_Right)
+ or else E.Get (E_Left, P.Get (P_Left, C)) /=
+ E.Get (E_Right, P.Get (P_Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved;
+
+ ------------------------------
+ -- Mapping_Preserved_Except --
+ ------------------------------
+
+ function Mapping_Preserved_Except
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map;
+ Position : Cursor) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if C /= Position
+ and (not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > E.Length (E_Left)
+ or else P.Get (P_Right, C) > E.Length (E_Right)
+ or else E.Get (E_Left, P.Get (P_Left, C)) /=
+ E.Get (E_Right, P.Get (P_Right, C)))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved_Except;
+
+ -------------------------
+ -- P_Positions_Shifted --
+ -------------------------
+
+ function P_Positions_Shifted
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ is
+ begin
+ for Cu of Small loop
+ if not P.Has_Key (Big, Cu) then
+ return False;
+ end if;
+ end loop;
+
+ for Cu of Big loop
+ declare
+ Pos : constant Positive_Count_Type := P.Get (Big, Cu);
+
+ begin
+ if Pos < Cut then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu)
+ then
+ return False;
+ end if;
+
+ elsif Pos >= Cut + Count then
+ if not P.Has_Key (Small, Cu)
+ or else Pos /= P.Get (Small, Cu) + Count
+ then
+ return False;
+ end if;
+
+ else
+ if P.Has_Key (Small, Cu) then
+ return False;
+ end if;
+ end if;
+ end;
+ end loop;
+
+ return True;
+ end P_Positions_Shifted;
+
+ -----------
+ -- Model --
+ -----------
+
+ function Model (Container : Set) return M.Set is
+ Position : Count_Type := Container.First;
+ R : M.Set;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R :=
+ M.Add
+ (Container => R,
+ Item => Container.Nodes (Position).Element);
+
+ Position := Tree_Operations.Next (Container, Position);
+ end loop;
+
+ return R;
+ end Model;
+
+ ---------------
+ -- Positions --
+ ---------------
+
+ function Positions (Container : Set) return P.Map is
+ I : Count_Type := 1;
+ Position : Count_Type := Container.First;
+ R : P.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := P.Add (R, (Node => Position), I);
+ pragma Assert (P.Length (R) = I);
+ Position := Tree_Operations.Next (Container, Position);
+ I := I + 1;
+ end loop;
+
+ return R;
+ end Positions;
+
+ end Formal_Model;
+
----------
-- Free --
----------
return (if Node = 0 then No_Element else (Node => Node));
end Floor;
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -------------------------
+ -- E_Bigger_Than_Range --
+ -------------------------
+
+ function E_Bigger_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Key : Key_Type) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if not (Generic_Keys.Key (E.Get (Container, I)) < Key) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end E_Bigger_Than_Range;
+
+ ---------------
+ -- E_Is_Find --
+ ---------------
+
+ function E_Is_Find
+ (Container : E.Sequence;
+ Key : Key_Type;
+ Position : Count_Type) return Boolean
+ is
+ begin
+ for I in 1 .. Position - 1 loop
+ if Key < Generic_Keys.Key (E.Get (Container, I)) then
+ return False;
+ end if;
+ end loop;
+
+ if Position < E.Length (Container) then
+ for I in Position + 1 .. E.Length (Container) loop
+ if Generic_Keys.Key (E.Get (Container, I)) < Key then
+ return False;
+ end if;
+ end loop;
+ end if;
+ return True;
+ end E_Is_Find;
+
+ --------------------------
+ -- E_Smaller_Than_Range --
+ --------------------------
+
+ function E_Smaller_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Key : Key_Type) return Boolean
+ is
+ begin
+ for I in Fst .. Lst loop
+ if not (Key < Generic_Keys.Key (E.Get (Container, I))) then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end E_Smaller_Than_Range;
+
+ ----------
+ -- Find --
+ ----------
+
+ function Find
+ (Container : E.Sequence;
+ Key : Key_Type) return Count_Type
+ is
+ begin
+ for I in 1 .. E.Length (Container) loop
+ if Equivalent_Keys
+ (Key, Generic_Keys.Key (E.Get (Container, I)))
+ then
+ return I;
+ end if;
+ end loop;
+ return 0;
+ end Find;
+
+ -----------------------
+ -- M_Included_Except --
+ -----------------------
+
+ function M_Included_Except
+ (Left : M.Set;
+ Right : M.Set;
+ Key : Key_Type) return Boolean
+ is
+ begin
+ for E of Left loop
+ if not Contains (Right, E)
+ and not Equivalent_Keys (Generic_Keys.Key (E), Key)
+ then
+ return False;
+ end if;
+ end loop;
+ return True;
+ end M_Included_Except;
+ end Formal_Model;
+
-------------------------
-- Is_Greater_Key_Node --
-------------------------
Node.Right := Right;
end Set_Right;
- ------------------
- -- Strict_Equal --
- ------------------
-
- function Strict_Equal (Left, Right : Set) return Boolean is
- LNode : Count_Type := First (Left).Node;
- RNode : Count_Type := First (Right).Node;
-
- begin
- if Length (Left) /= Length (Right) then
- return False;
- end if;
-
- while LNode = RNode loop
- if LNode = 0 then
- return True;
- end if;
-
- if Left.Nodes (LNode).Element /= Right.Nodes (RNode).Element then
- exit;
- end if;
-
- LNode := Next (Left, LNode);
- RNode := Next (Right, RNode);
- end loop;
-
- return False;
- end Strict_Equal;
-
--------------------------
-- Symmetric_Difference --
--------------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2017, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- container. The operators "<" and ">" that could not be modified that way
-- have been removed.
--- There are three new functions:
-
--- function Strict_Equal (Left, Right : Set) return Boolean;
--- function First_To_Previous (Container : Set; Current : Cursor)
--- return Set;
--- function Current_To_Last (Container : Set; Current : Cursor)
--- return Set;
-
--- See detailed specifications for these subprograms
-
+with Ada.Containers.Functional_Maps;
+with Ada.Containers.Functional_Sets;
+with Ada.Containers.Functional_Vectors;
private with Ada.Containers.Red_Black_Trees;
generic
type Element_Type is private;
with function "<" (Left, Right : Element_Type) return Boolean is <>;
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Ordered_Sets with
- Pure,
SPARK_Mode
is
- pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis);
function Equivalent_Elements (Left, Right : Element_Type) return Boolean
with
- Global => null;
+ Global => null,
+ Post =>
+ Equivalent_Elements'Result =
+ (not (Left < Right) and not (Right < Left));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements);
type Set (Capacity : Count_Type) is private with
Iterable => (First => First,
Default_Initial_Condition => Is_Empty (Set);
pragma Preelaborable_Initialization (Set);
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
+ type Cursor is record
+ Node : Count_Type;
+ end record;
- Empty_Set : constant Set;
+ No_Element : constant Cursor := (Node => 0);
+
+ function Length (Container : Set) return Count_Type with
+ Global => null,
+ Post => Length'Result <= Container.Capacity;
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ package Formal_Model with Ghost is
+ subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+ package M is new Ada.Containers.Functional_Sets
+ (Element_Type => Element_Type,
+ Equivalent_Elements => Equivalent_Elements);
+
+ function "="
+ (Left : M.Set;
+ Right : M.Set) return Boolean renames M."=";
+
+ function "<="
+ (Left : M.Set;
+ Right : M.Set) return Boolean renames M."<=";
+
+ package E is new Ada.Containers.Functional_Vectors
+ (Element_Type => Element_Type,
+ Index_Type => Positive_Count_Type);
+
+ function "="
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."=";
+
+ function "<"
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."<";
+
+ function "<="
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean renames E."<=";
+
+ function E_Bigger_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Item : Element_Type) return Boolean
+ with
+ Global => null,
+ Pre => Lst <= E.Length (Container),
+ Post =>
+ E_Bigger_Than_Range'Result =
+ (for all I in Fst .. Lst => E.Get (Container, I) < Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
+
+ function E_Smaller_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Item : Element_Type) return Boolean
+ with
+ Global => null,
+ Pre => Lst <= E.Length (Container),
+ Post =>
+ E_Smaller_Than_Range'Result =
+ (for all I in Fst .. Lst => Item < E.Get (Container, I));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
+
+ function E_Is_Find
+ (Container : E.Sequence;
+ Item : Element_Type;
+ Position : Count_Type) return Boolean
+ with
+ Global => null,
+ Pre => Position - 1 <= E.Length (Container),
+ Post =>
+ E_Is_Find'Result =
+
+ ((if Position > 0 then
+ E_Bigger_Than_Range (Container, 1, Position - 1, Item))
+
+ and (if Position < E.Length (Container) then
+ E_Smaller_Than_Range
+ (Container,
+ Position + 1,
+ E.Length (Container),
+ Item)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
+
+ function Find
+ (Container : E.Sequence;
+ Item : Element_Type) return Count_Type
+ -- Search for Item in Container
+
+ with
+ Global => null,
+ Post =>
+ (if Find'Result > 0 then
+ Find'Result <= E.Length (Container)
+ and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ -- The elements of Left are contained in Right
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Left) =>
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ function E_Elements_Included
+ (Left : E.Sequence;
+ Model : M.Set;
+ Right : E.Sequence) return Boolean
+ -- The elements of Container contained in Model are in Right
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Left) =>
+ (if M.Contains (Model, E.Get (Left, I)) then
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ function E_Elements_Included
+ (Container : E.Sequence;
+ Model : M.Set;
+ Left : E.Sequence;
+ Right : E.Sequence) return Boolean
+ -- The elements of Container contained in Model are in Left and others
+ -- are in Right.
+
+ with
+ Global => null,
+ Post =>
+ E_Elements_Included'Result =
+ (for all I in 1 .. E.Length (Container) =>
+ (if M.Contains (Model, E.Get (Container, I)) then
+ Find (Left, E.Get (Container, I)) > 0
+ and then E.Get (Left, Find (Left, E.Get (Container, I))) =
+ E.Get (Container, I)
+ else
+ Find (Right, E.Get (Container, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Container, I))) =
+ E.Get (Container, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
+
+ package P is new Ada.Containers.Functional_Maps
+ (Key_Type => Cursor,
+ Element_Type => Positive_Count_Type,
+ Equivalent_Keys => "=",
+ Enable_Handling_Of_Equivalence => False);
+
+ function "="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."=";
+
+ function "<="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."<=";
+
+ function P_Positions_Shifted
+ (Small : P.Map;
+ Big : P.Map;
+ Cut : Positive_Count_Type;
+ Count : Count_Type := 1) return Boolean
+ with
+ Global => null,
+ Post =>
+ P_Positions_Shifted'Result =
+
+ -- Big contains all cursors of Small
+
+ (P.Keys_Included (Small, Big)
+
+ -- Cursors located before Cut are not moved, cursors located
+ -- after are shifted by Count.
+
+ and (for all I of Small =>
+ (if P.Get (Small, I) < Cut then
+ P.Get (Big, I) = P.Get (Small, I)
+ else
+ P.Get (Big, I) - Count = P.Get (Small, I)))
+
+ -- New cursors of Big (if any) are between Cut and Cut - 1 +
+ -- Count.
+
+ and (for all I of Big =>
+ P.Has_Key (Small, I)
+ or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
+
+ function Mapping_Preserved
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved'Result then
+
+ -- Right contains all the cursors of Left
+
+ P.Keys_Included (P_Left, P_Right)
+
+ -- Right contains all the elements of Left
+
+ and E_Elements_Included (E_Left, E_Right)
+
+ -- Mappings from cursors to elements induced by E_Left, P_Left
+ -- and E_Right, P_Right are the same.
+
+ and (for all C of P_Left =>
+ E.Get (E_Left, P.Get (P_Left, C)) =
+ E.Get (E_Right, P.Get (P_Right, C))));
+
+ function Mapping_Preserved_Except
+ (E_Left : E.Sequence;
+ E_Right : E.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map;
+ Position : Cursor) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved_Except'Result then
+
+ -- Right contains all the cursors of Left
+
+ P.Keys_Included (P_Left, P_Right)
+
+ -- Mappings from cursors to elements induced by E_Left, P_Left
+ -- and E_Right, P_Right are the same except for Position.
+
+ and (for all C of P_Left =>
+ (if C /= Position then
+ E.Get (E_Left, P.Get (P_Left, C)) =
+ E.Get (E_Right, P.Get (P_Right, C)))));
+
+ function Model (Container : Set) return M.Set with
+ -- The high-level model of a set is a set of elements. Neither cursors
+ -- nor order of elements are represented in this model. Elements are
+ -- modeled up to equivalence.
+
+ Ghost,
+ Global => null,
+ Post => M.Length (Model'Result) = Length (Container);
+
+ function Elements (Container : Set) return E.Sequence with
+ -- The Elements sequence represents the underlying list structure of
+ -- sets that is used for iteration. It stores the actual values of
+ -- elements in the set. It does not model cursors.
+
+ Ghost,
+ Global => null,
+ Post =>
+ E.Length (Elements'Result) = Length (Container)
+
+ -- It only contains keys contained in Model
+
+ and (for all Item of Elements'Result =>
+ M.Contains (Model (Container), Item))
+
+ -- It contains all the elements contained in Model
+
+ and (for all Item of Model (Container) =>
+ (Find (Elements'Result, Item) > 0
+ and then Equivalent_Elements
+ (E.Get (Elements'Result, Find (Elements'Result, Item)),
+ Item)))
+
+ -- It is sorted in increasing order
+
+ and (for all I in 1 .. Length (Container) =>
+ Find (Elements'Result, E.Get (Elements'Result, I)) = I
+ and
+ E_Is_Find
+ (Elements'Result, E.Get (Elements'Result, I), I));
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
+
+ function Positions (Container : Set) return P.Map with
+ -- The Positions map is used to model cursors. It only contains valid
+ -- cursors and maps them to their position in the container.
+
+ Ghost,
+ Global => null,
+ Post =>
+ not P.Has_Key (Positions'Result, No_Element)
+
+ -- Positions of cursors are smaller than the container's length
+
+ and then
+ (for all I of Positions'Result =>
+ P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+ -- No two cursors have the same position. Note that we do not
+ -- state that there is a cursor in the map for each position, as
+ -- it is rarely needed.
+
+ and then
+ (for all J of Positions'Result =>
+ (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
+ then I = J)));
+
+ procedure Lift_Abstraction_Level (Container : Set) with
+ -- Lift_Abstraction_Level is a ghost procedure that does nothing but
+ -- assume that we can access the same elements by iterating over
+ -- positions or cursors.
+ -- This information is not generally useful except when switching from
+ -- a low-level, cursor-aware view of a container, to a high-level,
+ -- position-based view.
+
+ Ghost,
+ Global => null,
+ Post =>
+ (for all Item of Elements (Container) =>
+ (for some I of Positions (Container) =>
+ E.Get (Elements (Container), P.Get (Positions (Container), I)) =
+ Item));
+
+ function Contains
+ (C : M.Set;
+ K : Element_Type) return Boolean renames M.Contains;
+ -- To improve readability of contracts, we rename the function used to
+ -- search for an element in the model to Contains.
+
+ end Formal_Model;
+ use Formal_Model;
- No_Element : constant Cursor;
+ Empty_Set : constant Set;
function "=" (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+
+ -- If two sets are equal, they contain the same elements in the same
+ -- order.
+
+ (if "="'Result then Elements (Left) = Elements (Right)
+
+ -- If they are different, then they do not contain the same elements
+
+ else
+ not E_Elements_Included (Elements (Left), Elements (Right))
+ or not E_Elements_Included (Elements (Right), Elements (Left)));
function Equivalent_Sets (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
function To_Set (New_Item : Element_Type) return Set with
- Global => null;
-
- function Length (Container : Set) return Count_Type with
- Global => null;
+ Global => null,
+ Post =>
+ M.Is_Singleton (Model (To_Set'Result), New_Item)
+ and Length (To_Set'Result) = 1
+ and E.Get (Elements (To_Set'Result), 1) = New_Item;
function Is_Empty (Container : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Set) with
- Global => null;
+ Global => null,
+ Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
procedure Assign (Target : in out Set; Source : Set) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Model (Target) = Model (Source)
+ and Elements (Target) = Elements (Source)
+ and Length (Target) = Length (Source);
function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
Global => null,
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity,
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Elements (Copy'Result) = Elements (Source)
+ and Positions (Copy'Result) = Positions (Source)
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Source.Capacity
+ else
+ Copy'Result.Capacity = Capacity);
function Element
(Container : Set;
Position : Cursor) return Element_Type
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Element'Result =
+ E.Get (Elements (Container), P.Get (Positions (Container), Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Set;
New_Item : Element_Type)
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Position now maps to New_Item
+
+ and Element (Container, Position) = New_Item
+
+ -- New_Item is contained in Container
+
+ and Contains (Model (Container), New_Item)
+
+ -- Other elements are preserved
+
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Element (Container, Position)'Old)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved_Except
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container),
+ Position => Position)
+ and Positions (Container) = Positions (Container)'Old;
procedure Move (Target : in out Set; Source : in out Set) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Model (Target) = Model (Source)'Old
+ and Elements (Target) = Elements (Source)'Old
+ and Length (Source)'Old = Length (Target)
+ and Length (Source) = 0;
procedure Insert
(Container : in out Set;
Position : out Cursor;
Inserted : out Boolean)
with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity
+ or Contains (Container, New_Item),
+ Post =>
+ Contains (Container, New_Item)
+ and Has_Element (Container, Position)
+ and Equivalent_Elements (Element (Container, Position), New_Item)
+ and E_Is_Find
+ (Elements (Container),
+ New_Item,
+ P.Get (Positions (Container), Position)),
+ Contract_Cases =>
+
+ -- If New_Item is already in Container, it is not modified and Inserted
+ -- is set to False.
+
+ (Contains (Container, New_Item) =>
+ not Inserted
+ and Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, New_Item is inserted in Container and Inserted is set to
+ -- True
+
+ others =>
+ Inserted
+ and Length (Container) = Length (Container)'Old + 1
+
+ -- Position now maps to New_Item
+
+ and Element (Container, Position) = New_Item
+
+ -- Other elements are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- The elements of Container located before Position are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container), Position) - 1)
+
+ -- Other elements are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => P.Get (Positions (Container), Position),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- A new cursor has been inserted at position Position in
+ -- Container.
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => P.Get (Positions (Container), Position)));
procedure Insert
(Container : in out Set;
New_Item : Element_Type)
with
Global => null,
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, New_Item));
+ Pre =>
+ Length (Container) < Container.Capacity
+ and then (not Contains (Container, New_Item)),
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+ and Contains (Container, New_Item)
+
+ -- New_Item is inserted in the set
+
+ and E.Get (Elements (Container),
+ Find (Elements (Container), New_Item)) = New_Item
+
+ -- Other mappings are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- The elements of Container located before New_Item are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), New_Item) - 1)
+
+ -- Other elements are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => Find (Elements (Container), New_Item),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- A new cursor has been inserted in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Find (Elements (Container), New_Item));
procedure Include
(Container : in out Set;
New_Item : Element_Type)
with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity
+ or Contains (Container, New_Item),
+ Post => Contains (Container, New_Item),
+ Contract_Cases =>
+
+ -- If New_Item is already in Container
+
+ (Contains (Container, New_Item) =>
+
+ -- Elements are preserved
+
+ Model (Container)'Old = Model (Container)
+
+ -- Cursors are preserved
+
+ and Positions (Container) = Positions (Container)'Old
+
+ -- The element equivalent to New_Item in Container is replaced by
+ -- New_Item.
+
+ and E.Get (Elements (Container),
+ Find (Elements (Container), New_Item)) = New_Item
+
+ and E.Equal_Except
+ (Elements (Container)'Old,
+ Elements (Container),
+ Find (Elements (Container), New_Item)),
+
+ -- Otherwise, New_Item is inserted in Container
+
+ others =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Other elements are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- New_Item is inserted in Container
+
+ and E.Get (Elements (Container),
+ Find (Elements (Container), New_Item)) = New_Item
+
+ -- The Elements of Container located before New_Item are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), New_Item) - 1)
+
+ -- Other Elements are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => Find (Elements (Container), New_Item),
+ Lst => Length (Container)'Old,
+ Offset => 1)
+
+ -- A new cursor has been inserted in Container
+
+ and P_Positions_Shifted
+ (Positions (Container)'Old,
+ Positions (Container),
+ Cut => Find (Elements (Container), New_Item)));
procedure Replace
(Container : in out Set;
New_Item : Element_Type)
with
Global => null,
- Pre => Contains (Container, New_Item);
+ Pre => Contains (Container, New_Item),
+ Post =>
+
+ -- Elements are preserved
+
+ Model (Container)'Old = Model (Container)
+
+ -- Cursors are preserved
+
+ and Positions (Container) = Positions (Container)'Old
+
+ -- The element equivalent to New_Item in Container is replaced by
+ -- New_Item.
+
+ and E.Get (Elements (Container),
+ Find (Elements (Container), New_Item)) = New_Item
+ and E.Equal_Except
+ (Elements (Container)'Old,
+ Elements (Container),
+ Find (Elements (Container), New_Item));
procedure Exclude
(Container : in out Set;
Item : Element_Type)
with
- Global => null;
+ Global => null,
+ Post => not Contains (Container, Item),
+ Contract_Cases =>
+
+ -- If Item is not in Container, nothing is changed
+
+ (not Contains (Container, Item) =>
+ Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Item is removed from Container
+
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Item)
+
+ -- The elements of Container located before Item are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), Item)'Old - 1)
+
+ -- The elements located after Item are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => Find (Elements (Container), Item)'Old,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- A cursor has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Find (Elements (Container), Item)'Old));
procedure Delete
(Container : in out Set;
Item : Element_Type)
with
Global => null,
- Pre => Contains (Container, Item);
+ Pre => Contains (Container, Item),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Item is no longer in Container
+
+ and not Contains (Container, Item)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Item)
+
+ -- The elements of Container located before Item are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), Item)'Old - 1)
+
+ -- The elements located after Item are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => Find (Elements (Container), Item)'Old,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- A cursor has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Find (Elements (Container), Item)'Old);
procedure Delete
(Container : in out Set;
Position : in out Cursor)
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Position = No_Element
+ and Length (Container) = Length (Container)'Old - 1
+
+ -- The element at position Position is no longer in Container
+
+ and not Contains (Container, Element (Container, Position)'Old)
+ and not P.Has_Key (Positions (Container), Position'Old)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Element (Container, Position)'Old)
+
+ -- The elements of Container located before Position are preserved.
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
+
+ -- The elements located after Position are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => P.Get (Positions (Container)'Old, Position'Old),
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- Position has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => P.Get (Positions (Container)'Old, Position'Old));
procedure Delete_First (Container : in out Set) with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 => Length (Container) = 0,
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- The first element has been removed from Container
+
+ and not Contains (Container, First_Element (Container)'Old)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ First_Element (Container)'Old)
+
+ -- Other elements are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => 1,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- First has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => 1));
procedure Delete_Last (Container : in out Set) with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 => Length (Container) = 0,
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- The last element has been removed from Container
+
+ and not Contains (Container, Last_Element (Container)'Old)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Last_Element (Container)'Old)
+
+ -- Others elements of Container are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Length (Container))
+
+ -- Last cursor has been removed from Container
+
+ and Positions (Container) <= Positions (Container)'Old);
procedure Union (Target : in out Set; Source : Set) with
Global => null,
- Pre => Length (Target) + Length (Source) -
- Length (Intersection (Target, Source)) <= Target.Capacity;
+ Pre =>
+ Length (Source) - Length (Target and Source) <=
+ Target.Capacity - Length (Target),
+ Post =>
+ Length (Target) = Length (Target)'Old
+ - M.Num_Overlaps (Model (Target)'Old, Model (Source))
+ + Length (Source)
+
+ -- Elements already in Target are still in Target
+
+ and Model (Target)'Old <= Model (Target)
+
+ -- Elements of Source are included in Target
+
+ and Model (Source) <= Model (Target)
+
+ -- Elements of Target come from either Source or Target
+
+ and
+ M.Included_In_Union
+ (Model (Target), Model (Source), Model (Target)'Old)
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
+ and
+ E_Elements_Included
+ (Elements (Source),
+ Model (Target)'Old,
+ Elements (Source),
+ Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target)'Old,
+ E_Right => Elements (Target),
+ P_Left => Positions (Target)'Old,
+ P_Right => Positions (Target));
function Union (Left, Right : Set) return Set with
Global => null,
- Pre => Length (Left) + Length (Right) -
- Length (Intersection (Left, Right)) <= Count_Type'Last;
+ Pre => Length (Left) <= Count_Type'Last - Length (Right),
+ Post =>
+ Length (Union'Result) = Length (Left)
+ - M.Num_Overlaps (Model (Left), Model (Right))
+ + Length (Right)
+
+ -- Elements of Left and Right are in the result of Union
+
+ and Model (Left) <= Model (Union'Result)
+ and Model (Right) <= Model (Union'Result)
+
+ -- Elements of the result of union come from either Left or Right
+
+ and
+ M.Included_In_Union
+ (Model (Union'Result), Model (Left), Model (Right))
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Union'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+ and
+ E_Elements_Included
+ (Elements (Left), Model (Left), Elements (Union'Result))
+ and
+ E_Elements_Included
+ (Elements (Right),
+ Model (Left),
+ Elements (Right),
+ Elements (Union'Result));
function "or" (Left, Right : Set) return Set renames Union;
procedure Intersection (Target : in out Set; Source : Set) with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Target) =
+ M.Num_Overlaps (Model (Target)'Old, Model (Source))
+
+ -- Elements of Target were already in Target
+
+ and Model (Target) <= Model (Target)'Old
+
+ -- Elements of Target are in Source
+
+ and Model (Target) <= Model (Source)
+
+ -- Elements both in Source and Target are in the intersection
+
+ and
+ M.Includes_Intersection
+ (Model (Target), Model (Source), Model (Target)'Old)
+
+ -- Actual value of elements of Target is preserved
+
+ and E_Elements_Included (Elements (Target), Elements (Target)'Old)
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Source), Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target),
+ E_Right => Elements (Target)'Old,
+ P_Left => Positions (Target),
+ P_Right => Positions (Target)'Old);
function Intersection (Left, Right : Set) return Set with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Intersection'Result) =
+ M.Num_Overlaps (Model (Left), Model (Right))
+
+ -- Elements in the result of Intersection are in Left and Right
+
+ and Model (Intersection'Result) <= Model (Left)
+ and Model (Intersection'Result) <= Model (Right)
+
+ -- Elements both in Left and Right are in the result of Intersection
+
+ and
+ M.Includes_Intersection
+ (Model (Intersection'Result), Model (Left), Model (Right))
+
+ -- Actual value of elements come from Left
+
+ and
+ E_Elements_Included
+ (Elements (Intersection'Result), Elements (Left))
+ and
+ E_Elements_Included
+ (Elements (Left), Model (Right), Elements (Intersection'Result));
function "and" (Left, Right : Set) return Set renames Intersection;
procedure Difference (Target : in out Set; Source : Set) with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Target) = Length (Target)'Old -
+ M.Num_Overlaps (Model (Target)'Old, Model (Source))
+
+ -- Elements of Target were already in Target
+
+ and Model (Target) <= Model (Target)'Old
+
+ -- Elements of Target are not in Source
+
+ and M.No_Overlap (Model (Target), Model (Source))
+
+ -- Elements in Target but not in Source are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
+
+ -- Actual value of elements of Target is preserved
+
+ and E_Elements_Included (Elements (Target), Elements (Target)'Old)
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
+
+ -- Mapping from cursors of Target to elements is preserved
+
+ and Mapping_Preserved
+ (E_Left => Elements (Target),
+ E_Right => Elements (Target)'Old,
+ P_Left => Positions (Target),
+ P_Right => Positions (Target)'Old);
function Difference (Left, Right : Set) return Set with
- Global => null;
+ Global => null,
+ Post =>
+ Length (Difference'Result) = Length (Left) -
+ M.Num_Overlaps (Model (Left), Model (Right))
+
+ -- Elements of the result of Difference are in Left
+
+ and Model (Difference'Result) <= Model (Left)
+
+ -- Elements of the result of Difference are in Right
+
+ and M.No_Overlap (Model (Difference'Result), Model (Right))
+
+ -- Elements in Left but not in Right are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Left), Model (Difference'Result), Model (Right))
+
+ -- Actual value of elements come from Left
+
+ and
+ E_Elements_Included (Elements (Difference'Result), Elements (Left))
+ and
+ E_Elements_Included
+ (Elements (Left),
+ Model (Difference'Result),
+ Elements (Difference'Result));
function "-" (Left, Right : Set) return Set renames Difference;
procedure Symmetric_Difference (Target : in out Set; Source : Set) with
Global => null,
- Pre => Length (Target) + Length (Source) -
- 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
+ Pre =>
+ Length (Source) - Length (Target and Source) <=
+ Target.Capacity - Length (Target) + Length (Target and Source),
+ Post =>
+ Length (Target) = Length (Target)'Old -
+ 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
+ Length (Source)
+
+ -- Elements of the difference were not both in Source and in Target
+
+ and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
+
+ -- Elements in Target but not in Source are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
+
+ -- Elements in Source but not in Target are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Source), Model (Target), Model (Target)'Old)
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+ and
+ E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
+ and
+ E_Elements_Included
+ (Elements (Source), Model (Target), Elements (Target));
function Symmetric_Difference (Left, Right : Set) return Set with
Global => null,
- Pre => Length (Left) + Length (Right) -
- 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
-
- function "xor" (Left, Right : Set) return Set renames Symmetric_Difference;
+ Pre => Length (Left) <= Count_Type'Last - Length (Right),
+ Post =>
+ Length (Symmetric_Difference'Result) = Length (Left) -
+ 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
+ Length (Right)
+
+ -- Elements of the difference were not both in Left and Right
+
+ and
+ M.Not_In_Both
+ (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
+
+ -- Elements in Left but not in Right are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
+
+ -- Elements in Right but not in Left are in the difference
+
+ and
+ M.Included_In_Union
+ (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
+
+ -- Actual value of elements come from either Left or Right
+
+ and
+ E_Elements_Included
+ (Elements (Symmetric_Difference'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+ and
+ E_Elements_Included
+ (Elements (Left),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result))
+ and
+ E_Elements_Included
+ (Elements (Right),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result));
+
+ function "xor" (Left, Right : Set) return Set
+ renames Symmetric_Difference;
function Overlap (Left, Right : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+ Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
function First (Container : Set) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ First'Result = No_Element,
+
+ others =>
+ Has_Element (Container, First'Result)
+ and P.Get (Positions (Container), First'Result) = 1);
function First_Element (Container : Set) return Element_Type with
Global => null,
- Pre => not Is_Empty (Container);
-
- function Last (Container : Set) return Cursor;
+ Pre => not Is_Empty (Container),
+ Post =>
+ First_Element'Result = E.Get (Elements (Container), 1)
+ and E_Smaller_Than_Range
+ (Elements (Container),
+ 2,
+ Length (Container),
+ First_Element'Result);
+
+ function Last (Container : Set) return Cursor with
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ Last'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Last'Result)
+ and P.Get (Positions (Container), Last'Result) =
+ Length (Container));
function Last_Element (Container : Set) return Element_Type with
Global => null,
- Pre => not Is_Empty (Container);
+ Pre => not Is_Empty (Container),
+ Post =>
+ Last_Element'Result = E.Get (Elements (Container), Length (Container))
+ and E_Bigger_Than_Range
+ (Elements (Container),
+ 1,
+ Length (Container) - 1,
+ Last_Element'Result);
function Next (Container : Set; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Next'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Next'Result)
+ and then P.Get (Positions (Container), Next'Result) =
+ P.Get (Positions (Container), Position) + 1);
procedure Next (Container : Set; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) + 1);
function Previous (Container : Set; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = 1
+ =>
+ Previous'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Previous'Result)
+ and then P.Get (Positions (Container), Previous'Result) =
+ P.Get (Positions (Container), Position) - 1);
procedure Previous (Container : Set; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = 1
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) - 1);
function Find (Container : Set; Item : Element_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+
+ -- If Item is not contained in Container, Find returns No_Element
+
+ (not Contains (Model (Container), Item) =>
+ not P.Has_Key (Positions (Container), Find'Result)
+ and Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cursor in Container
+
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
+ and P.Get (Positions (Container), Find'Result) =
+ Find (Elements (Container), Item)
+
+ -- The element designated by the result of Find is Item
+
+ and Equivalent_Elements
+ (Element (Container, Find'Result), Item));
function Floor (Container : Set; Item : Element_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 or else Item < First_Element (Container) =>
+ Floor'Result = No_Element,
+ others =>
+ Has_Element (Container, Floor'Result)
+ and
+ not (Item < E.Get (Elements (Container),
+ P.Get (Positions (Container), Floor'Result)))
+ and E_Is_Find
+ (Elements (Container),
+ Item,
+ P.Get (Positions (Container), Floor'Result)));
function Ceiling (Container : Set; Item : Element_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 or else Last_Element (Container) < Item =>
+ Ceiling'Result = No_Element,
+ others =>
+ Has_Element (Container, Ceiling'Result)
+ and
+ not (E.Get (Elements (Container),
+ P.Get (Positions (Container), Ceiling'Result)) <
+ Item)
+ and E_Is_Find
+ (Elements (Container),
+ Item,
+ P.Get (Positions (Container), Ceiling'Result)));
function Contains (Container : Set; Item : Element_Type) return Boolean with
- Global => null;
+ Global => null,
+ Post => Contains'Result = Contains (Model (Container), Item);
+ pragma Annotate (GNATprove, Inline_For_Proof, Contains);
function Has_Element (Container : Set; Position : Cursor) return Boolean
with
- Global => null;
+ Global => null,
+ Post =>
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
+ pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
generic
type Key_Type (<>) is private;
package Generic_Keys with SPARK_Mode is
function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+ Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left));
+ pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys);
+
+ package Formal_Model with Ghost is
+ function E_Bigger_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Key : Key_Type) return Boolean
+ with
+ Global => null,
+ Pre => Lst <= E.Length (Container),
+ Post =>
+ E_Bigger_Than_Range'Result =
+ (for all I in Fst .. Lst =>
+ Generic_Keys.Key (E.Get (Container, I)) < Key);
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
+
+ function E_Smaller_Than_Range
+ (Container : E.Sequence;
+ Fst : Positive_Count_Type;
+ Lst : Count_Type;
+ Key : Key_Type) return Boolean
+ with
+ Global => null,
+ Pre => Lst <= E.Length (Container),
+ Post =>
+ E_Smaller_Than_Range'Result =
+ (for all I in Fst .. Lst =>
+ Key < Generic_Keys.Key (E.Get (Container, I)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
+
+ function E_Is_Find
+ (Container : E.Sequence;
+ Key : Key_Type;
+ Position : Count_Type) return Boolean
+ with
+ Global => null,
+ Pre => Position - 1 <= E.Length (Container),
+ Post =>
+ E_Is_Find'Result =
+
+ ((if Position > 0 then
+ E_Bigger_Than_Range (Container, 1, Position - 1, Key))
+
+ and (if Position < E.Length (Container) then
+ E_Smaller_Than_Range
+ (Container,
+ Position + 1,
+ E.Length (Container),
+ Key)));
+ pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
+
+ function Find
+ (Container : E.Sequence;
+ Key : Key_Type) return Count_Type
+ -- Search for Key in Container
+
+ with
+ Global => null,
+ Post =>
+ (if Find'Result > 0 then
+ Find'Result <= E.Length (Container)
+ and Equivalent_Keys
+ (Key, Generic_Keys.Key (E.Get (Container, Find'Result)))
+ and E_Is_Find (Container, Key, Find'Result));
+
+ function M_Included_Except
+ (Left : M.Set;
+ Right : M.Set;
+ Key : Key_Type) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Included_Except'Result =
+ (for all E of Left =>
+ Contains (Right, E)
+ or Equivalent_Keys (Generic_Keys.Key (E), Key));
+ end Formal_Model;
+ use Formal_Model;
function Key (Container : Set; Position : Cursor) return Key_Type with
- Global => null;
+ Global => null,
+ Post => Key'Result = Key (Element (Container, Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Key);
function Element (Container : Set; Key : Key_Type) return Element_Type
with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Element'Result = Element (Container, Find (Container, Key));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace
(Container : in out Set;
Key : Key_Type;
New_Item : Element_Type)
with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Length (Container) = Length (Container)'Old
+
+ -- Key now maps to New_Item
+
+ and Element (Container, Key) = New_Item
+
+ -- New_Item is contained in Container
+
+ and Contains (Model (Container), New_Item)
+
+ -- Other elements are preserved
+
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+ and M.Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ New_Item)
+
+ -- Mapping from cursors to elements is preserved
+
+ and Mapping_Preserved_Except
+ (E_Left => Elements (Container)'Old,
+ E_Right => Elements (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container),
+ Position => Find (Container, Key))
+ and Positions (Container) = Positions (Container)'Old;
procedure Exclude (Container : in out Set; Key : Key_Type) with
- Global => null;
+ Global => null,
+ Post => not Contains (Container, Key),
+ Contract_Cases =>
+
+ -- If Key is not in Container, nothing is changed
+
+ (not Contains (Container, Key) =>
+ Model (Container) = Model (Container)'Old
+ and Elements (Container) = Elements (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Key is removed from Container
+
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- The elements of Container located before Key are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), Key)'Old - 1)
+
+ -- The elements located after Key are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => Find (Elements (Container), Key)'Old,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- A cursor has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Find (Elements (Container), Key)'Old));
procedure Delete (Container : in out Set; Key : Key_Type) with
- Global => null;
+ Global => null,
+ Pre => Contains (Container, Key),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Key is no longer in Container
+
+ and not Contains (Container, Key)
+
+ -- Other elements are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- The elements of Container located before Key are preserved
+
+ and E.Range_Equal
+ (Left => Elements (Container)'Old,
+ Right => Elements (Container),
+ Fst => 1,
+ Lst => Find (Elements (Container), Key)'Old - 1)
+
+ -- The elements located after Key are shifted by 1
+
+ and E.Range_Shifted
+ (Left => Elements (Container),
+ Right => Elements (Container)'Old,
+ Fst => Find (Elements (Container), Key)'Old,
+ Lst => Length (Container),
+ Offset => 1)
+
+ -- A cursor has been removed from Container
+
+ and P_Positions_Shifted
+ (Positions (Container),
+ Positions (Container)'Old,
+ Cut => Find (Elements (Container), Key)'Old);
function Find (Container : Set; Key : Key_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+
+ -- If Key is not contained in Container, Find returns No_Element
+
+ ((for all E of Model (Container) =>
+ not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
+ not P.Has_Key (Positions (Container), Find'Result)
+ and Find'Result = No_Element,
+
+ -- Otherwise, Find returns a valid cursor in Container
+
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
+ and P.Get (Positions (Container), Find'Result) =
+ Find (Elements (Container), Key)
+
+ -- The element designated by the result of Find is Key
+
+ and Equivalent_Keys
+ (Generic_Keys.Key (Element (Container, Find'Result)), Key));
function Floor (Container : Set; Key : Key_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0
+ or else Key < Generic_Keys.Key (First_Element (Container)) =>
+ Floor'Result = No_Element,
+ others =>
+ Has_Element (Container, Floor'Result)
+ and
+ not (Key <
+ Generic_Keys.Key
+ (E.Get (Elements (Container),
+ P.Get (Positions (Container), Floor'Result))))
+ and E_Is_Find
+ (Elements (Container),
+ Key,
+ P.Get (Positions (Container), Floor'Result)));
function Ceiling (Container : Set; Key : Key_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0
+ or else Generic_Keys.Key (Last_Element (Container)) < Key =>
+ Ceiling'Result = No_Element,
+ others =>
+ Has_Element (Container, Ceiling'Result)
+ and
+ not (Generic_Keys.Key
+ (E.Get (Elements (Container),
+ P.Get (Positions (Container), Ceiling'Result)))
+ < Key)
+ and E_Is_Find
+ (Elements (Container),
+ Key,
+ P.Get (Positions (Container), Ceiling'Result)));
function Contains (Container : Set; Key : Key_Type) return Boolean with
- Global => null;
+ Global => null,
+ Post =>
+ Contains'Result =
+ (for some E of Model (Container) =>
+ Equivalent_Keys (Key, Generic_Keys.Key (E)));
end Generic_Keys;
- function Strict_Equal (Left, Right : Set) return Boolean with
- Ghost,
- Global => null;
- -- Strict_Equal returns True if the containers are physically equal, i.e.
- -- they are structurally equal (function "=" returns True) and that they
- -- have the same set of cursors.
-
- function First_To_Previous (Container : Set; Current : Cursor) return Set
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
-
- function Current_To_Last (Container : Set; Current : Cursor) return Set
- with
- Ghost,
- Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
- -- First_To_Previous returns a container containing all elements preceding
- -- Current (excluded) in Container. Current_To_Last returns a container
- -- containing all elements following Current (included) in Container.
- -- These two new functions can be used to express invariant properties in
- -- loops which iterate over containers. First_To_Previous returns the part
- -- of the container already scanned and Current_To_Last the part not
- -- scanned yet.
-
private
pragma SPARK_Mode (Off);
use Red_Black_Trees;
- type Cursor is record
- Node : Count_Type;
- end record;
-
- No_Element : constant Cursor := (Node => 0);
-
Empty_Set : constant Set := (Capacity => 0, others => <>);
end Ada.Containers.Formal_Ordered_Sets;
package body Generic_Sorting with SPARK_Mode => Off is
+ ------------------
+ -- Formal_Model --
+ ------------------
+
+ package body Formal_Model is
+
+ -----------------------
+ -- M_Elements_Sorted --
+ -----------------------
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean is
+ begin
+ if M.Length (Container) = 0 then
+ return True;
+ end if;
+
+ declare
+ E1 : Element_Type := Element (Container, Index_Type'First);
+
+ begin
+ for I in Index_Type'First + 1 .. M.Last (Container) loop
+ declare
+ E2 : constant Element_Type := Element (Container, I);
+
+ begin
+ if E2 < E1 then
+ return False;
+ end if;
+
+ E1 := E2;
+ end;
+ end loop;
+ end;
+
+ return True;
+ end M_Elements_Sorted;
+
+ end Formal_Model;
+
---------------
-- Is_Sorted --
---------------
return True;
end Is_Sorted;
- -----------------------
- -- M_Elements_Sorted --
- -----------------------
-
- function M_Elements_Sorted (Container : M.Sequence) return Boolean is
- begin
- if M.Length (Container) = 0 then
- return True;
- end if;
-
- declare
- E1 : Element_Type := Element (Container, Index_Type'First);
-
- begin
- for I in Index_Type'First + 1 .. M.Last (Container) loop
- declare
- E2 : constant Element_Type := Element (Container, I);
-
- begin
- if E2 < E1 then
- return False;
- end if;
-
- E1 := E2;
- end;
- end loop;
- end;
-
- return True;
- end M_Elements_Sorted;
-
----------
-- Sort --
----------
Global => null,
Contract_Cases =>
- -- If Item is not is not contained in Container after Index, Find_Index
+ -- If Item is not contained in Container after Index, Find_Index
-- returns No_Index.
(Index > Last_Index (Container)
Global => null,
Contract_Cases =>
- -- If Item is not is not contained in Container before Index,
+ -- If Item is not contained in Container before Index,
-- Reverse_Find_Index returns No_Index.
(not M.Contains
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode is
- function M_Elements_Sorted (Container : M.Sequence) return Boolean with
- Ghost,
- Global => null,
- Post =>
- M_Elements_Sorted'Result =
- (for all I in Index_Type'First .. M.Last (Container) =>
- (for all J in I .. M.Last (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
- pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ package Formal_Model with Ghost is
+
+ function M_Elements_Sorted (Container : M.Sequence) return Boolean
+ with
+ Global => null,
+ Post =>
+ M_Elements_Sorted'Result =
+ (for all I in Index_Type'First .. M.Last (Container) =>
+ (for all J in I .. M.Last (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
+ pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
+
+ end Formal_Model;
+ use Formal_Model;
function Is_Sorted (Container : Vector) return Boolean with
Global => null,
generic
type Key_Type (<>) is private;
type Element_Type (<>) is private;
- with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+ with function Equivalent_Keys
+ (Left : Key_Type;
+ Right : Key_Type) return Boolean is "=";
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
-- "For in" quantification over maps should not be used.
-- "For of" quantification over maps iterates over keys.
-- Note that, for proof, "for of" quantification is understood modulo
- -- equivalence (quantification includes keys equivalent to keys of the
- -- map).
+ -- equivalence (the range of quantification comprises all the keys that are
+ -- equivalent to any key of the map).
-----------------------
-- Basic operations --
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))));
+ (Equivalent_Keys (K, Key) =
+ (Witness (Container, Key) = Witness (Container, K)))));
function Length (Container : Map) return Count_Type with
Global => null;
function Is_Empty (Container : Set) return Boolean is
(Length (Container.Content) = 0);
+ ------------------
+ -- Is_Singleton --
+ ------------------
+
+ function Is_Singleton
+ (Container : Set;
+ New_Item : Element_Type) return Boolean
+ is
+ (Length (Container.Content) = 1
+ and New_Item = Get (Container.Content, 1));
+
------------
-- Length --
------------
function Length (Container : Set) return Count_Type is
(Length (Container.Content));
+ -----------------
+ -- Not_In_Both --
+ -----------------
+
+ function Not_In_Both
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
+ is
+ (for all Item of Container =>
+ not Contains (Right, Item) or not Contains (Left, Item));
+
+ ----------------
+ -- No_Overlap --
+ ----------------
+
+ function No_Overlap (Left : Set; Right : Set) return Boolean is
+ (Num_Overlaps (Left.Content, Right.Content) = 0);
+
------------------
-- Num_Overlaps --
------------------
type Element_Type (<>) is private;
with function Equivalent_Elements
(Left : Element_Type;
- Right : Element_Type) return Boolean;
+ Right : Element_Type) return Boolean is "=";
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
package Ada.Containers.Functional_Sets with SPARK_Mode is
type Set is private with
- Default_Initial_Condition => Is_Empty (Set) and Length (Set) = 0,
+ Default_Initial_Condition => Is_Empty (Set),
Iterable => (First => Iter_First,
Next => Iter_Next,
Has_Element => Iter_Has_Element,
-- "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).
+ -- equivalence (the range of quantification comprises all the elements that
+ -- are equivalent to any element of the set).
-----------------------
-- Basic operations --
-- Set inclusion
Global => null,
- Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
+ Post => "<="'Result = (for all Item of Left => Contains (Right, Item))
+ and (if "<="'Result then Length (Left) <= Length (Right));
function "=" (Left : Set; Right : Set) return Boolean with
-- Extensional equality over sets
Global => null,
- Post =>
- "="'Result =
- (for all Item of Left => Contains (Right, Item))
- and (for all Item of Right => Contains (Left, Item));
+ Post => "="'Result = (Left <= Right and Right <= Left);
pragma Warnings (Off, "unused variable ""Item""");
function Is_Empty (Container : Set) return Boolean with
-- A set is empty if it contains no element
Global => null,
- Post => Is_Empty'Result = (for all Item of Container => False);
+ Post =>
+ Is_Empty'Result = (for all Item of Container => False)
+ and Is_Empty'Result = (Length (Container) = 0);
pragma Warnings (On, "unused variable ""Item""");
function Included_Except
(for all Item of Container =>
Contains (Left, Item) or Contains (Right, Item));
+ function Is_Singleton
+ (Container : Set;
+ New_Item : Element_Type) return Boolean
+ with
+ -- Return True Container only contains New_Item
+
+ Global => null,
+ Post =>
+ Is_Singleton'Result =
+ (for all Item of Container => Equivalent_Elements (Item, New_Item));
+
+ function Not_In_Both
+ (Container : Set;
+ Left : Set;
+ Right : Set) return Boolean
+ -- Return True if there are no elements in Container that are in Left and
+ -- Right.
+
+ with
+ Global => null,
+ Post =>
+ Not_In_Both'Result =
+ (for all Item of Container =>
+ not Contains (Left, Item) or not Contains (Right, Item));
+
+ function No_Overlap (Left : Set; Right : Set) return Boolean with
+ -- Return True if there are no equivalent elements in Left and Right
+
+ Global => null,
+ Post =>
+ No_Overlap'Result =
+ (for all Item of Left => not Contains (Right, Item));
+
function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
-- Number of elements that are both in Left and Right
Global => null,
Post =>
- Num_Overlaps'Result <= Length (Left)
- and Num_Overlaps'Result <= Length (Right)
- and (if Num_Overlaps'Result = 0 then
- (for all Item of Left => not Contains (Right, Item)));
+ Num_Overlaps'Result = Length (Intersection (Left, Right));
----------------------------
-- Construction Functions --
Global => null,
Post =>
- Length (Intersection'Result) = Num_Overlaps (Left, Right)
- and Intersection'Result <= Left
+ Intersection'Result <= Left
and Intersection'Result <= Right
and Includes_Intersection (Intersection'Result, Left, Right);
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+ function "="
+ (Left : Element_Type;
+ Right : Element_Type) return Boolean renames Equivalent_Elements;
+
package Containers is new Ada.Containers.Functional_Base
- (Element_Type => Element_Type,
- Index_Type => Positive_Count_Type);
+ (Element_Type => Element_Type,
+ Index_Type => Positive_Count_Type);
type Set is record
Content : Containers.Container;
with Debug; use Debug;
with Einfo; use Einfo;
with Erroutc; use Erroutc;
-with Fname; use Fname;
with Gnatvsn; use Gnatvsn;
with Lib; use Lib;
with Opt; use Opt;
-- Types in other language defined units are displayed as
-- "package-name.type-name"
- elsif
- Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Ent)))
- then
+ elsif Is_Predefined_Unit (Get_Source_Unit (Ent)) then
Get_Unqualified_Decoded_Name_String
(Unit_Name (Get_Source_Unit (Ent)));
Name_Len := Name_Len - 2;
if Sloc (Error_Msg_Node_1) > Standard_Location
and then
- not Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Error_Msg_Node_1)))
+ not Is_Predefined_Unit (Get_Source_Unit (Error_Msg_Node_1))
then
Get_Name_String (Unit_File_Name (Get_Source_Unit (Error_Msg_Node_1)));
Set_Msg_Str (" defined");
with Exp_Ch9; use Exp_Ch9;
with Exp_Disp; use Exp_Disp;
with Exp_Tss; use Exp_Tss;
-with Fname; use Fname;
with Freeze; use Freeze;
with Itypes; use Itypes;
with Lib; use Lib;
and then
Is_Preelaborated (Spec_Entity (P)))
or else
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (P)))
+ Is_Predefined_Unit (Get_Source_Unit (P))
then
null;
with Exp_Strm; use Exp_Strm;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Freeze; use Freeze;
with Gnatvsn; use Gnatvsn;
with Itypes; use Itypes;
-- instead. That is why we include the test Is_Available when dealing
-- with these cases.
- if not Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit)) then
+ if not Is_Predefined_Unit (Current_Sem_Unit) then
-- Storage_Array as defined in package System.Storage_Elements
if Is_RTE (Base_Typ, RE_Storage_Array) then
-- --
-- B o d y --
-- --
--- Copyright (C) 1996-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 1996-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Atree; use Atree;
with Einfo; use Einfo;
with Errout; use Errout;
-with Fname; use Fname;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
-- referenced entity is in a runtime routine.
if Is_Entity_Name (N)
- and then
- Is_Predefined_File_Name (Unit_File_Name
- (Get_Source_Unit (Entity (N))))
+ and then Is_Predefined_Unit (Get_Source_Unit (Entity (N)))
then
return;
-- If the entity is an overridden primitive and we are not in
-- GNATprove mode, we must build a wrapper for the current
- -- inherited operation.
-
- if Is_Subprogram (New_E) and then not GNATprove_Mode then
+ -- inherited operation. If the reference is the prefix of an
+ -- attribute such as 'Result (or others ???) there is no need
+ -- for a wrapper: the condition is just rewritten in terms of
+ -- the inherited subprogram.
+
+ if Is_Subprogram (New_E)
+ and then Nkind (Parent (N)) /= N_Attribute_Reference
+ and then not GNATprove_Mode
+ then
Needs_Wrapper := True;
end if;
end if;
* *
* C Header File *
* *
- * Copyright (C) 1992-2016, Free Software Foundation, Inc. *
+ * Copyright (C) 1992-2017, Free Software Foundation, Inc. *
* *
* GNAT is free software; you can redistribute it and/or modify it under *
* terms of the GNU General Public License as published by the Free Soft- *
extern void Check_Implicit_Dynamic_Code_Allowed (Node_Id);
/* sem_aggr: */
+
#define Is_Others_Aggregate sem_aggr__is_others_aggregate
extern Boolean Is_Others_Aggregate (Node_Id);
extern Boolean Stack_Check_Probes_On_Target;
extern Boolean Stack_Check_Limits_On_Target;
+/* warnsw: */
+
+#define Warn_On_Questionable_Layout warnsw__warn_on_questionable_layout
+
+extern Boolean Warn_On_Questionable_Layout;
+
#ifdef __cplusplus
}
#endif
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
return False;
end Has_Prefix;
- ---------------------------
- -- Is_Internal_File_Name --
- ---------------------------
+ -----------------------
+ -- Is_GNAT_File_Name --
+ -----------------------
- function Is_Internal_File_Name
- (Fname : String;
- Renamings_Included : Boolean := True) return Boolean
- is
+ function Is_GNAT_File_Name (Fname : String) return Boolean is
begin
- if Is_Predefined_File_Name (Fname, Renamings_Included) then
- return True;
- end if;
-
- -- Check for internal extensions first, so we don't think (e.g.)
- -- "gnat.adc" is internal.
+ -- Check for internal extensions before checking prefixes, so we don't
+ -- think (e.g.) "gnat.adc" is internal.
if not Has_Internal_Extension (Fname) then
return False;
-- See the note in Is_Predefined_File_Name for the rationale
return Fname'Length = 8 and then Has_Prefix (Fname, "gnat");
+ end Is_GNAT_File_Name;
+
+ function Is_GNAT_File_Name (Fname : File_Name_Type) return Boolean is
+ Result : constant Boolean :=
+ Is_GNAT_File_Name (Get_Name_String (Fname));
+ begin
+ return Result;
+ end Is_GNAT_File_Name;
+
+ ---------------------------
+ -- Is_Internal_File_Name --
+ ---------------------------
+
+ function Is_Internal_File_Name
+ (Fname : String;
+ Renamings_Included : Boolean := True) return Boolean
+ is
+ begin
+ if Is_Predefined_File_Name (Fname, Renamings_Included) then
+ return True;
+ end if;
+
+ return Is_GNAT_File_Name (Fname);
end Is_Internal_File_Name;
function Is_Internal_File_Name
(Fname : String;
Renamings_Included : Boolean := True) return Boolean
is
- subtype Str8 is String (1 .. 8);
-
- Renaming_Names : constant array (1 .. 8) of Str8 :=
- ("calendar", -- Calendar
- "machcode", -- Machine_Code
- "unchconv", -- Unchecked_Conversion
- "unchdeal", -- Unchecked_Deallocation
- "directio", -- Direct_IO
- "ioexcept", -- IO_Exceptions
- "sequenio", -- Sequential_IO
- "text_io."); -- Text_IO
+ begin
+ -- Definitely false if longer than 12 characters (8.3)
- -- Note: the implementation is optimized to perform uniform comparisons
- -- on string slices whose length is known at compile time and is a small
- -- power of 2 (at most 8 characters); the remaining calls to Has_Prefix
- -- must be inlined to expose the compile-time known length. There must
- -- be no calls to the fallback string comparison routine (e.g. memcmp)
- -- left in the object code for the function; this can save up to 10% of
- -- the entire compilation time spent in the front end.
+ if Fname'Length > 12 then
+ return False;
+ end if;
- begin
if not Has_Internal_Extension (Fname) then
return False;
end if;
end;
end if;
- -- Definitely false if longer than 12 characters (8.3)
-
- if Fname'Length > 12 then
- return False;
- end if;
-
-- We include the "." in the prefixes below, so we don't match (e.g.)
-- adamant.ads. So the first line matches "ada.ads", "ada.adb", and
-- "ada.ali". But that's not necessary if they have 8 characters.
-- If instructed and the name has 8+ characters, check for renamings
- if Renamings_Included and then Fname'Length >= 8 then
+ if Renamings_Included
+ and then Is_Predefined_Renaming_File_Name (Fname)
+ then
+ return True;
+ end if;
+
+ return False;
+ end Is_Predefined_File_Name;
+
+ function Is_Predefined_File_Name
+ (Fname : File_Name_Type;
+ Renamings_Included : Boolean := True) return Boolean
+ is
+ Result : constant Boolean :=
+ Is_Predefined_File_Name
+ (Get_Name_String (Fname), Renamings_Included);
+ begin
+ return Result;
+ end Is_Predefined_File_Name;
+
+ --------------------------------------
+ -- Is_Predefined_Renaming_File_Name --
+ --------------------------------------
+
+ function Is_Predefined_Renaming_File_Name
+ (Fname : String) return Boolean
+ is
+ subtype Str8 is String (1 .. 8);
+
+ Renaming_Names : constant array (1 .. 8) of Str8 :=
+ ("calendar", -- Calendar
+ "machcode", -- Machine_Code
+ "unchconv", -- Unchecked_Conversion
+ "unchdeal", -- Unchecked_Deallocation
+ "directio", -- Direct_IO
+ "ioexcept", -- IO_Exceptions
+ "sequenio", -- Sequential_IO
+ "text_io."); -- Text_IO
+ begin
+ -- Definitely false if longer than 12 characters (8.3)
+
+ if Fname'Length in 8 .. 12 then
declare
S : String renames Fname (Fname'First .. Fname'First + 7);
begin
end if;
return False;
- end Is_Predefined_File_Name;
+ end Is_Predefined_Renaming_File_Name;
- function Is_Predefined_File_Name
- (Fname : File_Name_Type;
- Renamings_Included : Boolean := True) return Boolean
- is
+ function Is_Predefined_Renaming_File_Name
+ (Fname : File_Name_Type) return Boolean is
Result : constant Boolean :=
- Is_Predefined_File_Name
- (Get_Name_String (Fname), Renamings_Included);
+ Is_Predefined_Renaming_File_Name (Get_Name_String (Fname));
begin
return Result;
- end Is_Predefined_File_Name;
+ end Is_Predefined_Renaming_File_Name;
---------------
-- Tree_Read --
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- Renamings_Included is True, then Text_IO will return True, otherwise
-- only children of Ada, Interfaces and System return True.
+ function Is_Predefined_Renaming_File_Name
+ (Fname : String) return Boolean;
+ function Is_Predefined_Renaming_File_Name
+ (Fname : File_Name_Type) return Boolean;
+ -- True if Fname is the file name for a predefined renaming (the same file
+ -- names that are included if Renamings_Included => True is passed to
+ -- Is_Predefined_File_Name).
+
function Is_Internal_File_Name
(Fname : String;
Renamings_Included : Boolean := True) return Boolean;
-- Same as Is_Predefined_File_Name, except units in the GNAT hierarchy are
-- included.
+ function Is_GNAT_File_Name (Fname : String) return Boolean;
+ function Is_GNAT_File_Name (Fname : File_Name_Type) return Boolean;
+ -- True for units in the GNAT hierarchy
+
procedure Tree_Read;
-- Dummy procedure (reads dummy table values from tree file)
with Exp_Pakd; use Exp_Pakd;
with Exp_Util; use Exp_Util;
with Exp_Tss; use Exp_Tss;
-with Fname; use Fname;
with Ghost; use Ghost;
with Layout; use Layout;
with Lib; use Lib;
if Is_Pure (E)
and then Is_Subprogram (E)
and then not Has_Pragma_Pure_Function (E)
- and then not Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
+ and then not Is_Internal_Unit (Current_Sem_Unit)
then
Check_Function_With_Address_Parameter (E);
end if;
-- these.
procedure Sort_Sections
- (Line : GNAT.OS_Lib.Argument_List_Access;
+ (Line : not null GNAT.OS_Lib.Argument_List_Access;
Sections : GNAT.OS_Lib.Argument_List_Access;
Params : GNAT.OS_Lib.Argument_List_Access);
-- Reorder the command line switches so that the switches belonging to a
-------------------
procedure Sort_Sections
- (Line : GNAT.OS_Lib.Argument_List_Access;
+ (Line : not null GNAT.OS_Lib.Argument_List_Access;
Sections : GNAT.OS_Lib.Argument_List_Access;
Params : GNAT.OS_Lib.Argument_List_Access)
is
Index : Natural;
begin
- if Line = null then
- return;
- end if;
-
-- First construct a list of all sections
for E in Line'Range loop
static bool allocatable_size_p (tree, bool);
static bool initial_value_needs_conversion (tree, tree);
static int compare_field_bitpos (const PTR, const PTR);
-static bool components_to_record (tree, Node_Id, tree, int, bool, bool, bool,
- bool, bool, bool, bool, bool, tree, tree *);
+static bool components_to_record (Node_Id, Entity_Id, tree, tree, int, bool,
+ bool, bool, bool, bool, bool, bool, tree,
+ tree *);
static Uint annotate_value (tree);
static void annotate_rep (Entity_Id, tree);
static tree build_position_list (tree, bool, tree, tree, unsigned int, tree);
}
/* Add the fields into the record type and finish it up. */
- components_to_record (gnu_type, Component_List (record_definition),
- gnu_field_list, packed, definition, false,
- all_rep, is_unchecked_union,
- artificial_p, debug_info_p,
- false, OK_To_Reorder_Components (gnat_entity),
+ components_to_record (Component_List (record_definition), gnat_entity,
+ gnu_field_list, gnu_type, packed, definition,
+ false, all_rep, is_unchecked_union, artificial_p,
+ debug_info_p, false,
all_rep ? NULL_TREE : bitsize_zero_node, NULL);
/* Fill in locations of fields. */
return ret ? ret : (int) (DECL_UID (field1) - DECL_UID (field2));
}
+/* Reverse function from gnat_to_gnu_field: return the GNAT field present in
+ either GNAT_COMPONENT_LIST or the discriminants of GNAT_RECORD_TYPE, and
+ corresponding to the GNU tree GNU_FIELD. */
+
+static Entity_Id
+gnu_field_to_gnat (tree gnu_field, Node_Id gnat_component_list,
+ Entity_Id gnat_record_type)
+{
+ Entity_Id gnat_component_decl, gnat_field;
+
+ if (Present (Component_Items (gnat_component_list)))
+ for (gnat_component_decl
+ = First_Non_Pragma (Component_Items (gnat_component_list));
+ Present (gnat_component_decl);
+ gnat_component_decl = Next_Non_Pragma (gnat_component_decl))
+ {
+ gnat_field = Defining_Entity (gnat_component_decl);
+ if (gnat_to_gnu_field_decl (gnat_field) == gnu_field)
+ return gnat_field;
+ }
+
+ if (Has_Discriminants (gnat_record_type))
+ for (gnat_field = First_Stored_Discriminant (gnat_record_type);
+ Present (gnat_field);
+ gnat_field = Next_Stored_Discriminant (gnat_field))
+ if (gnat_to_gnu_field_decl (gnat_field) == gnu_field)
+ return gnat_field;
+
+ return Empty;
+}
+
+/* Issue a warning for the problematic placement of GNU_FIELD present in
+ either GNAT_COMPONENT_LIST or the discriminants of GNAT_RECORD_TYPE.
+ IN_VARIANT is true if GNAT_COMPONENT_LIST is the list of a variant.
+ DO_REORDER is true if fields of GNAT_RECORD_TYPE are being reordered. */
+
+static void
+warn_on_field_placement (tree gnu_field, Node_Id gnat_component_list,
+ Entity_Id gnat_record_type, bool in_variant,
+ bool do_reorder)
+{
+ const char *msg1
+ = in_variant
+ ? "?variant layout may cause performance issues"
+ : "?record layout may cause performance issues";
+ const char *msg2
+ = field_has_self_size (gnu_field)
+ ? "?component & whose length depends on a discriminant"
+ : field_has_variable_size (gnu_field)
+ ? "?component & whose length is not fixed"
+ : "?component & whose length is not multiple of a byte";
+ const char *msg3
+ = do_reorder
+ ? "?comes too early and was moved down"
+ : "?comes too early and ought to be moved down";
+ Entity_Id gnat_field
+ = gnu_field_to_gnat (gnu_field, gnat_component_list, gnat_record_type);
+
+ gcc_assert (Present (gnat_field));
+
+ post_error (msg1, gnat_field);
+ post_error_ne (msg2, gnat_field, gnat_field);
+ post_error (msg3, gnat_field);
+}
+
/* Structure holding information for a given variant. */
typedef struct vinfo
{
} vinfo_t;
-/* Translate and chain the GNAT_COMPONENT_LIST to the GNU_FIELD_LIST, set the
- result as the field list of GNU_RECORD_TYPE and finish it up. Return true
- if GNU_RECORD_TYPE has a rep clause which affects the layout (see below).
- When called from gnat_to_gnu_entity during the processing of a record type
- definition, the GCC node for the parent, if any, will be the single field
- of GNU_RECORD_TYPE and the GCC nodes for the discriminants will be on the
- GNU_FIELD_LIST. The other calls to this function are recursive calls for
- the component list of a variant and, in this case, GNU_FIELD_LIST is empty.
+/* Translate and chain GNAT_COMPONENT_LIST present in GNAT_RECORD_TYPE to
+ GNU_FIELD_LIST, set the result as the field list of GNU_RECORD_TYPE and
+ finish it up. Return true if GNU_RECORD_TYPE has a rep clause that affects
+ the layout (see below). When called from gnat_to_gnu_entity during the
+ processing of a record definition, the GCC node for the parent, if any,
+ will be the single field of GNU_RECORD_TYPE and the GCC nodes for the
+ discriminants will be on GNU_FIELD_LIST. The other call to this function
+ is a recursive call for the component list of a variant and, in this case,
+ GNU_FIELD_LIST is empty.
PACKED is 1 if this is for a packed record or -1 if this is for a record
with Component_Alignment of Storage_Unit.
MAYBE_UNUSED is true if this type may be unused in the end; this doesn't
mean that its contents may be unused as well, only the container itself.
- REORDER is true if we are permitted to reorder components of this type.
-
FIRST_FREE_POS, if nonzero, is the first (lowest) free field position in
the outer record type down to this variant level. It is nonzero only if
all the fields down to this level have a rep clause and ALL_REP is false.
be done with such fields and the return value will be false. */
static bool
-components_to_record (tree gnu_record_type, Node_Id gnat_component_list,
- tree gnu_field_list, int packed, bool definition,
- bool cancel_alignment, bool all_rep,
- bool unchecked_union, bool artificial,
- bool debug_info, bool maybe_unused, bool reorder,
- tree first_free_pos, tree *p_gnu_rep_list)
+components_to_record (Node_Id gnat_component_list, Entity_Id gnat_record_type,
+ tree gnu_field_list, tree gnu_record_type, int packed,
+ bool definition, bool cancel_alignment, bool all_rep,
+ bool unchecked_union, bool artificial, bool debug_info,
+ bool maybe_unused, tree first_free_pos,
+ tree *p_gnu_rep_list)
{
const bool needs_xv_encodings
= debug_info && gnat_encodings != DWARF_GNAT_ENCODINGS_MINIMAL;
bool layout_with_rep = false;
bool has_self_field = false;
bool has_aliased_after_self_field = false;
- Node_Id component_decl, variant_part;
+ Entity_Id gnat_component_decl, gnat_variant_part;
tree gnu_field, gnu_next, gnu_last;
tree gnu_variant_part = NULL_TREE;
tree gnu_rep_list = NULL_TREE;
- tree gnu_var_list = NULL_TREE;
- tree gnu_self_list = NULL_TREE;
- tree gnu_zero_list = NULL_TREE;
/* For each component referenced in a component declaration create a GCC
field and add it to the list, skipping pragmas in the GNAT list. */
gnu_last = tree_last (gnu_field_list);
if (Present (Component_Items (gnat_component_list)))
- for (component_decl
+ for (gnat_component_decl
= First_Non_Pragma (Component_Items (gnat_component_list));
- Present (component_decl);
- component_decl = Next_Non_Pragma (component_decl))
+ Present (gnat_component_decl);
+ gnat_component_decl = Next_Non_Pragma (gnat_component_decl))
{
- Entity_Id gnat_field = Defining_Entity (component_decl);
+ Entity_Id gnat_field = Defining_Entity (gnat_component_decl);
Name_Id gnat_name = Chars (gnat_field);
/* If present, the _Parent field must have been created as the single
}
/* At the end of the component list there may be a variant part. */
- variant_part = Variant_Part (gnat_component_list);
+ gnat_variant_part = Variant_Part (gnat_component_list);
/* We create a QUAL_UNION_TYPE for the variant part since the variants are
mutually exclusive and should go in the same memory. To do this we need
lists for the variants and put them all into the QUAL_UNION_TYPE.
If this is an Unchecked_Union, we make a UNION_TYPE instead or
use GNU_RECORD_TYPE if there are no fields so far. */
- if (Present (variant_part))
+ if (Present (gnat_variant_part))
{
- Node_Id gnat_discr = Name (variant_part), variant;
+ Node_Id gnat_discr = Name (gnat_variant_part), variant;
tree gnu_discr = gnat_to_gnu (gnat_discr);
tree gnu_name = TYPE_IDENTIFIER (gnu_record_type);
tree gnu_var_name
the container types and computing the associated properties. However
we cannot finish up the container types during this pass because we
don't know where the variant part will be placed until the end. */
- for (variant = First_Non_Pragma (Variants (variant_part));
+ for (variant = First_Non_Pragma (Variants (gnat_variant_part));
Present (variant);
variant = Next_Non_Pragma (variant))
{
/* Add the fields into the record type for the variant. Note that
we aren't sure to really use it at this point, see below. */
has_rep
- = components_to_record (gnu_variant_type, Component_List (variant),
- NULL_TREE, packed, definition,
- !all_rep_and_size, all_rep,
- unchecked_union,
- true, needs_xv_encodings, true, reorder,
- this_first_free_pos,
+ = components_to_record (Component_List (variant), gnat_record_type,
+ NULL_TREE, gnu_variant_type, packed,
+ definition, !all_rep_and_size, all_rep,
+ unchecked_union, true, needs_xv_encodings,
+ true, this_first_free_pos,
all_rep || this_first_free_pos
? NULL : &gnu_rep_list);
}
}
- /* Scan GNU_FIELD_LIST and see if any fields have rep clauses and, if we are
- permitted to reorder components, self-referential sizes or variable sizes.
- If they do, pull them out and put them onto the appropriate list. We have
- to do this in a separate pass since we want to handle the discriminants
- but can't play with them until we've used them in debugging data above.
+ /* Scan GNU_FIELD_LIST and see if any fields have rep clauses. If they do,
+ pull them out and put them onto the appropriate list. We have to do it
+ in a separate pass since we want to handle the discriminants but can't
+ play with them until we've used them in debugging data above.
Similarly, pull out the fields with zero size and no rep clause, as they
would otherwise modify the layout and thus very likely run afoul of the
Ada semantics, which are different from those of C here.
+ Finally, if there is an aliased field placed in the list after fields
+ with self-referential size, pull out the latter in the same way.
+
+ Optionally, if the reordering mechanism is enabled, pull out the fields
+ with self-referential size, variable size and fixed size not a multiple
+ of a byte, so that they don't cause the regular fields to be either at
+ self-referential/variable offset or misaligned. Note, in the latter
+ case, that this can only happen in packed record types so the alignment
+ is effectively capped to the byte for the whole record.
+
+ Optionally, if the layout warning is enabled, keep track of the above 4
+ different kinds of fields and issue a warning if some of them would be
+ (or are being) reordered by the reordering mechanism.
+
??? If we reorder them, debugging information will be wrong but there is
nothing that can be done about this at the moment. */
- gnu_last = NULL_TREE;
+ const bool do_reorder = OK_To_Reorder_Components (gnat_record_type);
+ const bool w_reorder
+ = Warn_On_Questionable_Layout
+ && (Convention (gnat_record_type) == Convention_Ada);
+ const bool in_variant = (p_gnu_rep_list != NULL);
+ tree gnu_zero_list = NULL_TREE;
+ tree gnu_self_list = NULL_TREE;
+ tree gnu_var_list = NULL_TREE;
+ tree gnu_bitp_list = NULL_TREE;
+ tree gnu_tmp_bitp_list = NULL_TREE;
+ unsigned int tmp_bitp_size = 0;
+ unsigned int last_reorder_field_type = -1;
+ unsigned int tmp_last_reorder_field_type = -1;
#define MOVE_FROM_FIELD_LIST_TO(LIST) \
do { \
(LIST) = gnu_field; \
} while (0)
+ gnu_last = NULL_TREE;
for (gnu_field = gnu_field_list; gnu_field; gnu_field = gnu_next)
{
gnu_next = DECL_CHAIN (gnu_field);
continue;
}
- if ((reorder || has_aliased_after_self_field)
- && field_has_self_size (gnu_field))
- {
- MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
- continue;
- }
-
- if (reorder && field_has_variable_size (gnu_field))
- {
- MOVE_FROM_FIELD_LIST_TO (gnu_var_list);
- continue;
- }
-
if (DECL_SIZE (gnu_field) && integer_zerop (DECL_SIZE (gnu_field)))
{
DECL_FIELD_OFFSET (gnu_field) = size_zero_node;
continue;
}
+ if (has_aliased_after_self_field && field_has_self_size (gnu_field))
+ {
+ MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
+ continue;
+ }
+
+ /* We don't need further processing in default mode. */
+ if (!w_reorder && !do_reorder)
+ {
+ gnu_last = gnu_field;
+ continue;
+ }
+
+ if (field_has_self_size (gnu_field))
+ {
+ if (w_reorder)
+ {
+ if (last_reorder_field_type < 4)
+ warn_on_field_placement (gnu_field, gnat_component_list,
+ gnat_record_type, in_variant,
+ do_reorder);
+ else
+ last_reorder_field_type = 4;
+ }
+
+ if (do_reorder)
+ {
+ MOVE_FROM_FIELD_LIST_TO (gnu_self_list);
+ continue;
+ }
+ }
+
+ else if (field_has_variable_size (gnu_field))
+ {
+ if (w_reorder)
+ {
+ if (last_reorder_field_type < 3)
+ warn_on_field_placement (gnu_field, gnat_component_list,
+ gnat_record_type, in_variant,
+ do_reorder);
+ else
+ last_reorder_field_type = 3;
+ }
+
+ if (do_reorder)
+ {
+ MOVE_FROM_FIELD_LIST_TO (gnu_var_list);
+ continue;
+ }
+ }
+
+ else
+ {
+ /* If the field has no size, then it cannot be bit-packed. */
+ const unsigned int bitp_size
+ = DECL_SIZE (gnu_field)
+ ? TREE_INT_CST_LOW (DECL_SIZE (gnu_field)) % BITS_PER_UNIT
+ : 0;
+
+ /* If the field is bit-packed, we move it to a temporary list that
+ contains the contiguously preceding bit-packed fields, because
+ we want to be able to put them back if the misalignment happens
+ to cancel itself after several bit-packed fields. */
+ if (bitp_size != 0)
+ {
+ tmp_bitp_size = (tmp_bitp_size + bitp_size) % BITS_PER_UNIT;
+
+ if (last_reorder_field_type != 2)
+ {
+ tmp_last_reorder_field_type = last_reorder_field_type;
+ last_reorder_field_type = 2;
+ }
+
+ if (do_reorder)
+ {
+ MOVE_FROM_FIELD_LIST_TO (gnu_tmp_bitp_list);
+ continue;
+ }
+ }
+
+ /* No more bit-packed fields, move the existing ones to the end or
+ put them back at their original location. */
+ else if (last_reorder_field_type == 2 || gnu_tmp_bitp_list)
+ {
+ last_reorder_field_type = 1;
+
+ if (tmp_bitp_size != 0)
+ {
+ if (w_reorder && tmp_last_reorder_field_type < 2)
+ warn_on_field_placement (gnu_tmp_bitp_list
+ ? gnu_tmp_bitp_list : gnu_last,
+ gnat_component_list,
+ gnat_record_type, in_variant,
+ do_reorder);
+
+ if (do_reorder)
+ gnu_bitp_list = chainon (gnu_tmp_bitp_list, gnu_bitp_list);
+
+ gnu_tmp_bitp_list = NULL_TREE;
+ tmp_bitp_size = 0;
+ }
+ else
+ {
+ /* Rechain the temporary list in front of GNU_FIELD. */
+ tree gnu_bitp_field = gnu_field;
+ while (gnu_tmp_bitp_list)
+ {
+ tree gnu_bitp_next = DECL_CHAIN (gnu_tmp_bitp_list);
+ DECL_CHAIN (gnu_tmp_bitp_list) = gnu_bitp_field;
+ if (gnu_last)
+ DECL_CHAIN (gnu_last) = gnu_tmp_bitp_list;
+ else
+ gnu_field_list = gnu_tmp_bitp_list;
+ gnu_bitp_field = gnu_tmp_bitp_list;
+ gnu_tmp_bitp_list = gnu_bitp_next;
+ }
+ }
+ }
+
+ else
+ last_reorder_field_type = 1;
+ }
+
gnu_last = gnu_field;
}
/* If permitted, we reorder the fields as follows:
- 1) all fixed length fields,
- 2) all fields whose length doesn't depend on discriminants,
- 3) all fields whose length depends on discriminants,
- 4) the variant part,
+ 1) all (groups of) fields whose length is fixed and multiple of a byte,
+ 2) the remaining fields whose length is fixed and not multiple of a byte,
+ 3) the remaining fields whose length doesn't depend on discriminants,
+ 4) all fields whose length depends on discriminants,
+ 5) the variant part,
within the record and within each variant recursively. */
- if (reorder)
- gnu_field_list
- = chainon (gnu_field_list, chainon (gnu_var_list, gnu_self_list));
+ if (w_reorder
+ && last_reorder_field_type == 2
+ && tmp_last_reorder_field_type < 2)
+ warn_on_field_placement (gnu_tmp_bitp_list
+ ? gnu_tmp_bitp_list : gnu_field_list,
+ gnat_component_list, gnat_record_type,
+ in_variant, do_reorder);
+ if (do_reorder)
+ {
+ if (gnu_tmp_bitp_list)
+ gnu_bitp_list = chainon (gnu_tmp_bitp_list, gnu_bitp_list);
+
+ gnu_field_list
+ = chainon (gnu_field_list,
+ chainon (gnu_bitp_list,
+ chainon (gnu_var_list, gnu_self_list)));
+ }
/* Otherwise, if there is an aliased field placed after a field whose length
depends on discriminants, we put all the fields of the latter sort, last.
-- Detect that the runtime library support for floating-point numbers
-- may not be compatible with SPARK analysis of IEEE-754 floats.
- if Denorm_On_Target = False then
- Write_Line
- ("warning: Run-time library may be configured incorrectly");
- Write_Line
- ("warning: "
- & "(SPARK analysis requires support for float subnormals)");
-
- elsif Machine_Rounds_On_Target = False then
- Write_Line
- ("warning: Run-time library may be configured incorrectly");
- Write_Line
- ("warning: "
- & "(SPARK analysis requires support for float rounding)");
-
- elsif Signed_Zeros_On_Target = False then
- Write_Line
- ("warning: Run-time library may be configured incorrectly");
- Write_Line
- ("warning: (SPARK analysis requires support for signed zeros)");
- end if;
+ declare
+ procedure SPARK_Library_Warning (Kind : String);
+ -- Issue a warning in GNATprove mode if the run-time library does
+ -- not fully support IEEE-754 floating-point semantics.
+
+ procedure SPARK_Library_Warning (Kind : String) is
+ begin
+ Write_Line
+ ("warning: run-time library may be configured incorrectly");
+ Write_Line
+ ("warning: (SPARK analysis requires support for " & Kind
+ & ')');
+ end SPARK_Library_Warning;
+
+ begin
+ if Denorm_On_Target = False then
+ SPARK_Library_Warning ("float subnormals");
+ elsif Machine_Rounds_On_Target = False then
+ SPARK_Library_Warning ("float rounding");
+ elsif Signed_Zeros_On_Target = False then
+ SPARK_Library_Warning ("signed zeros");
+ end if;
+ end;
end if;
-- Set Configurable_Run_Time mode if system.ads flag set or if the
if not Comes_From_Source (N)
and then In_Extended_Main_Source_Unit (N)
- and then
- Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (E)))
+ and then Is_Predefined_Unit (Get_Source_Unit (E))
then
Set_Needs_Debug_Info (E, False);
end if;
-- subprograms may contain nested subprograms and become ineligible
-- for inlining.
- if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
+ if Is_Predefined_Unit (Get_Source_Unit (Subp))
and then not In_Extended_Main_Source_Unit (Subp)
then
null;
-- compatibility but it will be removed when we enforce the
-- strictness of the new rules.
- if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (Subp)))
+ if Is_Predefined_Unit (Get_Source_Unit (Subp))
and then not In_Extended_Main_Source_Unit (Subp)
then
null;
declare
Gen_P : constant Entity_Id := Generic_Parent (Parent (Subp));
begin
- if Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Gen_P)))
- then
+ if Is_Predefined_Unit (Get_Source_Unit (Gen_P)) then
Set_Is_Inlined (Subp, False);
Error_Msg_NE (Msg & "p?", N, Subp);
return;
is
Loc : constant Source_Ptr := Sloc (N);
Is_Predef : constant Boolean :=
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Subp)));
+ Is_Predefined_Unit (Get_Source_Unit (Subp));
Orig_Bod : constant Node_Id :=
Body_To_Inline (Unit_Declaration_Node (Subp));
end if;
return Present (Conv)
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Conv)))
+ and then Is_Predefined_Unit (Get_Source_Unit (Conv))
and then Is_Intrinsic_Subprogram (Conv);
end Is_Unchecked_Conversion;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2009, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
for R in Sorted_Units'Range loop
if File_Names_Only then
- if not Is_Internal_File_Name
- (File_Name (Source_Index (Sorted_Units (R))))
- then
+ if not Is_Internal_Unit (Sorted_Units (R)) then
Write_Name (Full_File_Name (Source_Index (Sorted_Units (R))));
Write_Eol;
end if;
Cunit : Node_Id;
Du_Name : Node_Or_Entity_Id;
End_Lab : Node_Id;
- Save_CS : constant Boolean := Get_Comes_From_Source_Default;
+ Fname : constant File_Name_Type :=
+ Get_File_Name (Spec_Name, Subunit => False);
+ Pre_Name : constant Boolean :=
+ Is_Predefined_File_Name (Fname, Renamings_Included => False);
+ Ren_Name : constant Boolean :=
+ Is_Predefined_Renaming_File_Name (Fname);
+ GNAT_Name : constant Boolean :=
+ Is_GNAT_File_Name (Fname);
+ Save_CS : constant Boolean := Get_Comes_From_Source_Default;
begin
-- The created dummy package unit does not come from source
Units.Increment_Last;
Unum := Units.Last;
- Units.Table (Unum) := (
- Cunit => Cunit,
- Cunit_Entity => Cunit_Entity,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => Sloc (With_Node),
- Expected_Unit => Spec_Name,
- Fatal_Error => Error_Detected,
- Generate_Code => False,
- Has_RACW => False,
- Filler => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- No_Elab_Code_All => False,
- Serial_Number => 0,
- Source_Index => No_Source_File,
- Unit_File_Name => Get_File_Name (Spec_Name, Subunit => False),
- Unit_Name => Spec_Name,
- Version => 0,
- OA_Setting => 'O');
+ Units.Table (Unum) :=
+ (Cunit => Cunit,
+ Cunit_Entity => Cunit_Entity,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => Sloc (With_Node),
+ Expected_Unit => Spec_Name,
+ Fatal_Error => Error_Detected,
+ Generate_Code => False,
+ Has_RACW => False,
+ Filler => False,
+ Ident_String => Empty,
+
+ Is_Predefined_Renaming => Ren_Name,
+ Is_Predefined_Unit => Pre_Name or Ren_Name,
+ Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
+ Filler2 => False,
+
+ Loading => False,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ No_Elab_Code_All => False,
+ Serial_Number => 0,
+ Source_Index => No_Source_File,
+ Unit_File_Name => Fname,
+ Unit_Name => Spec_Name,
+ Version => 0,
+ OA_Setting => 'O');
Set_Comes_From_Source_Default (Save_CS);
Set_Error_Posted (Cunit_Entity);
----------------------
procedure Load_Main_Source is
- Fname : File_Name_Type;
+ Fname : constant File_Name_Type := Next_Main_Source;
+ Pre_Name : constant Boolean :=
+ Is_Predefined_File_Name (Fname, Renamings_Included => False);
+ Ren_Name : constant Boolean :=
+ Is_Predefined_Renaming_File_Name (Fname);
+ GNAT_Name : constant Boolean :=
+ Is_GNAT_File_Name (Fname);
Version : Word := 0;
begin
-- Cunit_Entity fields also get filled in later by the parser.
Units.Increment_Last;
- Fname := Next_Main_Source;
Units.Table (Main_Unit).Unit_File_Name := Fname;
Version := Source_Checksum (Main_Source_File);
end if;
- Units.Table (Main_Unit) := (
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => No_Location,
- Expected_Unit => No_Unit_Name,
- Fatal_Error => None,
- Generate_Code => False,
- Has_RACW => False,
- Filler => False,
- Ident_String => Empty,
- Loading => True,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- No_Elab_Code_All => False,
- Serial_Number => 0,
- Source_Index => Main_Source_File,
- Unit_File_Name => Fname,
- Unit_Name => No_Unit_Name,
- Version => Version,
- OA_Setting => 'O');
+ Units.Table (Main_Unit) :=
+ (Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => No_Location,
+ Expected_Unit => No_Unit_Name,
+ Fatal_Error => None,
+ Generate_Code => False,
+ Has_RACW => False,
+ Filler => False,
+ Ident_String => Empty,
+
+ Is_Predefined_Renaming => Ren_Name,
+ Is_Predefined_Unit => Pre_Name or Ren_Name,
+ Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
+ Filler2 => False,
+
+ Loading => True,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ No_Elab_Code_All => False,
+ Serial_Number => 0,
+ Source_Index => Main_Source_File,
+ Unit_File_Name => Fname,
+ Unit_Name => No_Unit_Name,
+ Version => Version,
+ OA_Setting => 'O');
end if;
end Load_Main_Source;
Unum : Unit_Number_Type;
Unump : Unit_Number_Type;
Fname : File_Name_Type;
+ Pre_Name : Boolean;
+ Ren_Name : Boolean;
+ GNAT_Name : Boolean;
Src_Ind : Source_File_Index;
Save_PMES : constant Boolean := Parsing_Main_Extended_Source;
Uname_Actual := Load_Name;
end if;
- Fname := Get_File_Name (Uname_Actual, Subunit);
+ Fname := Get_File_Name (Uname_Actual, Subunit);
+ Pre_Name :=
+ Is_Predefined_File_Name (Fname, Renamings_Included => False);
+ Ren_Name := Is_Predefined_Renaming_File_Name (Fname);
+ GNAT_Name := Is_GNAT_File_Name (Fname);
if Debug_Flag_L then
Write_Eol;
-- File was found
if Src_Ind /= No_Source_File then
- Units.Table (Unum) := (
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Error_Location => Sloc (Error_Node),
- Expected_Unit => Uname_Actual,
- Fatal_Error => None,
- Generate_Code => False,
- Has_RACW => False,
- Filler => False,
- Ident_String => Empty,
- Loading => True,
- Main_Priority => Default_Main_Priority,
- Main_CPU => Default_Main_CPU,
- Munit_Index => 0,
- No_Elab_Code_All => False,
- Serial_Number => 0,
- Source_Index => Src_Ind,
- Unit_File_Name => Fname,
- Unit_Name => Uname_Actual,
- Version => Source_Checksum (Src_Ind),
- OA_Setting => 'O');
+ Units.Table (Unum) :=
+ (Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Error_Location => Sloc (Error_Node),
+ Expected_Unit => Uname_Actual,
+ Fatal_Error => None,
+ Generate_Code => False,
+ Has_RACW => False,
+ Filler => False,
+ Ident_String => Empty,
+
+ Is_Predefined_Renaming => Ren_Name,
+ Is_Predefined_Unit => Pre_Name or Ren_Name,
+ Is_Internal_Unit => Pre_Name or Ren_Name or GNAT_Name,
+ Filler2 => False,
+
+ Loading => True,
+ Main_Priority => Default_Main_Priority,
+ Main_CPU => Default_Main_CPU,
+ Munit_Index => 0,
+ No_Elab_Code_All => False,
+ Serial_Number => 0,
+ Source_Index => Src_Ind,
+ Unit_File_Name => Fname,
+ Unit_Name => Uname_Actual,
+ Version => Source_Checksum (Src_Ind),
+ OA_Setting => 'O');
-- Parse the new unit
-- code will have to be generated for it.
procedure Make_Instance_Unit (N : Node_Id; In_Main : Boolean) is
- Sind : constant Source_File_Index := Source_Index (Main_Unit);
+ Sind : constant Source_File_Index := Source_Index (Main_Unit);
begin
Units.Increment_Last;
begin
Units.Increment_Last;
Units.Table (Units.Last) :=
- (Unit_File_Name => File_Name (S),
- Unit_Name => No_Unit_Name,
- Expected_Unit => No_Unit_Name,
- Source_Index => S,
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Fatal_Error => None,
- Generate_Code => False,
- Has_RACW => False,
- Filler => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => -1,
- Main_CPU => -1,
- Munit_Index => 0,
- No_Elab_Code_All => False,
- Serial_Number => 0,
- Version => 0,
- Error_Location => No_Location,
- OA_Setting => 'O');
+ (Unit_File_Name => File_Name (S),
+ Unit_Name => No_Unit_Name,
+ Expected_Unit => No_Unit_Name,
+ Source_Index => S,
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Fatal_Error => None,
+ Generate_Code => False,
+ Has_RACW => False,
+ Filler => False,
+ Ident_String => Empty,
+ Is_Predefined_Renaming => False,
+ Is_Internal_Unit => False,
+ Is_Predefined_Unit => False,
+ Filler2 => False,
+ Loading => False,
+ Main_Priority => -1,
+ Main_CPU => -1,
+ Munit_Index => 0,
+ No_Elab_Code_All => False,
+ Serial_Number => 0,
+ Version => 0,
+ Error_Location => No_Location,
+ OA_Setting => 'O');
end Add_Preprocessing_Dependency;
------------------------------
System_Fname := File_Name (System_Source_File_Index);
Units.Increment_Last;
- Units.Table (Units.Last) := (
- Unit_File_Name => System_Fname,
- Unit_Name => System_Uname,
- Expected_Unit => System_Uname,
- Source_Index => System_Source_File_Index,
- Cunit => Empty,
- Cunit_Entity => Empty,
- Dependency_Num => 0,
- Dynamic_Elab => False,
- Fatal_Error => None,
- Generate_Code => False,
- Has_RACW => False,
- Filler => False,
- Ident_String => Empty,
- Loading => False,
- Main_Priority => -1,
- Main_CPU => -1,
- Munit_Index => 0,
- No_Elab_Code_All => False,
- Serial_Number => 0,
- Version => 0,
- Error_Location => No_Location,
- OA_Setting => 'O');
+ Units.Table (Units.Last) :=
+ (Unit_File_Name => System_Fname,
+ Unit_Name => System_Uname,
+ Expected_Unit => System_Uname,
+ Source_Index => System_Source_File_Index,
+ Cunit => Empty,
+ Cunit_Entity => Empty,
+ Dependency_Num => 0,
+ Dynamic_Elab => False,
+ Fatal_Error => None,
+ Generate_Code => False,
+ Has_RACW => False,
+ Filler => False,
+ Ident_String => Empty,
+ Is_Predefined_Renaming => False,
+ Is_Internal_Unit => True,
+ Is_Predefined_Unit => True,
+ Filler2 => False,
+ Loading => False,
+ Main_Priority => -1,
+ Main_CPU => -1,
+ Munit_Index => 0,
+ No_Elab_Code_All => False,
+ Serial_Number => 0,
+ Version => 0,
+ Error_Location => No_Location,
+ OA_Setting => 'O');
-- Parse system.ads so that the checksum is set right. Style checks are
-- not applied. The Ekind is set to ensure that this reference is always
Write_Info_Str (" GE");
end if;
- if not Is_Internal_File_Name (Unit_File_Name (Unit_Num), True) then
+ if not Is_Internal_Unit (Unit_Num) then
case Identifier_Casing (Source_Index (Unit_Num)) is
when All_Lower_Case => Write_Info_Str (" IL");
when All_Upper_Case => Write_Info_Str (" IU");
-- parameters (see Lib_Writ spec for an explanation).
if Is_Generic_Unit (Cunit_Entity (Main_Unit))
- and then
- Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
+ and then Is_Predefined_Unit (Current_Sem_Unit)
and then Linker_Option_Lines.Table (J).Unit = Unit_Num
then
Set_Standard_Error;
if not ((Nkind (Unit (Cunit)) in N_Generic_Declaration
or else
Nkind (Unit (Cunit)) in N_Generic_Renaming_Declaration)
- and then Generic_May_Lack_ALI (Fname))
+ and then Generic_May_Lack_ALI (Unum))
-- In SPARK mode, always generate the dependencies on ALI
-- files, which are required to compute frame conditions
Write_Info_Str (" DB");
end if;
- if Tasking_Used
- and then not Is_Predefined_File_Name (Unit_File_Name (Main_Unit))
- then
+ if Tasking_Used and then not Is_Predefined_Unit (Main_Unit) then
if Locking_Policy /= ' ' then
Write_Info_Str (" L");
Write_Info_Char (Locking_Policy);
with Atree; use Atree;
with Csets; use Csets;
with Einfo; use Einfo;
-with Fname; use Fname;
with Nlists; use Nlists;
with Opt; use Opt;
with Output; use Output;
return Units.Table (U).Has_RACW;
end Has_RACW;
+ function Is_Predefined_Renaming (U : Unit_Number_Type) return Boolean is
+ begin
+ return Units.Table (U).Is_Predefined_Renaming;
+ end Is_Predefined_Renaming;
+
+ function Is_Internal_Unit (U : Unit_Number_Type) return Boolean is
+ begin
+ return Units.Table (U).Is_Internal_Unit;
+ end Is_Internal_Unit;
+
+ function Is_Predefined_Unit (U : Unit_Number_Type) return Boolean is
+ begin
+ return Units.Table (U).Is_Predefined_Unit;
+ end Is_Predefined_Unit;
+
function Ident_String (U : Unit_Number_Type) return Node_Id is
begin
return Units.Table (U).Ident_String;
-- Generic_May_Lack_ALI --
--------------------------
- function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean is
+ function Generic_May_Lack_ALI (Unum : Unit_Number_Type) return Boolean is
begin
-- We allow internal generic units to be used without having a
-- corresponding ALI files to help bootstrapping with older compilers
-- is the elaboration boolean, and we are careful to elaborate all
-- predefined units first anyway.
- return Is_Internal_File_Name
- (Fname => Sfile,
- Renamings_Included => True);
+ return Is_Internal_Unit (Unum);
end Generic_May_Lack_ALI;
-----------------------------
function In_Internal_Unit (S : Source_Ptr) return Boolean is
Unit : constant Unit_Number_Type := Get_Source_Unit (S);
- File : constant File_Name_Type := Unit_File_Name (Unit);
-
begin
- return Is_Internal_File_Name (File);
+ return Is_Internal_Unit (Unit);
end In_Internal_Unit;
+ ----------------------------
+ -- In_Predefined_Renaming --
+ ----------------------------
+
+ function In_Predefined_Renaming (N : Node_Or_Entity_Id) return Boolean is
+ begin
+ return In_Predefined_Renaming (Sloc (N));
+ end In_Predefined_Renaming;
+
+ function In_Predefined_Renaming (S : Source_Ptr) return Boolean is
+ Unit : constant Unit_Number_Type := Get_Source_Unit (S);
+ begin
+ return Is_Predefined_Renaming (Unit);
+ end In_Predefined_Renaming;
+
------------------------
-- In_Predefined_Unit --
------------------------
function In_Predefined_Unit (S : Source_Ptr) return Boolean is
Unit : constant Unit_Number_Type := Get_Source_Unit (S);
- File : constant File_Name_Type := Unit_File_Name (Unit);
begin
- return Is_Predefined_File_Name (File);
+ return Is_Predefined_Unit (Unit);
end In_Predefined_Unit;
-----------------------
-- N_String_Literal node from a valid pragma Ident that applies to
-- this unit. If no Ident pragma applies to the unit, then Empty.
+ -- Is_Predefined_Renaming
+ -- True if this unit is a predefined renaming, as in "Text_IO renames
+ -- Ada.Text_IO").
+
+ -- Is_Internal_Unit
+ -- Same as In_Predefined_Unit, except units in the GNAT hierarchy are
+ -- included.
+
+ -- Is_Predefined_Unit
+ -- True if this unit is predefined (i.e. part of the Ada, System, or
+ -- Interface hierarchies, or Is_Predefined_Renaming). Note that units
+ -- in the GNAT hierarchy are not considered predefined.
+
-- Loading
-- A flag that is used to catch circular WITH dependencies. It is set
-- True when an entry is initially created in the file table, and set
function Generate_Code (U : Unit_Number_Type) return Boolean;
function Ident_String (U : Unit_Number_Type) return Node_Id;
function Has_RACW (U : Unit_Number_Type) return Boolean;
+ function Is_Predefined_Renaming (U : Unit_Number_Type) return Boolean;
+ function Is_Internal_Unit (U : Unit_Number_Type) return Boolean;
+ function Is_Predefined_Unit (U : Unit_Number_Type) return Boolean;
function Loading (U : Unit_Number_Type) return Boolean;
function Main_CPU (U : Unit_Number_Type) return Int;
function Main_Priority (U : Unit_Number_Type) return Int;
-- Return the Nth stored compilation switch, or null if less than N
-- switches have been stored. Used by ASIS and back ends written in Ada.
- function Generic_May_Lack_ALI (Sfile : File_Name_Type) return Boolean;
+ function Generic_May_Lack_ALI (Unum : Unit_Number_Type) return Boolean;
-- Generic units must be separately compiled. Since we always use
-- macro substitution for generics, the resulting object file is a dummy
-- one with no code, but the ALI file has the normal form, and we need
-- of the descendant packages of one of these three packages).
function In_Predefined_Unit (S : Source_Ptr) return Boolean;
+ pragma Inline (In_Predefined_Unit);
-- Same function as above but argument is a source pointer
function In_Internal_Unit (N : Node_Or_Entity_Id) return Boolean;
function In_Internal_Unit (S : Source_Ptr) return Boolean;
+ pragma Inline (In_Internal_Unit);
-- Same as In_Predefined_Unit, except units in the GNAT hierarchy are
-- included.
+ function In_Predefined_Renaming (N : Node_Or_Entity_Id) return Boolean;
+ function In_Predefined_Renaming (S : Source_Ptr) return Boolean;
+ pragma Inline (In_Predefined_Renaming);
+ -- Returns True if N or S is in a predefined renaming unit
+
function In_Same_Code_Unit (N1, N2 : Node_Or_Entity_Id) return Boolean;
pragma Inline (In_Same_Code_Unit);
-- Determines if the two nodes or entities N1 and N2 are in the same
pragma Inline (Set_Fatal_Error);
pragma Inline (Set_Generate_Code);
pragma Inline (Set_Has_RACW);
+ pragma Inline (Is_Predefined_Renaming);
+ pragma Inline (Is_Internal_Unit);
+ pragma Inline (Is_Predefined_Unit);
pragma Inline (Set_Loading);
pragma Inline (Set_Main_CPU);
pragma Inline (Set_Main_Priority);
Filler : Boolean;
Loading : Boolean;
OA_Setting : Character;
+
+ Is_Predefined_Renaming : Boolean;
+ Is_Internal_Unit : Boolean;
+ Is_Predefined_Unit : Boolean;
+ Filler2 : Boolean;
end record;
-- The following representation clause ensures that the above record
Filler at 61 range 0 .. 7;
OA_Setting at 62 range 0 .. 7;
Loading at 63 range 0 .. 7;
+
+ Is_Predefined_Renaming at 64 range 0 .. 7;
+ Is_Internal_Unit at 65 range 0 .. 7;
+ Is_Predefined_Unit at 66 range 0 .. 7;
+ Filler2 at 67 range 0 .. 7;
end record;
- for Unit_Record'Size use 64 * 8;
+ for Unit_Record'Size use 68 * 8;
-- This ensures that we did not leave out any fields
package Units is new Table.Table (
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
for Ucount in Pos loop
Set_Opt_Config_Switches
- (Is_Internal_File_Name (File_Name (Current_Source_File)),
- Current_Source_Unit = Main_Unit);
+ (Is_Internal_Unit (Current_Source_Unit),
+ Main_Unit => Current_Source_Unit = Main_Unit);
-- Initialize scope table and other parser control variables
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- Otherwise suppress message if internal file
else
- return Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (N)));
+ return In_Internal_Unit (N);
end if;
end Suppress_Restriction_Message;
-- unit for inlining purposes, the body must be illegal in this
-- mode, and there is no point in continuing.
- if Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Sloc (Current_Error_Node))))
- then
+ if In_Predefined_Unit (Current_Error_Node) then
Error_Msg_N
("construct not allowed in no run time mode!",
Current_Error_Node);
E : constant Entity_Id :=
Defining_Entity (Unit (Cunit (Unum)));
begin
- pragma Assert (Is_Predefined_File_Name (Unit_File_Name (Unum)));
+ pragma Assert (Is_Predefined_Unit (Unum));
-- Loop through entries in RTU table looking for matching entry
with Elists; use Elists;
with Exp_SPARK; use Exp_SPARK;
with Expander; use Expander;
-with Fname; use Fname;
with Ghost; use Ghost;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
-- Sequential_IO) as this would prevent pragma Extend_System from being
-- taken into account, for example when Text_IO is renaming DEC.Text_IO.
- if Is_Predefined_File_Name
- (Unit_File_Name (Current_Sem_Unit), Renamings_Included => False)
+ if Is_Predefined_Unit (Current_Sem_Unit)
+ and then not Is_Predefined_Renaming (Current_Sem_Unit)
then
GNAT_Mode := True;
end if;
Save_Opt_Config_Switches (Save_Config_Switches);
Set_Opt_Config_Switches
- (Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit)),
+ (Is_Internal_Unit (Current_Sem_Unit),
Is_Main_Unit_Or_Main_Unit_Spec);
-- Save current non-partition-wide restrictions
with Elists; use Elists;
with Errout; use Errout;
with Exp_Disp; use Exp_Disp;
-with Fname; use Fname;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
-- so it is convenient not to generate them (since it causes
-- annoying interference with debugging).
- if Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
- and then not Is_Internal_File_Name (Unit_File_Name (Main_Unit))
+ if Is_Internal_Unit (Current_Sem_Unit)
+ and then not Is_Internal_Unit (Main_Unit)
then
return;
if Is_Private_Type (T)
and then not Has_Pragma_Preelab_Init (T)
- and then not Is_Internal_File_Name
- (Unit_File_Name (Get_Source_Unit (N)))
+ and then not In_Internal_Unit (N)
then
Error_Msg_N
("private ancestor type not allowed in preelaborated unit", A);
if In_Preelaborated_Unit
and then not Debug_Flag_PP
and then Comes_From_Source (E)
- and then not
- Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (E)))
+ and then not In_Internal_Unit (E)
and then (not Inside_A_Generic
or else Present (Enclosing_Generic_Body (E)))
and then not Is_Protected_Type (Etype (E))
E := Entity (N);
Val := Constant_Value (E);
- if Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (N)))
+ if In_Internal_Unit (N)
and then
Enclosing_Comp_Unit_Node (N) /= Enclosing_Comp_Unit_Node (E)
and then (Is_Preelaborated (Scope (E))
Circularity : Boolean := True;
begin
- if Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Unit (N))))
- then
+ if In_Predefined_Unit (N) then
Circularity := False;
else
-- Register predefined units in Rtsfind
- declare
- Unum : constant Unit_Number_Type := Get_Source_Unit (Sloc (N));
- begin
- if Is_Predefined_File_Name (Unit_File_Name (Unum)) then
- Set_RTU_Loaded (Unit_Node);
- end if;
- end;
+ if In_Predefined_Unit (N) then
+ Set_RTU_Loaded (Unit_Node);
+ end if;
-- Treat compilation unit pragmas that appear after the library unit
-- No checks needed for predefined files
- or else Is_Predefined_File_Name (Unit_File_Name (Unum))
+ or else Is_Predefined_Unit (Unum)
-- No checks required if no separate spec
-- himself, but that's a marginal case, and fixing it is hard ???
if Restriction_Check_Required (No_Obsolescent_Features) then
- declare
- F : constant File_Name_Type :=
- Unit_File_Name (Get_Source_Unit (U));
- begin
- if Is_Predefined_File_Name (F, Renamings_Included => True)
- and then not
- Is_Predefined_File_Name (F, Renamings_Included => False)
- then
- Check_Restriction (No_Obsolescent_Features, N);
- Restriction_Violation := True;
- end if;
- end;
+ if In_Predefined_Renaming (U) then
+ Check_Restriction (No_Obsolescent_Features, N);
+ Restriction_Violation := True;
+ end if;
end if;
-- Check No_Implementation_Units violation
-- clauses into regular with clauses.
if Sloc (U) /= No_Location then
- if Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (U)))
+ if In_Predefined_Unit (U)
-- In ASIS mode the rtsfind mechanism plays no role, and
-- we need to maintain the original tree structure, so
Semantics (Library_Unit (N));
- Intunit := Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit));
+ Intunit := Is_Internal_Unit (Current_Sem_Unit);
if Sloc (U) /= No_Location then
-- Exclude license check if withed unit is an internal unit.
-- This situation arises e.g. with the GPL version of GNAT.
- if Is_Internal_File_Name (Unit_File_Name (Withu)) then
+ if Is_Internal_Unit (Withu) then
null;
-- Otherwise check various cases
-- skipped for dummy units (for missing packages).
if Sloc (Uname) /= No_Location
- and then (not Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
+ and then (not Is_Internal_Unit (Current_Sem_Unit)
or else Current_Sem_Unit = Main_Unit)
then
Check_Restricted_Unit
-- predefined subprograms marked Inline_Always, to minimize
-- the use of the run-time library.
- elsif Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Gen_Decl)))
+ elsif In_Predefined_Unit (Gen_Decl)
and then Configurable_Run_Time_Mode
and then Nkind (Parent (N)) /= N_Compilation_Unit
then
-- interested in finding possible runtime errors.
if not CodePeer_Mode
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Gen_Decl)))
+ and then In_Predefined_Unit (Gen_Decl)
then
Analyze (Act_Body, Suppress => All_Checks);
else
-- to predefined units. Nothing needs to be done for non-internal units.
-- These are always analyzed in the current mode.
- if Is_Internal_File_Name
- (Fname => Unit_File_Name (Get_Source_Unit (Gen_Unit)),
- Renamings_Included => True)
- then
+ if In_Internal_Unit (Gen_Unit) then
Set_Opt_Config_Switches (True, Current_Sem_Unit = Main_Unit);
-- In Ada2012 we may want to enable assertions in an instance of a
with Exp_Dist; use Exp_Dist;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Itypes; use Itypes;
if Chars (Scope (Def_Id)) = Name_System
and then Chars (Def_Id) = Name_Address
- and then Is_Predefined_File_Name (Unit_File_Name (Get_Source_Unit (N)))
+ and then In_Predefined_Unit (N)
then
Set_Is_Descendant_Of_Address (Def_Id);
Set_Is_Descendant_Of_Address (Base_Type (Def_Id));
with Elists; use Elists;
with Errout; use Errout;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Itypes; use Itypes;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
and then
(Etype (Actual) /= Universal_Integer
or else not Is_Descendant_Of_Address (Etype (Formal))
- or else
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (N))))
+ or else In_Predefined_Unit (N))
then
Next_Actual (Actual);
Next_Formal (Formal);
-- variants of System, and it must be removed as well.
elsif Ada_Version >= Ada_2005
- or else Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (It.Nam)))
+ or else In_Predefined_Unit (It.Nam)
then
Remove_Interp (I);
exit;
with Exp_Disp; use Exp_Disp;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
elsif Style_Check
and then Can_Override_Operator (Spec_Id)
- and then not Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Spec_Id)))
+ and then not In_Predefined_Unit (Spec_Id)
then
pragma Assert (Unit_Declaration_Node (Body_Id) = N);
Style.Missing_Overriding (N, Body_Id);
and then Chars (Overridden_Subp) = Name_Adjust
and then Is_Limited_Type (Etype (First_Formal (Subp)))
and then Present (Alias (Overridden_Subp))
- and then
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Alias (Overridden_Subp))))
+ and then In_Predefined_Unit (Alias (Overridden_Subp))
then
Get_Name_String
(Unit_File_Name (Get_Source_Unit (Alias (Overridden_Subp))));
elsif not Error_Posted (Subp)
and then Style_Check
and then Can_Override_Operator (Subp)
- and then
- not Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Subp)))
+ and then not In_Predefined_Unit (Subp)
then
-- If style checks are enabled, indicate that the indicator is
-- missing. However, at the point of declaration, the type of
with Exp_Disp; use Exp_Disp;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Impunit; use Impunit;
-- except that packages whose file name starts a-n are OK (these are
-- children of Ada.Numerics, which are never loaded by Rtsfind).
- if Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
+ if Is_Predefined_Unit (Current_Sem_Unit)
and then Get_Name_String
(Unit_File_Name (Current_Sem_Unit)) (1 .. 3) /= "a-n"
and then Nkind (Unit (Cunit (Current_Sem_Unit))) =
-- Case of from internal file
- if Is_Internal_File_Name (Fname) then
+ if In_Internal_Unit (E) then
-- Private part entities in internal files are never considered
-- to be known to the writer of normal application code.
Nvis_Messages;
goto Done;
- elsif Is_Predefined_File_Name (Unit_File_Name (Current_Sem_Unit))
- then
+ elsif Is_Predefined_Unit (Current_Sem_Unit) then
-- A use-clause in the body of a system file creates conflict
-- with some entity in a user scope, while rtsfind is active.
-- Keep only the entity coming from another predefined unit.
E2 := E;
while Present (E2) loop
- if Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Sloc (E2))))
- then
+ if In_Predefined_Unit (E2) then
E := E2;
goto Found;
end if;
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Errout; use Errout;
with Exp_Ch9; use Exp_Ch9;
with Elists; use Elists;
-with Fname; use Fname;
with Freeze; use Freeze;
with Layout; use Layout;
with Lib; use Lib;
-- implemented.
if In_Private_Part (Current_Scope)
- and then Is_Internal_File_Name (Unit_File_Name (Current_Sem_Unit))
+ and then Is_Internal_Unit (Current_Sem_Unit)
then
Set_Has_Protected (T, False);
else
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
with Expander; use Expander;
-with Fname; use Fname;
with Lib; use Lib;
with Lib.Load; use Lib.Load;
with Namet; use Namet;
-- Check cases of internal units
- Callee_Unit_Internal :=
- Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (E_Scope)));
+ Callee_Unit_Internal := In_Internal_Unit (E_Scope);
-- Do not give a warning if the with'ed unit is internal and this is
-- the generic instantiation case (this saves a lot of hassle dealing
if C_Scope = Standard_Standard then
Caller_Unit_Internal := False;
else
- Caller_Unit_Internal :=
- Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (C_Scope)));
+ Caller_Unit_Internal := In_Internal_Unit (C_Scope);
end if;
-- Do not give a warning if the with'ed unit is internal and the caller
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Atree; use Atree;
with Einfo; use Einfo;
with Errout; use Errout;
-with Fname; use Fname;
with Lib; use Lib;
with Namet; use Namet;
with Opt; use Opt;
elsif not Comes_From_Source (E)
or else not Comes_From_Source (N)
- or else Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (N)))
+ or else In_Predefined_Unit (N)
then
null;
with Exp_Ch7; use Exp_Ch7;
with Exp_Tss; use Exp_Tss;
with Exp_Util; use Exp_Util;
-with Fname; use Fname;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
function Comes_From_Predefined_Lib_Unit (Nod : Node_Id) return Boolean is
begin
return
- Sloc (Nod) = Standard_Location
- or else Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Sloc (Nod))));
+ Sloc (Nod) = Standard_Location or else In_Predefined_Unit (Nod);
end Comes_From_Predefined_Lib_Unit;
--------------------
begin
if Present (Init)
and then Comes_From_Source (Init)
- and then not
- Is_Predefined_File_Name
- (File_Name (Get_Source_File_Index (Sloc (Init))))
+ and then not In_Predefined_Unit (Init)
then
return True;
return
Nam_In (Chars (Iter_Typ), Name_Forward_Iterator,
Name_Reversible_Iterator)
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Root_Type (Iter_Typ))));
+ and then In_Predefined_Unit (Root_Type (Iter_Typ));
end Denotes_Iterator;
-- Local variables
begin
if Is_Class_Wide_Type (Typ)
and then Chars (Root_Type (Typ)) = Name_Reversible_Iterator
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Root_Type (Typ))))
+ and then In_Predefined_Unit (Root_Type (Typ))
then
return True;
while Present (Iface_Elmt) loop
Iface := Node (Iface_Elmt);
if Chars (Iface) = Name_Reversible_Iterator
- and then
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Iface)))
+ and then In_Predefined_Unit (Iface)
then
return True;
end if;
return
Chars (Par) = Name_Unchecked_Conversion
and then Is_Intrinsic_Subprogram (Par)
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Par)));
+ and then In_Predefined_Unit (Par);
else
return
Present (Alias (Id))
then
return;
- elsif In_Inlined_Body
- and then Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Sloc (T))))
- then
+ elsif In_Inlined_Body and then In_Predefined_Unit (T) then
Set_Needs_Debug_Info (T, False);
end if;
with Einfo; use Einfo;
with Errout; use Errout;
with Exp_Code; use Exp_Code;
-with Fname; use Fname;
with Lib; use Lib;
with Lib.Xref; use Lib.Xref;
with Namet; use Namet;
-- (these would be junk warnings for an applications program,
-- since they refer to problems in internal units).
- if GNAT_Mode
- or else not Is_Internal_File_Name
- (Unit_File_Name (Get_Source_Unit (E1)))
- then
+ if GNAT_Mode or else not In_Internal_Unit (E1) then
-- We do not immediately flag the error. This is because we
-- have not expanded generic bodies yet, and they may have
-- the missing reference. So instead we park the entity on a
-- clearly undesirable.
elsif Configurable_Run_Time_Mode
- and then Is_Predefined_File_Name (Unit_File_Name (Unit))
+ and then Is_Predefined_Unit (Unit)
then
return;
end if;
-- (these would be junk warnings for an application program,
-- since they refer to problems in internal units).
- if GNAT_Mode
- or else not Is_Internal_File_Name (Unit_File_Name (Unit))
- then
+ if GNAT_Mode or else not Is_Internal_Unit (Unit) then
-- Here we definitely have a non-referenced unit. If it
-- is the special call for a spec unit, then just set the
-- flag to be read later.
-- Do not consider internal files to allow for various assertions and
-- safeguards within our runtime.
- and then not Is_Internal_File_Name
- (Unit_File_Name (Get_Source_Unit (Op)))
+ and then not In_Internal_Unit (Op)
then
Test_Comparison
(Op => Op,
-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
with Csets; use Csets;
with Debug; use Debug;
with Einfo; use Einfo;
-with Fname; use Fname;
with Lib; use Lib;
with Namet; use Namet;
with Nlists; use Nlists;
Ent : constant Entity_Id := Entity (N);
begin
if not In_Extended_Main_Source_Unit (Ent)
- and then
- Is_Predefined_File_Name
- (Unit_File_Name (Get_Source_Unit (Ent)))
+ and then In_Predefined_Unit (Ent)
then
-- Run-time routine name, output name with a preceding dollar
-- making sure that we do not get a line split between them.
-- --
-- B o d y --
-- --
--- Copyright (C) 1999-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1999-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
Warn_On_Overlap := Setting;
Warn_On_Overridden_Size := Setting;
Warn_On_Parameter_Order := Setting;
+ Warn_On_Questionable_Layout := Setting;
Warn_On_Questionable_Missing_Parens := Setting;
Warn_On_Record_Holes := Setting;
Warn_On_Redundant_Constructs := Setting;
W.Warn_On_Overridden_Size;
Warn_On_Parameter_Order :=
W.Warn_On_Parameter_Order;
+ Warn_On_Questionable_Layout :=
+ W.Warn_On_Questionable_Layout;
Warn_On_Questionable_Missing_Parens :=
W.Warn_On_Questionable_Missing_Parens;
Warn_On_Record_Holes :=
Warn_On_Overridden_Size;
W.Warn_On_Parameter_Order :=
Warn_On_Parameter_Order;
+ W.Warn_On_Questionable_Layout :=
+ Warn_On_Questionable_Layout;
W.Warn_On_Questionable_Missing_Parens :=
Warn_On_Questionable_Missing_Parens;
W.Warn_On_Record_Holes :=
when 'P' =>
Warn_On_Parameter_Order := False;
+ when 'q' =>
+ Warn_On_Questionable_Layout := True;
+
+ when 'Q' =>
+ Warn_On_Questionable_Layout := False;
+
when 'r' =>
Warn_On_Object_Renames_Function := True;
-- --
-- S p e c --
-- --
--- Copyright (C) 1999-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1999-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- Warn when tagged type public primitives are defined after its private
-- extensions.
- Warn_On_Record_Holes : Boolean := False;
- -- Warn when explicit record component clauses leave uncovered holes (gaps)
- -- in a record layout. Off by default, set by -gnatw.h (but not -gnatwa).
-
Warn_On_Overridden_Size : Boolean := False;
-- Warn when explicit record component clause or array component_size
-- clause specifies a size that overrides a size for the type which was
-- set with an explicit size clause. Off by default, modified by use of
-- -gnatw.s/.S (but not -gnatwa).
+ Warn_On_Questionable_Layout : Boolean := False;
+ -- Warn when default layout of a record type is questionable for run-time
+ -- efficiency reasons and would be improved by reordering the components.
+ -- Off by default, modified by use of -gnatw.q/.Q (but not -gnatwa).
+
+ Warn_On_Record_Holes : Boolean := False;
+ -- Warn when explicit record component clauses leave uncovered holes (gaps)
+ -- in a record layout. Off by default, set by -gnatw.h (but not -gnatwa).
+
Warn_On_Size_Alignment : Boolean := True;
-- Warn when explicit Size and Alignment clauses are given for a type, and
-- the size is not a multiple of the alignment. Off by default, modified
Warn_On_Overlap : Boolean;
Warn_On_Overridden_Size : Boolean;
Warn_On_Parameter_Order : Boolean;
+ Warn_On_Questionable_Layout : Boolean;
Warn_On_Questionable_Missing_Parens : Boolean;
Warn_On_Record_Holes : Boolean;
Warn_On_Redundant_Constructs : Boolean;
projects / gcc.git / commitdiff