The formal verification back-end expects declaration to be present for Itypes,
even if they are not attached to the tree. Add such declarations in the case
of Itypes introduced for index/component types of arrays and anonymous array
types in object declaration.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-08-29 Yannick Moy <m...@adacore.com>
* sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes
created in Alfa mode, instead of inserting artificial declarations of
non-Itypes in the tree.
* sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to
know if an Itype has a corresponding declaration, as defined in
itypes.ads.
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 178239)
+++ sem_ch3.adb (working copy)
@@ -4741,26 +4741,20 @@
Make_Index (Index, P, Related_Id, Nb_Index);
- -- In formal verification mode, create an explicit subtype for every
- -- index if not already a subtype_mark, and replace the existing type
- -- of index by this new type. Having a declaration for all type
+ -- In formal verification mode, create an explicit declaration for
+ -- Itypes created for index types. Having a declaration for all type
-- entities facilitates the task of the formal verification back-end.
+ -- Notice that this declaration is not attached to the tree.
if ALFA_Mode
- and then not Nkind_In (Index, N_Identifier, N_Expanded_Name)
+ and then Is_Itype (Etype (Index))
then
declare
Loc : constant Source_Ptr := Sloc (Def);
- New_E : Entity_Id;
+ Sub_Ind : Node_Id;
Decl : Entity_Id;
- Sub_Ind : Node_Id;
begin
- New_E :=
- New_External_Entity
- (E_Void, Current_Scope, Sloc (P), Related_Id, 'D',
- Nb_Index, 'T');
-
if Nkind (Index) = N_Subtype_Indication then
Sub_Ind := Relocate_Node (Index);
else
@@ -4775,11 +4769,10 @@
Decl :=
Make_Subtype_Declaration (Loc,
- Defining_Identifier => New_E,
+ Defining_Identifier => Etype (Index),
Subtype_Indication => Sub_Ind);
- Insert_Action (Parent (Def), Decl);
- Set_Etype (Index, New_E);
+ Analyze (Decl);
end;
end if;
@@ -4799,34 +4792,29 @@
if Present (Component_Typ) then
- -- In formal verification mode, create an explicit subtype for the
- -- component type if not already a subtype_mark. Having a declaration
- -- for all type entities facilitates the task of the formal
- -- verification back-end.
+ Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+ -- In formal verification mode, create an explicit declaration for
+ -- the Itype created for a component type. Having a declaration for
+ -- all type entities facilitates the task of the formal verification
+ -- back-end. Notice that this declaration is not attached to the
+ -- tree.
+
if ALFA_Mode
- and then Nkind (Component_Typ) = N_Subtype_Indication
+ and then Is_Itype (Element_Type)
then
declare
Loc : constant Source_Ptr := Sloc (Def);
Decl : Entity_Id;
begin
- Element_Type :=
- New_External_Entity
- (E_Void, Current_Scope, Sloc (P), Related_Id, 'C', 0, 'T');
-
Decl :=
Make_Subtype_Declaration (Loc,
Defining_Identifier => Element_Type,
Subtype_Indication => Relocate_Node (Component_Typ));
- Insert_Action (Parent (Def), Decl);
+ Analyze (Decl);
end;
-
- else
- Element_Type :=
- Process_Subtype (Component_Typ, P, Related_Id, 'C');
end if;
Set_Etype (Component_Typ, Element_Type);
@@ -4915,6 +4903,30 @@
(Implicit_Base, Finalize_Storage_Only
(Element_Type));
+ -- In ALFA mode, generate a declaration for Itype T, so that the
+ -- formal verification back-end can use it.
+
+ if ALFA_Mode
+ and then Is_Itype (T)
+ then
+ declare
+ Loc : constant Source_Ptr := Sloc (Def);
+ Decl : Node_Id;
+
+ begin
+ Decl := Make_Full_Type_Declaration (Loc,
+ Defining_Identifier => T,
+ Type_Definition =>
+ Make_Constrained_Array_Definition (Loc,
+ Discrete_Subtype_Definitions =>
+ New_Copy_List (Discrete_Subtype_Definitions (Def)),
+ Component_Definition =>
+ Relocate_Node (Component_Definition (Def))));
+
+ Analyze (Decl);
+ end;
+ end if;
+
-- Unconstrained array case
else
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 178239)
+++ sem_util.adb (working copy)
@@ -8507,6 +8507,20 @@
end if;
end Is_Volatile_Object;
+ ---------------------------
+ -- Itype_Has_Declaration --
+ ---------------------------
+
+ function Itype_Has_Declaration (Id : Entity_Id) return Boolean is
+ begin
+ pragma Assert (Is_Itype (Id));
+ return Present (Parent (Id))
+ and then Nkind_In (Parent (Id),
+ N_Full_Type_Declaration,
+ N_Subtype_Declaration)
+ and then Defining_Entity (Parent (Id)) = Id;
+ end Itype_Has_Declaration;
+
-------------------------
-- Kill_Current_Values --
-------------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 178235)
+++ sem_util.ads (working copy)
@@ -969,6 +969,11 @@
-- for something actually declared as volatile, not for an object that gets
-- treated as volatile (see Einfo.Treat_As_Volatile).
+ function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
+ -- Applies to Itypes. True if the Itype is attached to a declaration for
+ -- the type through its Parent field, which may or not be present in the
+ -- tree.
+
procedure Kill_Current_Values (Last_Assignment_Only : Boolean := False);
-- This procedure is called to clear all constant indications from all
-- entities in the current scope and in any parent scopes if the current
