[multiple changes]

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.

From-SVN: r179258

gcc/ada/ChangeLog

 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>

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 --
    ----------------------

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;

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 --
    ----------------------

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;

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;
 

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.

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;

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"

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));