diff mbox

[Ada] Special cross references in ALFA mode for constants and formals

Message ID 20110804135511.GA16101@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 1:55 p.m. UTC 
ALFA mode used for formal verification requires different cross references,
in which read of constants is absent, and formal is not referenced when used
as selector of parameter association.

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

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

	* lib-xref-alfa.adb (Is_Global_Constant): new function that detects
	library-level constant.
	(Add_ALFA_Xrefs): ignore global constants in ALFA xref.
	* sem_res.adb (Resolve_Actuals): do not add cross-reference to Formal
	used as selector of parameter association, in ALFA mode.
diff mbox

Patch

Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 177365)
+++ sem_res.adb	(working copy)
@@ -3971,9 +3971,14 @@ 
             Eval_Actual (A);
 
             --  If it is a named association, treat the selector_name as a
-            --  proper identifier, and mark the corresponding entity.
+            --  proper identifier, and mark the corresponding entity. Ignore
+            --  this reference in ALFA mode, as it refers to an entity not in
+            --  scope at the point of reference, so the reference should be
+            --  ignored for computing effects of subprograms.
 
-            if Nkind (Parent (A)) = N_Parameter_Association then
+            if Nkind (Parent (A)) = N_Parameter_Association
+              and then not ALFA_Mode
+            then
                Set_Entity (Selector_Name (Parent (A)), F);
                Generate_Reference (F, Selector_Name (Parent (A)));
                Set_Etype (Selector_Name (Parent (A)), F_Typ);
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb	(revision 177383)
+++ lib-xref-alfa.adb	(working copy)
@@ -524,6 +524,10 @@ 
          function Is_ALFA_Scope (E : Entity_Id) return Boolean;
          --  Return whether the entity or reference scope is adequate
 
+         function Is_Global_Constant (E : Entity_Id) return Boolean;
+         --  Return True if E is a global constant for which we should ignore
+         --  reads in ALFA.
+
          -------------------
          -- Is_ALFA_Scope --
          -------------------
@@ -536,6 +540,16 @@ 
               and then Get_Scope_Num (E) /= No_Scope;
          end Is_ALFA_Scope;
 
+         ------------------------
+         -- Is_Global_Constant --
+         ------------------------
+
+         function Is_Global_Constant (E : Entity_Id) return Boolean is
+         begin
+            return Ekind (E) in E_Constant
+              and then Ekind_In (Scope (E), E_Package, E_Package_Body);
+         end Is_Global_Constant;
+
          --  Start of processing for Eliminate_Before_Sort
       begin
 
@@ -547,6 +561,7 @@ 
               and then ALFA_References (Xrefs.Table (Rnums (J)).Typ)
               and then Is_ALFA_Scope (Xrefs.Table (Rnums (J)).Ent_Scope)
               and then Is_ALFA_Scope (Xrefs.Table (Rnums (J)).Ref_Scope)
+              and then not Is_Global_Constant (Xrefs.Table (Rnums (J)).Ent)
             then
                Nrefs         := Nrefs + 1;
                Rnums (Nrefs) := Rnums (J);