diff mbox

[Ada] Fix generation of references for SPARK formal verification

Message ID 20131017103225.GA1920@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 17, 2013, 10:32 a.m. UTC 
The generation of references for SPARK formal verification was missing some
write references through renamings. This is now fixed.

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

2013-10-17  Yannick Moy  <moy@adacore.com>

	* sem_ch8.adb (Find_Direct_Name): Keep track of assignments for
	renamings in SPARK mode.
diff mbox

Patch

Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb	(revision 203568)
+++ sem_ch8.adb	(working copy)
@@ -5073,9 +5073,14 @@ 
             --  Entity is unambiguous, indicate that it is referenced here
 
             --  For a renaming of an object, always generate simple reference,
-            --  we don't try to keep track of assignments in this case.
+            --  we don't try to keep track of assignments in this case, except
+            --  in SPARK mode where renamings are traversed for generating
+            --  local effects of subprograms.
 
-            if Is_Object (E) and then Present (Renamed_Object (E)) then
+            if Is_Object (E)
+              and then Present (Renamed_Object (E))
+              and then not SPARK_Mode
+            then
                Generate_Reference (E, N);
 
                --  If the renamed entity is a private protected component,