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 <m...@adacore.com>
* sem_ch8.adb (Find_Direct_Name): Keep track of assignments for
renamings in SPARK mode.
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,
