From 8ab31c0c31ecf1fa368974dc98196955cb2c25cd Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 27 Apr 2017 15:53:26 +0200 Subject: [PATCH] [multiple changes] 2017-04-27 Eric Botcazou * 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 * 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 * g-comlin.adb (Sort_Sections): remove useless test. 2017-04-27 Claire Dross * 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 * gnat1drv.adb: Code cleanup. 2017-04-27 Ed Schonberg * 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. From-SVN: r247338 --- gcc/ada/ChangeLog | 70 ++ gcc/ada/a-cfdlli.adb | 70 +- gcc/ada/a-cfdlli.ads | 37 +- gcc/ada/a-cfhama.adb | 33 + gcc/ada/a-cfhama.ads | 61 +- gcc/ada/a-cfhase.adb | 709 ++++++++++-------- gcc/ada/a-cfhase.ads | 1226 +++++++++++++++++++++++++++---- gcc/ada/a-cfinve.adb | 70 +- gcc/ada/a-cfinve.ads | 30 +- gcc/ada/a-cforma.adb | 17 + gcc/ada/a-cforma.ads | 94 ++- gcc/ada/a-cforse.adb | 526 +++++++++++--- gcc/ada/a-cforse.ads | 1636 ++++++++++++++++++++++++++++++++++++++---- gcc/ada/a-cofove.adb | 70 +- gcc/ada/a-cofove.ads | 30 +- gcc/ada/a-cofuma.ads | 12 +- gcc/ada/a-cofuse.adb | 30 + gcc/ada/a-cofuse.ads | 69 +- gcc/ada/errout.adb | 8 +- gcc/ada/exp_aggr.adb | 4 +- gcc/ada/exp_attr.adb | 3 +- gcc/ada/exp_code.adb | 7 +- gcc/ada/exp_util.adb | 12 +- gcc/ada/fe.h | 9 +- gcc/ada/fname.adb | 130 ++-- gcc/ada/fname.ads | 14 +- gcc/ada/freeze.adb | 3 +- gcc/ada/g-comlin.adb | 8 +- gcc/ada/gcc-interface/decl.c | 345 +++++++-- gcc/ada/gnat1drv.adb | 43 +- gcc/ada/inline.adb | 17 +- gcc/ada/lib-list.adb | 6 +- gcc/ada/lib-load.adb | 186 +++-- gcc/ada/lib-writ.adb | 109 +-- gcc/ada/lib.adb | 44 +- gcc/ada/lib.ads | 40 +- gcc/ada/par.adb | 6 +- gcc/ada/restrict.adb | 4 +- gcc/ada/rtsfind.adb | 6 +- gcc/ada/sem.adb | 7 +- gcc/ada/sem_cat.adb | 13 +- gcc/ada/sem_ch10.adb | 40 +- gcc/ada/sem_ch12.adb | 11 +- gcc/ada/sem_ch3.adb | 3 +- gcc/ada/sem_ch4.adb | 8 +- gcc/ada/sem_ch6.adb | 12 +- gcc/ada/sem_ch8.adb | 12 +- gcc/ada/sem_ch9.adb | 5 +- gcc/ada/sem_elab.adb | 7 +- gcc/ada/sem_intr.adb | 6 +- gcc/ada/sem_res.adb | 5 +- gcc/ada/sem_util.adb | 22 +- gcc/ada/sem_warn.adb | 15 +- gcc/ada/sprint.adb | 7 +- gcc/ada/warnsw.adb | 13 +- gcc/ada/warnsw.ads | 16 +- 56 files changed, 4680 insertions(+), 1316 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 30dbbfc..667d863 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,73 @@ +2017-04-27 Eric Botcazou + + * 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 + + * 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 + + * g-comlin.adb (Sort_Sections): remove useless test. + +2017-04-27 Claire Dross + + * 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 + + * gnat1drv.adb: Code cleanup. + +2017-04-27 Ed Schonberg + + * 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 * sinput.adb: Minor code cleanup. diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index 7e64133..0b4674d 100644 --- a/gcc/ada/a-cfdlli.adb +++ b/gcc/ada/a-cfdlli.adb @@ -847,6 +847,45 @@ is 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 -- --------------- @@ -867,37 +906,6 @@ is 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 -- ----------- diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 0bd57bf..e7b7ba7 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -1408,8 +1408,8 @@ is 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), @@ -1423,7 +1423,7 @@ is => 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) @@ -1463,8 +1463,8 @@ is 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), @@ -1478,7 +1478,7 @@ is => 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) @@ -1533,16 +1533,21 @@ is 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, diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb index 526a556..4351102 100644 --- a/gcc/ada/a-cfhama.adb +++ b/gcc/ada/a-cfhama.adb @@ -367,6 +367,39 @@ is 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 -- ---------- diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads index 533a3bf..dc60dc8 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -56,7 +56,9 @@ generic 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 @@ -117,6 +119,30 @@ is (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, @@ -137,7 +163,6 @@ is P_Left : P.Map; P_Right : P.Map) return Boolean with - Ghost, Global => null, Post => (if Mapping_Preserved'Result then @@ -146,6 +171,10 @@ is 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. @@ -179,11 +208,16 @@ is -- 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 (K.Get (Keys'Result, I), K.Get (Keys'Result, J)) @@ -259,7 +293,14 @@ is 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, @@ -278,8 +319,8 @@ is -- 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; @@ -355,8 +396,8 @@ is -- 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; @@ -700,7 +741,7 @@ is 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, @@ -709,6 +750,8 @@ is 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 diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb index cc900f35..f40fc2f 100644 --- a/gcc/ada/a-cfhase.adb +++ b/gcc/ada/a-cfhase.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -264,35 +264,6 @@ is 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 -- --------------------- @@ -521,83 +492,6 @@ is 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 -- --------------------- @@ -657,36 +551,221 @@ is 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 -- @@ -715,6 +794,190 @@ is 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 -- ----------------- @@ -1158,34 +1421,6 @@ is 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 -- -------------------------- @@ -1386,160 +1621,4 @@ is 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; diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads index 7ab1611..0f2be85 100644 --- a/gcc/ada/a-cfhase.ads +++ b/gcc/ada/a-cfhase.ads @@ -6,7 +6,7 @@ -- -- -- 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 -- @@ -45,16 +45,9 @@ -- 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 @@ -63,15 +56,10 @@ 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 @@ -82,58 +70,368 @@ is 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; @@ -141,11 +439,53 @@ is 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; @@ -153,120 +493,654 @@ is 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; @@ -282,59 +1156,171 @@ is 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); @@ -356,12 +1342,6 @@ private 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; diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb index e1a979d..4cb3227 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -641,6 +641,45 @@ is 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 -- --------------- @@ -658,37 +697,6 @@ is 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 -- ---------- diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index 98dcea1..e1bc30c 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -723,7 +723,7 @@ is 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) @@ -760,7 +760,7 @@ is 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 @@ -821,16 +821,22 @@ is 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, diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb index c54515b..a7dc514 100644 --- a/gcc/ada/a-cforma.adb +++ b/gcc/ada/a-cforma.adb @@ -514,6 +514,23 @@ is 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 -- ------------------------- diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads index 7999e2e..6b0597e 100644 --- a/gcc/ada/a-cforma.ads +++ b/gcc/ada/a-cforma.ads @@ -171,6 +171,16 @@ is 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, @@ -240,17 +250,16 @@ is -- 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 @@ -482,7 +491,7 @@ is -- 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 @@ -499,15 +508,14 @@ is (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) @@ -516,7 +524,7 @@ is 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; @@ -541,13 +549,12 @@ is -- 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 @@ -573,8 +580,7 @@ is -- 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 @@ -582,16 +588,14 @@ is (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) @@ -600,8 +604,7 @@ is 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; @@ -610,7 +613,7 @@ is with Global => null, Pre => Contains (Container, Key), - Post => + Post => -- Cursors are preserved @@ -618,12 +621,11 @@ is -- 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 @@ -668,17 +670,14 @@ is (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) @@ -687,9 +686,7 @@ is 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, @@ -715,16 +712,14 @@ is (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) @@ -733,8 +728,7 @@ is 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, @@ -960,29 +954,23 @@ is 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, diff --git a/gcc/ada/a-cforse.adb b/gcc/ada/a-cforse.adb index 42a8503..47e863b 100644 --- a/gcc/ada/a-cforse.adb +++ b/gcc/ada/a-cforse.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -360,34 +360,6 @@ is 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 -- ------------ @@ -596,36 +568,6 @@ is 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 -- ----------- @@ -644,6 +586,333 @@ is 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 -- ---------- @@ -807,6 +1076,116 @@ is 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 -- ------------------------- @@ -1441,35 +1820,6 @@ is 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 -- -------------------------- diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads index f7f03ca..6c1323d 100644 --- a/gcc/ada/a-cforse.ads +++ b/gcc/ada/a-cforse.ads @@ -6,7 +6,7 @@ -- -- -- 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 -- @@ -46,34 +46,28 @@ -- 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, @@ -83,44 +77,413 @@ is 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; @@ -128,11 +491,47 @@ is 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; @@ -140,147 +539,918 @@ is 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; @@ -292,68 +1462,300 @@ is 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); @@ -377,12 +1779,6 @@ private 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; diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb index 87c1d3d..63cbebb 100644 --- a/gcc/ada/a-cofove.adb +++ b/gcc/ada/a-cofove.adb @@ -636,6 +636,45 @@ is 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 -- --------------- @@ -655,37 +694,6 @@ is 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 -- ---------- diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index d9b68d0..681e513 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -717,7 +717,7 @@ is 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) @@ -754,7 +754,7 @@ is 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 @@ -815,16 +815,22 @@ is 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, diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 2b167b2..ea44dcf 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -35,7 +35,9 @@ private with Ada.Containers.Functional_Base; 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 @@ -53,8 +55,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is -- "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 -- @@ -89,8 +91,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is 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; diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb index e0ea2ff..22bf688 100644 --- a/gcc/ada/a-cofuse.adb +++ b/gcc/ada/a-cofuse.adb @@ -113,6 +113,17 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is 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 -- ------------ @@ -120,6 +131,25 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is 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 -- ------------------ diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index 0a998f3..87165d7 100644 --- a/gcc/ada/a-cofuse.ads +++ b/gcc/ada/a-cofuse.ads @@ -36,7 +36,7 @@ generic 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 @@ -45,7 +45,7 @@ generic 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, @@ -54,8 +54,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- "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 -- @@ -89,23 +89,23 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- 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 @@ -149,15 +149,45 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is (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 -- @@ -195,8 +225,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is 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); @@ -250,9 +279,13 @@ private 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; diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb index 6003223..f71cc88 100644 --- a/gcc/ada/errout.adb +++ b/gcc/ada/errout.adb @@ -35,7 +35,6 @@ with Csets; use Csets; 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; @@ -2708,9 +2707,7 @@ package body Errout is -- 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; @@ -2748,8 +2745,7 @@ package body Errout is 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"); diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 0cbbd01..460b1c1 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -37,7 +37,6 @@ with Exp_Ch7; use Exp_Ch7; 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; @@ -4532,8 +4531,7 @@ package body Exp_Aggr is 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; diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index 21a1771..b81e26c 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -39,7 +39,6 @@ with Exp_Pakd; use Exp_Pakd; 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; @@ -7749,7 +7748,7 @@ package body Exp_Attr is -- 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 diff --git a/gcc/ada/exp_code.adb b/gcc/ada/exp_code.adb index 6fbe544..a04d90d 100644 --- a/gcc/ada/exp_code.adb +++ b/gcc/ada/exp_code.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -26,7 +26,6 @@ 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; @@ -274,9 +273,7 @@ package body Exp_Code is -- 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; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 0c87e1f..056a034 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1116,9 +1116,15 @@ package body Exp_Util is -- 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; diff --git a/gcc/ada/fe.h b/gcc/ada/fe.h index 6d31ae1..48727c6 100644 --- a/gcc/ada/fe.h +++ b/gcc/ada/fe.h @@ -6,7 +6,7 @@ * * * 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- * @@ -219,6 +219,7 @@ extern void Check_Elaboration_Code_Allowed (Node_Id); 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); @@ -297,6 +298,12 @@ extern Boolean Signed_Zeros_On_Target; 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 diff --git a/gcc/ada/fname.adb b/gcc/ada/fname.adb index c75048b..2bdfbf6 100644 --- a/gcc/ada/fname.adb +++ b/gcc/ada/fname.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -99,21 +99,14 @@ package body Fname is 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; @@ -128,6 +121,29 @@ package body Fname is -- 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 @@ -149,27 +165,13 @@ package body Fname is (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; @@ -186,12 +188,6 @@ package body Fname is 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. @@ -205,7 +201,48 @@ package body Fname is -- 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 @@ -218,18 +255,15 @@ package body Fname is 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 -- diff --git a/gcc/ada/fname.ads b/gcc/ada/fname.ads index 9a72517..4c84598 100644 --- a/gcc/ada/fname.ads +++ b/gcc/ada/fname.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -79,6 +79,14 @@ package Fname is -- 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; @@ -88,6 +96,10 @@ package Fname is -- 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) diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index d18d3d4..8ce16cd 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -37,7 +37,6 @@ with Exp_Disp; use Exp_Disp; 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; @@ -8197,7 +8196,7 @@ package body Freeze is 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; diff --git a/gcc/ada/g-comlin.adb b/gcc/ada/g-comlin.adb index 978040e..dc27915 100644 --- a/gcc/ada/g-comlin.adb +++ b/gcc/ada/g-comlin.adb @@ -177,7 +177,7 @@ package body GNAT.Command_Line is -- 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 @@ -2792,7 +2792,7 @@ package body GNAT.Command_Line is ------------------- 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 @@ -2805,10 +2805,6 @@ package body GNAT.Command_Line is Index : Natural; begin - if Line = null then - return; - end if; - -- First construct a list of all sections for E in Line'Range loop diff --git a/gcc/ada/gcc-interface/decl.c b/gcc/ada/gcc-interface/decl.c index 35fd92f..0c9c78a 100644 --- a/gcc/ada/gcc-interface/decl.c +++ b/gcc/ada/gcc-interface/decl.c @@ -217,8 +217,9 @@ static bool constructor_address_p (tree); 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); @@ -3328,11 +3329,10 @@ gnat_to_gnu_entity (Entity_Id gnat_entity, tree gnu_expr, bool definition) } /* 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. */ @@ -7463,6 +7463,71 @@ compare_field_bitpos (const PTR rt1, const PTR rt2) 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 { @@ -7483,14 +7548,15 @@ 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. @@ -7514,8 +7580,6 @@ typedef struct vinfo 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. @@ -7525,12 +7589,12 @@ typedef struct vinfo 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; @@ -7539,24 +7603,21 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, 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 @@ -7603,7 +7664,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, } /* 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 @@ -7612,9 +7673,9 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, 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 @@ -7676,7 +7737,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, 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)) { @@ -7712,12 +7773,11 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, /* 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); @@ -7873,19 +7933,44 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_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 { \ @@ -7898,6 +7983,7 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, (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); @@ -7908,19 +7994,6 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, 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; @@ -7934,6 +8007,129 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, 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; } @@ -7943,15 +8139,30 @@ components_to_record (tree gnu_record_type, Node_Id gnat_component_list, /* 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. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index 863f227..8da1c50 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -500,26 +500,29 @@ procedure Gnat1drv is -- 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 diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 0b9affd..a5b1d98 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -410,8 +410,7 @@ package body Inline is 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; @@ -1556,7 +1555,7 @@ package body Inline is -- 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; @@ -1602,7 +1601,7 @@ package body Inline is -- 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; @@ -1617,9 +1616,7 @@ package body Inline is 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; @@ -2283,8 +2280,7 @@ package body Inline is 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)); @@ -3565,8 +3561,7 @@ package body Inline is 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; diff --git a/gcc/ada/lib-list.adb b/gcc/ada/lib-list.adb index 831dc90..a856b14 100644 --- a/gcc/ada/lib-list.adb +++ b/gcc/ada/lib-list.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -78,9 +78,7 @@ begin 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; diff --git a/gcc/ada/lib-load.adb b/gcc/ada/lib-load.adb index dc8deb5..e05bde1 100644 --- a/gcc/ada/lib-load.adb +++ b/gcc/ada/lib-load.adb @@ -145,7 +145,15 @@ package body Lib.Load is 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 @@ -205,29 +213,35 @@ package body Lib.Load is 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); @@ -285,7 +299,13 @@ package body Lib.Load is ---------------------- 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 @@ -299,7 +319,6 @@ package body Lib.Load is -- 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; @@ -311,29 +330,35 @@ package body Lib.Load is 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; @@ -356,6 +381,9 @@ package body Lib.Load is 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; @@ -467,7 +495,11 @@ package body Lib.Load is 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; @@ -676,29 +708,35 @@ package body Lib.Load is -- 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 @@ -880,7 +918,7 @@ package body Lib.Load is -- 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; diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index f69e4ac..895e185 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -74,28 +74,32 @@ package body Lib.Writ is 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; ------------------------------ @@ -130,29 +134,33 @@ package body Lib.Writ is 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 @@ -533,7 +541,7 @@ package body Lib.Writ is 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"); @@ -618,8 +626,7 @@ package body Lib.Writ is -- 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; @@ -858,7 +865,7 @@ package body Lib.Writ is 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 @@ -1160,9 +1167,7 @@ package body Lib.Writ is 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); diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb index cce586c..16c8afc 100644 --- a/gcc/ada/lib.adb +++ b/gcc/ada/lib.adb @@ -36,7 +36,6 @@ pragma Style_Checks (All_Checks); 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; @@ -127,6 +126,21 @@ package body Lib is 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; @@ -576,7 +590,7 @@ package body Lib is -- 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 @@ -585,9 +599,7 @@ package body Lib is -- 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; ----------------------------- @@ -904,12 +916,25 @@ package body Lib is 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 -- ------------------------ @@ -921,9 +946,8 @@ package body Lib is 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; ----------------------- diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads index 54480e4..a5b9858 100644 --- a/gcc/ada/lib.ads +++ b/gcc/ada/lib.ads @@ -327,6 +327,19 @@ package Lib is -- 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 @@ -428,6 +441,9 @@ package Lib is 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; @@ -493,7 +509,7 @@ package Lib is -- 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 @@ -597,13 +613,20 @@ package Lib is -- 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 @@ -776,6 +799,9 @@ private 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); @@ -811,6 +837,11 @@ private 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 @@ -840,9 +871,14 @@ private 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 ( diff --git a/gcc/ada/par.adb b/gcc/ada/par.adb index 863149b..4145907 100644 --- a/gcc/ada/par.adb +++ b/gcc/ada/par.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -1526,8 +1526,8 @@ begin 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 diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index a66fffb..07df8ca 100644 --- a/gcc/ada/restrict.adb +++ b/gcc/ada/restrict.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -1763,7 +1763,7 @@ package body Restrict is -- 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; diff --git a/gcc/ada/rtsfind.adb b/gcc/ada/rtsfind.adb index faeffd2..8bedff6 100644 --- a/gcc/ada/rtsfind.adb +++ b/gcc/ada/rtsfind.adb @@ -469,9 +469,7 @@ package body Rtsfind is -- 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); @@ -1626,7 +1624,7 @@ package body Rtsfind is 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 diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index f277e03..35d0d48 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -29,7 +29,6 @@ with Debug_A; use Debug_A; 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; @@ -1425,8 +1424,8 @@ package body Sem is -- 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; @@ -1474,7 +1473,7 @@ package body Sem is 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 diff --git a/gcc/ada/sem_cat.adb b/gcc/ada/sem_cat.adb index 9212783..82c4a6a 100644 --- a/gcc/ada/sem_cat.adb +++ b/gcc/ada/sem_cat.adb @@ -29,7 +29,6 @@ with Einfo; use Einfo; 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; @@ -263,8 +262,8 @@ package body Sem_Cat is -- 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; @@ -949,8 +948,7 @@ package body Sem_Cat is 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); @@ -1098,8 +1096,7 @@ package body Sem_Cat is 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)) @@ -2202,7 +2199,7 @@ package body Sem_Cat is 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)) diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb index c4ae58a..1f6b237 100644 --- a/gcc/ada/sem_ch10.adb +++ b/gcc/ada/sem_ch10.adb @@ -648,9 +648,7 @@ package body Sem_Ch10 is 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 @@ -919,13 +917,9 @@ package body Sem_Ch10 is -- 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 @@ -1230,7 +1224,7 @@ package body Sem_Ch10 is -- 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 @@ -2524,18 +2518,10 @@ package body Sem_Ch10 is -- 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 @@ -2566,7 +2552,7 @@ package body Sem_Ch10 is -- 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 @@ -2598,7 +2584,7 @@ package body Sem_Ch10 is 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 @@ -3537,7 +3523,7 @@ package body Sem_Ch10 is -- 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 @@ -5276,7 +5262,7 @@ package body Sem_Ch10 is -- 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 diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 17b559c..1431441 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -4109,8 +4109,7 @@ package body Sem_Ch12 is -- 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 @@ -11210,8 +11209,7 @@ package body Sem_Ch12 is -- 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 @@ -15473,10 +15471,7 @@ package body Sem_Ch12 is -- 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 diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 342e1de..bf92e7d 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -38,7 +38,6 @@ with Exp_Disp; use Exp_Disp; 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; @@ -3266,7 +3265,7 @@ package body Sem_Ch3 is 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)); diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 8da266a..41e6ca5 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -30,7 +30,6 @@ with Einfo; use Einfo; 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; @@ -3483,9 +3482,7 @@ package body Sem_Ch4 is 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); @@ -7351,8 +7348,7 @@ package body Sem_Ch4 is -- 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; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 9ba68b1..45a71aa 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -39,7 +39,6 @@ with Exp_Dbug; use Exp_Dbug; 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; @@ -3308,8 +3307,7 @@ package body Sem_Ch6 is 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); @@ -6156,9 +6154,7 @@ package body Sem_Ch6 is 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)))); @@ -6243,9 +6239,7 @@ package body Sem_Ch6 is 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 diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 0a7f204..03a21c2 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -31,7 +31,6 @@ with Errout; use Errout; 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; @@ -3644,7 +3643,7 @@ package body Sem_Ch8 is -- 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))) = @@ -4968,7 +4967,7 @@ package body Sem_Ch8 is -- 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. @@ -5551,17 +5550,14 @@ package body Sem_Ch8 is 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; diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 7233f2b..25e9cbd 100644 --- a/gcc/ada/sem_ch9.adb +++ b/gcc/ada/sem_ch9.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -32,7 +32,6 @@ with Einfo; use Einfo; 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; @@ -2024,7 +2023,7 @@ package body Sem_Ch9 is -- 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 diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb index 2579ab5..0588c61 100644 --- a/gcc/ada/sem_elab.adb +++ b/gcc/ada/sem_elab.adb @@ -32,7 +32,6 @@ with Errout; use Errout; 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; @@ -910,8 +909,7 @@ package body Sem_Elab is -- 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 @@ -924,8 +922,7 @@ package body Sem_Elab is 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 diff --git a/gcc/ada/sem_intr.adb b/gcc/ada/sem_intr.adb index c038dc4..ad8c388 100644 --- a/gcc/ada/sem_intr.adb +++ b/gcc/ada/sem_intr.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -28,7 +28,6 @@ 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; @@ -339,8 +338,7 @@ package body Sem_Intr is 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; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 257237e..091a800 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -35,7 +35,6 @@ with Exp_Ch6; use Exp_Ch6; 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; @@ -1895,9 +1894,7 @@ package body Sem_Res is 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; -------------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1a3b042..f1a414f 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13482,9 +13482,7 @@ package body Sem_Util is 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; @@ -13771,8 +13769,7 @@ package body Sem_Util is 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 @@ -15069,8 +15066,7 @@ package body Sem_Util is 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; @@ -15084,9 +15080,7 @@ package body Sem_Util is 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; @@ -15597,8 +15591,7 @@ package body Sem_Util is 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)) @@ -20982,10 +20975,7 @@ package body Sem_Util is 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; diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb index 29d0a9d..c181072 100644 --- a/gcc/ada/sem_warn.adb +++ b/gcc/ada/sem_warn.adb @@ -28,7 +28,6 @@ with Debug; use Debug; 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; @@ -1612,10 +1611,7 @@ package body Sem_Warn is -- (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 @@ -2383,7 +2379,7 @@ package body Sem_Warn is -- 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; @@ -2414,9 +2410,7 @@ package body Sem_Warn is -- (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. @@ -3302,8 +3296,7 @@ package body Sem_Warn is -- 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, diff --git a/gcc/ada/sprint.adb b/gcc/ada/sprint.adb index f10ff03..85908cb 100644 --- a/gcc/ada/sprint.adb +++ b/gcc/ada/sprint.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -29,7 +29,6 @@ with Casing; use Casing; 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; @@ -4806,9 +4805,7 @@ package body Sprint is 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. diff --git a/gcc/ada/warnsw.adb b/gcc/ada/warnsw.adb index 1c0995c..013ea10 100644 --- a/gcc/ada/warnsw.adb +++ b/gcc/ada/warnsw.adb @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -75,6 +75,7 @@ package body Warnsw is 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; @@ -166,6 +167,8 @@ package body Warnsw is 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 := @@ -270,6 +273,8 @@ package body Warnsw is 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 := @@ -394,6 +399,12 @@ package body Warnsw is 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; diff --git a/gcc/ada/warnsw.ads b/gcc/ada/warnsw.ads index 9b6313a..4afb8b1 100644 --- a/gcc/ada/warnsw.ads +++ b/gcc/ada/warnsw.ads @@ -6,7 +6,7 @@ -- -- -- 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- -- @@ -42,16 +42,21 @@ package Warnsw is -- 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 @@ -104,6 +109,7 @@ package Warnsw is 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; -- 2.7.4