Patchwork [Ada] Insert subtypes for array index/component in formal verification mode

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 29, 2011, 8:30 a.m.
Message ID <20110829083021.GA30543@adacore.com>
Download mbox | patch
Permalink /patch/111975/
State New
Headers show

Comments

Arnaud Charlet - Aug. 29, 2011, 8:30 a.m.
In formal verification mode, it is expected that subtypes are declared before
use, hence these additional declarations.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Array_Type_Declaration): Insert a subtype declaration
	for every index type and component type that is not a subtype_mark.
	(Process_Subtype): Set Etype of subtype.

Patch

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 178155)
+++ sem_ch3.adb	(working copy)
@@ -4741,6 +4741,47 @@ 
 
          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. Why are we doing this ???
+
+         if ALFA_Mode
+           and then not Nkind_In (Index, N_Identifier, N_Expanded_Name)
+         then
+            declare
+               Loc     : constant Source_Ptr := Sloc (Def);
+               New_E   : Entity_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
+                  Sub_Ind :=
+                    Make_Subtype_Indication (Loc,
+                      Subtype_Mark =>
+                        New_Occurrence_Of (Base_Type (Etype (Index)), Loc),
+                      Constraint =>
+                        Make_Range_Constraint (Loc,
+                          Range_Expression => Relocate_Node (Index)));
+               end if;
+
+               Decl :=
+                 Make_Subtype_Declaration (Loc,
+                   Defining_Identifier => New_E,
+                   Subtype_Indication  => Sub_Ind);
+
+               Insert_Action (Parent (Def), Decl);
+               Set_Etype (Index, New_E);
+            end;
+         end if;
+
          --  Check error of subtype with predicate for index type
 
          Bad_Predicated_Subtype_Use
@@ -4756,8 +4797,37 @@ 
       --  Process subtype indication if one is present
 
       if Present (Component_Typ) then
-         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
 
+         --  In formal verification mode, create an explicit subtype for the
+         --  component type if not already a subtype_mark. Why do this ???
+
+         if ALFA_Mode
+           and then Nkind (Component_Typ) = N_Subtype_Indication
+         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);
+            end;
+
+         else
+            Element_Type :=
+              Process_Subtype (Component_Typ, P, Related_Id, 'C');
+         end if;
+
+         Set_Etype (Component_Typ, Element_Type);
+
          if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
             Check_SPARK_Restriction ("subtype mark required", Component_Typ);
          end if;