There was a problem with generation of ALFA cross-references for formal verification, which causes a reference to appear in two scopes. Now corrected.
Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-04 Yannick Moy <m...@adacore.com> * lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of xrefs in a scope.
Index: lib-xref-alfa.adb =================================================================== --- lib-xref-alfa.adb (revision 177378) +++ lib-xref-alfa.adb (working copy) @@ -339,7 +339,6 @@ -------------------- procedure Add_ALFA_Xrefs is - Prev_Scope_Idx : Scope_Index; Cur_Scope_Idx : Scope_Index; From_Xref_Idx : Xref_Index; Cur_Entity : Entity_Id; @@ -613,13 +612,12 @@ -- Initialize loop - Prev_Scope_Idx := 1; Cur_Scope_Idx := 1; From_Xref_Idx := 1; Cur_Entity := Empty; - if ALFA_Scope_Table.Last /= 0 then - ALFA_Scope_Table.Table (1).From_Xref := 1; + if ALFA_Scope_Table.Last = 0 then + return; end if; -- Loop to output references @@ -721,9 +719,15 @@ pragma Assert (Is_Future_Scope_Entity (XE.Ent_Scope)); + -- Update the range of cross references to which the current scope + -- refers to. This may be the empty range only for the first scope + -- considered. + if XE.Ent_Scope /= Cur_Scope then ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx; + ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref := + ALFA_Xref_Table.Last; From_Xref_Idx := ALFA_Xref_Table.Last + 1; end if; @@ -732,14 +736,6 @@ pragma Assert (Cur_Scope_Idx <= ALFA_Scope_Table.Last); end loop; - if Prev_Scope_Idx /= Cur_Scope_Idx - and then ALFA_Xref_Table.Last /= 0 - then - ALFA_Scope_Table.Table (Prev_Scope_Idx).To_Xref := - ALFA_Xref_Table.Last; - Prev_Scope_Idx := Cur_Scope_Idx; - end if; - if XE.Ent /= Cur_Entity then Cur_Entity_Name := new String'(Exact_Source_Name (Sloc (XE.Ent))); @@ -758,6 +754,8 @@ end Add_One_Xref; end loop; + -- Update the range of cross references to which the scope refers to + ALFA_Scope_Table.Table (Cur_Scope_Idx).From_Xref := From_Xref_Idx; ALFA_Scope_Table.Table (Cur_Scope_Idx).To_Xref := ALFA_Xref_Table.Last; end Add_ALFA_Xrefs;