diff mbox

[Ada] Correct wrong generation of ALFA cross-references

Message ID 20110804132633.GA30093@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Aug. 4, 2011, 1:26 p.m. UTC 
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  <moy@adacore.com>

	* lib-xref-alfa.adb (Add_ALFA_Xrefs): correct definition of ranges of
	xrefs in a scope.
diff mbox

Patch

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;