+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.
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 --
-----------------------
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 --
-----------------
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 --
---------------------
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 --
----------------
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 --
------------------
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 --
----------------------
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;
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 --
-----------------------
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 --
-----------------
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 --
---------------------
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 --
----------------
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 --
------------------
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 --
----------------------
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;
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;
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;
-- 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
-- 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.
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.
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;
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;
-- 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"
-- 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));
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));
projects / gcc.git / commitdiff