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 <m...@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.
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);