Patchwork [Ada] Generate Alfa cross-references for instantiations of generics

login
register
mail settings
Submitter Arnaud Charlet
Date March 30, 2012, 9:24 a.m.
Message ID <20120330092419.GA24057@adacore.com>
Download mbox | patch
Permalink /patch/149595/
State New
Headers show

Comments

Arnaud Charlet - March 30, 2012, 9:24 a.m.
In order to apply formal verification to code with instantiations of generics,
we must get Alfa cross-references for this code. This consists mostly in
enabling the generation of instances in Alfa mode, and adapting the Alfa xref
code.

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

2012-03-30  Yannick Moy  <moy@adacore.com>

	* lib-xref-alfa.adb (Generate_Dereference): Use Get_Code_Unit
	instead of Get_Source_Unit to get file for reference.
	(Traverse_Compilation_Unit): Do not add scopes for generic units.
	* lib-xref.adb (Generate_Reference): Use Get_Code_Unit instead
	of Get_Source_Unit to get file for reference.
	* sem_ch12.adb (Analyze_Package_Instantiation): Enable
	instantiation in Alfa mode.

Patch

Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 185995)
+++ sem_ch12.adb	(working copy)
@@ -3704,7 +3704,6 @@ 
                            or else Might_Inline_Subp)
                 and then not Is_Actual_Pack
                 and then not Inline_Now
-                and then not Alfa_Mode
                 and then (Operating_Mode = Generate_Code
                            or else (Operating_Mode = Check_Semantics
                                      and then ASIS_Mode));
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb	(revision 186001)
+++ lib-xref-alfa.adb	(working copy)
@@ -1051,15 +1051,13 @@ 
 
       Loc       : constant Source_Ptr := Sloc (N);
       Index     : Nat;
-      Ref       : Source_Ptr;
       Ref_Scope : Entity_Id;
 
    --  Start of processing for Generate_Dereference
 
    begin
-      Ref := Original_Location (Loc);
 
-      if Ref > No_Location then
+      if Loc > No_Location then
          Drefs.Increment_Last;
          Index := Drefs.Last;
 
@@ -1075,21 +1073,21 @@ 
             Ref_Scope := Enclosing_Subprogram_Or_Package (N);
 
             Deref.Ent := Heap;
-            Deref.Loc := Ref;
+            Deref.Loc := Loc;
             Deref.Typ := Typ;
 
             --  It is as if the special "Heap" was defined in every scope where
             --  it is referenced.
 
-            Deref.Eun := Get_Source_Unit (Ref);
-            Deref.Lun := Get_Source_Unit (Ref);
+            Deref.Eun := Get_Code_Unit (Loc);
+            Deref.Lun := Get_Code_Unit (Loc);
 
             Deref.Ref_Scope := Ref_Scope;
             Deref.Ent_Scope := Ref_Scope;
 
             Deref_Entry.Def := No_Location;
 
-            Deref_Entry.Ent_Scope_File := Get_Source_Unit (Ref_Scope);
+            Deref_Entry.Ent_Scope_File := Get_Code_Unit (N);
          end;
       end if;
    end Generate_Dereference;
@@ -1125,6 +1123,14 @@ 
          Lu := Proper_Body (Lu);
       end if;
 
+      --  Do not add scopes for generic units
+
+      if Nkind (Lu) = N_Package_Body
+        and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind
+      then
+         return;
+      end if;
+
       --  Call Process on all declarations
 
       if Nkind (Lu) in N_Declaration
Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 186001)
+++ lib-xref.adb	(working copy)
@@ -378,7 +378,6 @@ 
       Def            : Source_Ptr;
       Ent            : Entity_Id;
       Ent_Scope      : Entity_Id;
-      Ent_Scope_File : Unit_Number_Type;
       Formal         : Entity_Id;
       Kind           : Entity_Kind;
       Nod            : Node_Id;
@@ -633,6 +632,16 @@ 
            or else Typ = 'i'
            or else Typ = 'k'
            or else (Typ = 'b' and then Is_Generic_Instance (E))
+
+            --  Allow the generation of references to reads, writes and calls
+            --  in Alfa mode when the related context comes from an instance.
+
+           or else
+             (Alfa_Mode
+                and then In_Extended_Main_Code_Unit (N)
+                and then (Typ = 'm'
+                            or else Typ = 'r'
+                            or else Typ = 's'))
          then
             null;
          else
@@ -880,11 +889,12 @@ 
 
          --  Ignore references from within an instance. The only exceptions to
          --  this are default subprograms, for which we generate an implicit
-         --  reference.
+         --  reference and compilations in Alfa_Mode.
 
          and then
            (Instantiation_Location (Sloc (N)) = No_Location
-              or else Typ = 'i')
+              or else Typ = 'i'
+              or else Alfa_Mode)
 
          --  Ignore dummy references
 
@@ -995,9 +1005,6 @@ 
 
          --  Record reference to entity
 
-         Ref := Original_Location (Sloc (Nod));
-         Def := Original_Location (Sloc (Ent));
-
          if Actual_Typ = 'p'
            and then Is_Subprogram (Nod)
            and then Present (Overridden_Operation (Nod))
@@ -1006,6 +1013,9 @@ 
          end if;
 
          if Alfa_Mode then
+            Ref := Sloc (Nod);
+            Def := Sloc (Ent);
+
             Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (Nod);
             Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent);
 
@@ -1018,22 +1028,30 @@ 
                return;
             end if;
 
-            Ent_Scope_File := Get_Source_Unit (Ent_Scope);
+            Add_Entry
+              ((Ent      => Ent,
+                Loc       => Ref,
+                Typ       => Actual_Typ,
+                Eun       => Get_Code_Unit (Def),
+                Lun       => Get_Code_Unit (Ref),
+                Ref_Scope => Ref_Scope,
+                Ent_Scope => Ent_Scope),
+               Ent_Scope_File => Get_Code_Unit (Ent));
+
          else
-            Ref_Scope := Empty;
-            Ent_Scope := Empty;
-            Ent_Scope_File := No_Unit;
+            Ref := Original_Location (Sloc (Nod));
+            Def := Original_Location (Sloc (Ent));
+
+            Add_Entry
+              ((Ent      => Ent,
+                Loc       => Ref,
+                Typ       => Actual_Typ,
+                Eun       => Get_Source_Unit (Def),
+                Lun       => Get_Source_Unit (Ref),
+                Ref_Scope => Empty,
+                Ent_Scope => Empty),
+               Ent_Scope_File => No_Unit);
          end if;
-
-         Add_Entry
-           ((Ent => Ent,
-             Loc => Ref,
-             Typ => Actual_Typ,
-             Eun => Get_Source_Unit (Def),
-             Lun => Get_Source_Unit (Ref),
-             Ref_Scope => Ref_Scope,
-             Ent_Scope => Ent_Scope),
-            Ent_Scope_File => Ent_Scope_File);
       end if;
    end Generate_Reference;