diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 19 | ||||
| -rw-r--r-- | gcc/ada/a-cbmutr.adb | 75 | ||||
| -rw-r--r-- | gcc/ada/a-cbmutr.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/a-cimutr.adb | 75 | ||||
| -rw-r--r-- | gcc/ada/a-cimutr.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/a-comutr.ads | 6 | ||||
| -rw-r--r-- | gcc/ada/debug.adb | 5 | ||||
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 18 | ||||
| -rw-r--r-- | gcc/ada/opt.ads | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 97 |
10 files changed, 245 insertions, 65 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e44f19a9aac..8346b6b96eb 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,24 @@ 2011-09-27 Robert Dewar <dewar@adacore.com> + * a-comutr.ads: Minor reformatting. + +2011-09-27 Ed Schonberg <schonberg@adacore.com> + + * a-cimutr.adb, a-cimutr.ads, a-cbmutr.adb, a-cbmutr.ads: Add children + iterators to multiway trees. + +2011-09-27 Yannick Moy <moy@adacore.com> + + * debug.adb (d.D): New option for strict Alfa mode. + * opt.ads (Strict_Alfa_Mode): New flag to interpret compiler + permissions as strictly as possible. + * sem_ch3.adb (Signed_Integer_Type_Declaration): In non-strict + Alfa mode, now, interpret ranges of base types like GNAT does; in + strict mode, simply change the range of the implicit base Itype. + * gnat1drv.adb: Update comments. Set Strict_Alfa_Mode. + +2011-09-27 Robert Dewar <dewar@adacore.com> + * exp_ch9.adb: Minor comment fixes. 2011-09-27 Ed Schonberg <schonberg@adacore.com> diff --git a/gcc/ada/a-cbmutr.adb b/gcc/ada/a-cbmutr.adb index 8e6c148e914..f4bdc5e4035 100644 --- a/gcc/ada/a-cbmutr.adb +++ b/gcc/ada/a-cbmutr.adb @@ -40,10 +40,29 @@ package body Ada.Containers.Bounded_Multiway_Trees is end record; overriding function First (Object : Iterator) return Cursor; + overriding function Next (Object : Iterator; Position : Cursor) return Cursor; + type Child_Iterator is new Tree_Iterator_Interfaces.Reversible_Iterator with + record + Container : Tree_Access; + Position : Cursor; + end record; + + overriding function First (Object : Child_Iterator) return Cursor; + + overriding function Next + (Object : Child_Iterator; + Position : Cursor) return Cursor; + + overriding function Previous + (Object : Child_Iterator; + Position : Cursor) return Cursor; + + overriding function Last (Object : Child_Iterator) return Cursor; + ----------------------- -- Local Subprograms -- ----------------------- @@ -1241,6 +1260,14 @@ package body Ada.Containers.Bounded_Multiway_Trees is return Object.Position; end First; + function First (Object : Child_Iterator) return Cursor is + Node : Count_Type'Base; + + begin + Node := Object.Container.Nodes (Object.Position.Node).Children.First; + return (Object.Container, Node); + end First; + ----------------- -- First_Child -- ----------------- @@ -1809,6 +1836,16 @@ package body Ada.Containers.Bounded_Multiway_Trees is end loop; end Iterate_Children; + function Iterate_Children + (Container : Tree; + Parent : Cursor) + return Tree_Iterator_Interfaces.Reversible_Iterator'Class + is + pragma Unreferenced (Container); + begin + return Child_Iterator'(Parent.Container, Parent); + end Iterate_Children; + --------------------- -- Iterate_Subtree -- --------------------- @@ -1871,6 +1908,15 @@ package body Ada.Containers.Bounded_Multiway_Trees is Iterate_Children (Container, Subtree, Process); end Iterate_Subtree; + ---------- + -- Last -- + ---------- + + overriding function Last (Object : Child_Iterator) return Cursor is + begin + return Last_Child (Object.Position); + end Last; + ---------------- -- Last_Child -- ---------------- @@ -1992,6 +2038,19 @@ package body Ada.Containers.Bounded_Multiway_Trees is end if; end Next; + function Next + (Object : Child_Iterator; + Position : Cursor) return Cursor + is + + begin + if Object.Container /= Position.Container then + raise Program_Error; + end if; + + return Next_Sibling (Position); + end Next; + ------------------ -- Next_Sibling -- ------------------ @@ -2137,6 +2196,22 @@ package body Ada.Containers.Bounded_Multiway_Trees is Container.Count := Container.Count + Count; end Prepend_Child; + -------------- + -- Previous -- + -------------- + + overriding function Previous + (Object : Child_Iterator; + Position : Cursor) return Cursor + is + begin + if Object.Container /= Position.Container then + raise Program_Error; + end if; + + return Previous_Sibling (Position); + end Previous; + ---------------------- -- Previous_Sibling -- ---------------------- diff --git a/gcc/ada/a-cbmutr.ads b/gcc/ada/a-cbmutr.ads index 6d6c6f3f4de..e014f82d453 100644 --- a/gcc/ada/a-cbmutr.ads +++ b/gcc/ada/a-cbmutr.ads @@ -179,6 +179,11 @@ package Ada.Containers.Bounded_Multiway_Trees is function Iterate_Subtree (Position : Cursor) return Tree_Iterator_Interfaces.Forward_Iterator'Class; + function Iterate_Children + (Container : Tree; + Parent : Cursor) + return Tree_Iterator_Interfaces.Reversible_Iterator'Class; + function Child_Count (Parent : Cursor) return Count_Type; function Child_Depth (Parent, Child : Cursor) return Count_Type; diff --git a/gcc/ada/a-cimutr.adb b/gcc/ada/a-cimutr.adb index 6b9d7b6b2f1..2fdc8a75469 100644 --- a/gcc/ada/a-cimutr.adb +++ b/gcc/ada/a-cimutr.adb @@ -39,11 +39,28 @@ package body Ada.Containers.Indefinite_Multiway_Trees is From_Root : Boolean; end record; + type Child_Iterator is new Tree_Iterator_Interfaces.Reversible_Iterator with + record + Container : Tree_Access; + Position : Cursor; + end record; + overriding function First (Object : Iterator) return Cursor; overriding function Next (Object : Iterator; Position : Cursor) return Cursor; + overriding function First (Object : Child_Iterator) return Cursor; + overriding function Next + (Object : Child_Iterator; + Position : Cursor) return Cursor; + + overriding function Previous + (Object : Child_Iterator; + Position : Cursor) return Cursor; + + overriding function Last (Object : Child_Iterator) return Cursor; + ----------------------- -- Local Subprograms -- ----------------------- @@ -936,6 +953,11 @@ package body Ada.Containers.Indefinite_Multiway_Trees is return Object.Position; end First; + function First (Object : Child_Iterator) return Cursor is + begin + return (Object.Container, Object.Position.Node.Children.First); + end First; + ----------------- -- First_Child -- ----------------- @@ -1369,6 +1391,16 @@ package body Ada.Containers.Indefinite_Multiway_Trees is end loop; end Iterate_Children; + function Iterate_Children + (Container : Tree; + Parent : Cursor) + return Tree_Iterator_Interfaces.Reversible_Iterator'Class + is + pragma Unreferenced (Container); + begin + return Child_Iterator'(Parent.Container, Parent); + end Iterate_Children; + --------------------- -- Iterate_Subtree -- --------------------- @@ -1425,6 +1457,15 @@ package body Ada.Containers.Indefinite_Multiway_Trees is Iterate_Children (Container, Subtree, Process); end Iterate_Subtree; + ---------- + -- Last -- + ---------- + + overriding function Last (Object : Child_Iterator) return Cursor is + begin + return (Object.Container, Object.Position.Node.Children.Last); + end Last; + ---------------- -- Last_Child -- ---------------- @@ -1551,6 +1592,21 @@ package body Ada.Containers.Indefinite_Multiway_Trees is end if; end Next; + function Next + (Object : Child_Iterator; + Position : Cursor) return Cursor + is + C : constant Tree_Node_Access := Position.Node.Next; + + begin + if C = null then + return No_Element; + + else + return (Object.Container, C); + end if; + end Next; + ------------------ -- Next_Sibling -- ------------------ @@ -1673,6 +1729,25 @@ package body Ada.Containers.Indefinite_Multiway_Trees is Container.Count := Container.Count + Count; end Prepend_Child; + -------------- + -- Previous -- + -------------- + + overriding function Previous + (Object : Child_Iterator; + Position : Cursor) return Cursor + is + C : constant Tree_Node_Access := Position.Node.Prev; + + begin + if C = null then + return No_Element; + + else + return (Object.Container, C); + end if; + end Previous; + ---------------------- -- Previous_Sibling -- ---------------------- diff --git a/gcc/ada/a-cimutr.ads b/gcc/ada/a-cimutr.ads index 141ced0e47a..29be8ca39ea 100644 --- a/gcc/ada/a-cimutr.ads +++ b/gcc/ada/a-cimutr.ads @@ -181,6 +181,11 @@ package Ada.Containers.Indefinite_Multiway_Trees is function Iterate_Subtree (Position : Cursor) return Tree_Iterator_Interfaces.Forward_Iterator'Class; + function Iterate_Children + (Container : Tree; + Parent : Cursor) + return Tree_Iterator_Interfaces.Reversible_Iterator'Class; + function Child_Count (Parent : Cursor) return Count_Type; function Child_Depth (Parent, Child : Cursor) return Count_Type; diff --git a/gcc/ada/a-comutr.ads b/gcc/ada/a-comutr.ads index 94cacfc9f1b..b035e1637fe 100644 --- a/gcc/ada/a-comutr.ads +++ b/gcc/ada/a-comutr.ads @@ -171,8 +171,8 @@ package Ada.Containers.Multiway_Trees is Process : not null access procedure (Position : Cursor)); procedure Iterate_Subtree - (Position : Cursor; - Process : not null access procedure (Position : Cursor)); + (Position : Cursor; + Process : not null access procedure (Position : Cursor)); function Iterate (Container : Tree) return Tree_Iterator_Interfaces.Forward_Iterator'Class; @@ -183,7 +183,7 @@ package Ada.Containers.Multiway_Trees is function Iterate_Children (Container : Tree; Parent : Cursor) - return Tree_Iterator_Interfaces.Reversible_Iterator'Class; + return Tree_Iterator_Interfaces.Reversible_Iterator'Class; function Child_Count (Parent : Cursor) return Count_Type; diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb index 2e565b94054..b3eb5cfd8e8 100644 --- a/gcc/ada/debug.adb +++ b/gcc/ada/debug.adb @@ -121,7 +121,7 @@ package body Debug is -- d.A Read/write Aspect_Specifications hash table to tree -- d.B -- d.C Generate concatenation call, do not generate inline code - -- d.D + -- d.D Strict Alfa mode -- d.E Force Alfa mode for gnat2why -- d.F Alfa mode -- d.G Precondition only mode for gnat2why @@ -580,6 +580,9 @@ package body Debug is -- d.C Generate call to System.Concat_n.Str_Concat_n routines in cases -- where we would normally generate inline concatenation code. + -- d.D Strict Alfa mode. Interpret compiler permissions as strictly as + -- possible in Alfa mode. + -- d.E Force Alfa mode for gnat2why. In this mode, errors are issued for -- all violations of Alfa in user code, and warnings are issued for -- constructs not yet implemented in gnat2why. diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index bf811eb5fb5..57456cc67ff 100644 --- a/gcc/ada/gnat1drv.adb +++ b/gcc/ada/gnat1drv.adb @@ -392,6 +392,12 @@ procedure Gnat1drv is Alfa_Mode := True; + -- Set strict standard interpretation of compiler permissions + + if Debug_Flag_Dot_DD then + Strict_Alfa_Mode := True; + end if; + -- Turn off inlining, which would confuse formal verification output -- and gain nothing. @@ -428,6 +434,8 @@ procedure Gnat1drv is Debug_Generated_Code := False; -- Turn cross-referencing on in case it was disabled (e.g. by -gnatD) + -- as it is needed for computing effects of subprograms in the formal + -- verification backend. Xref_Active := True; @@ -473,13 +481,15 @@ procedure Gnat1drv is Warning_Mode := Suppress; - -- Suppress the generation of name tables for enumerations - -- why??? + -- Suppress the generation of name tables for enumerations, which are + -- not needed for formal verification, and fall outside the Alfa + -- subset (use of pointers). Global_Discard_Names := True; - -- Suppress the expansion of tagged types and dispatching calls - -- why??? + -- Suppress the expansion of tagged types and dispatching calls, + -- which lead to the generation of non-Alfa code (use of pointers), + -- which is more complex to formally verify than the original source. Tagged_Type_Expansion := False; end if; diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads index b84e4ec1adb..65a2d17b8e0 100644 --- a/gcc/ada/opt.ads +++ b/gcc/ada/opt.ads @@ -1883,6 +1883,11 @@ package Opt is -- generation of Why code for those parts of the input code that belong to -- the Alfa subset of Ada. Set by debug flag -gnatd.F. + Strict_Alfa_Mode : Boolean := False; + -- Interpret compiler permissions as strictly as possible. E.g. base ranges + -- for integers are limited to the strict minimum with this option. Set by + -- debug flag -gnatd.D. + function Full_Expander_Active return Boolean; pragma Inline (Full_Expander_Active); -- Returns the value of (Expander_Active and not Alfa_Mode). This "flag" diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 8802ae52077..dd48cff4d17 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -19792,7 +19792,6 @@ package body Sem_Ch3 is -- Complete both implicit base and declared first subtype entities Set_Etype (Implicit_Base, Base_Typ); - Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ)); Set_Size_Info (Implicit_Base, (Base_Typ)); Set_RM_Size (Implicit_Base, RM_Size (Base_Typ)); Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Base_Typ)); @@ -19800,80 +19799,64 @@ package body Sem_Ch3 is Set_Ekind (T, E_Signed_Integer_Subtype); Set_Etype (T, Implicit_Base); - -- In formal verification mode, override partially the decisions above - -- to restrict base type's range to the minimum allowed by RM 3.5.4, - -- namely the smallest symmetric range around zero with a possible extra - -- negative value that contains the subtype range. Keep Size, RM_Size - -- and First_Rep_Item info, which should not be relied upon in formal - -- verification. - - if Alfa_Mode then - - -- If the range of the type is already symmetric with a possible - -- extra negative value, leave it this way. - - if UI_Le (Lo_Val, Hi_Val) - and then (UI_Eq (Lo_Val, UI_Negate (Hi_Val)) - or else - UI_Eq (Lo_Val, UI_Sub (UI_Negate (Hi_Val), Uint_1))) - then - null; + -- In formal verification mode, restrict the base type's range to the + -- minimum allowed by RM 3.5.4, namely the smallest symmetric range + -- around zero with a possible extra negative value that contains the + -- subtype range. Keep Size, RM_Size and First_Rep_Item info, which + -- should not be relied upon in formal verification. - else - declare - Sym_Hi_Val : Uint; - Sym_Lo_Val : Uint; - Decl : Node_Id; - Dloc : constant Source_Ptr := Sloc (Def); - Lbound : Node_Id; - Ubound : Node_Id; + if Strict_Alfa_Mode then + declare + Sym_Hi_Val : Uint; + Sym_Lo_Val : Uint; + Dloc : constant Source_Ptr := Sloc (Def); + Lbound : Node_Id; + Ubound : Node_Id; + Bounds : Node_Id; - begin - -- If the subtype range is empty, the smallest base type range - -- is the symmetric range around zero containing Lo_Val and - -- Hi_Val. + begin + -- If the subtype range is empty, the smallest base type range + -- is the symmetric range around zero containing Lo_Val and + -- Hi_Val. - if UI_Gt (Lo_Val, Hi_Val) then - Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val)); - Sym_Lo_Val := UI_Negate (Sym_Hi_Val); + if UI_Gt (Lo_Val, Hi_Val) then + Sym_Hi_Val := UI_Max (UI_Abs (Lo_Val), UI_Abs (Hi_Val)); + Sym_Lo_Val := UI_Negate (Sym_Hi_Val); -- Otherwise, if the subtype range is not empty and Hi_Val has -- the largest absolute value, Hi_Val is non negative and the -- smallest base type range is the symmetric range around zero -- containing Hi_Val. - elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then - Sym_Hi_Val := Hi_Val; - Sym_Lo_Val := UI_Negate (Hi_Val); + elsif UI_Le (UI_Abs (Lo_Val), UI_Abs (Hi_Val)) then + Sym_Hi_Val := Hi_Val; + Sym_Lo_Val := UI_Negate (Hi_Val); -- Otherwise, the subtype range is not empty, Lo_Val has the -- strictly largest absolute value, Lo_Val is negative and the -- smallest base type range is the symmetric range around zero -- with an extra negative value Lo_Val. - else - Sym_Lo_Val := Lo_Val; - Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1); - end if; + else + Sym_Lo_Val := Lo_Val; + Sym_Hi_Val := UI_Sub (UI_Negate (Lo_Val), Uint_1); + end if; - Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val); - Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val); - Set_Is_Static_Expression (Lbound); - Set_Is_Static_Expression (Ubound); + Lbound := Make_Integer_Literal (Dloc, Sym_Lo_Val); + Ubound := Make_Integer_Literal (Dloc, Sym_Hi_Val); + Set_Is_Static_Expression (Lbound); + Set_Is_Static_Expression (Ubound); + Analyze_And_Resolve (Lbound, Any_Integer); + Analyze_And_Resolve (Ubound, Any_Integer); - Decl := Make_Full_Type_Declaration (Dloc, - Defining_Identifier => Implicit_Base, - Type_Definition => - Make_Signed_Integer_Type_Definition (Dloc, - Low_Bound => Lbound, - High_Bound => Ubound)); + Bounds := Make_Range (Dloc, Lbound, Ubound); + Set_Etype (Bounds, Base_Typ); - Analyze (Decl); - Set_Etype (Implicit_Base, Base_Type (Implicit_Base)); - Set_Etype (T, Base_Type (Implicit_Base)); - Insert_Before (Parent (Def), Decl); - end; - end if; + Set_Scalar_Range (Implicit_Base, Bounds); + end; + + else + Set_Scalar_Range (Implicit_Base, Scalar_Range (Base_Typ)); end if; Set_Size_Info (T, (Implicit_Base)); |