Alfa mode is meant for formal verification, in which we must gather all
modifications to variables, even those not coming from source. This is in
particular the case for rewritings of renamings in Alfa mode.
Tested on x86_64-pc-linux-gnu, committed on trunk
2011-11-07 Yannick Moy <[email protected]>
* sem_util.adb (Note_Possible_Modification): In Alfa mode,
generate a reference for a modification even when the modification
does not come from source.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 181092)
+++ sem_util.adb (working copy)
@@ -10837,7 +10837,9 @@
-- source. This excludes, for example, calls to a dispatching
-- assignment operation when the left-hand side is tagged.
- if Modification_Comes_From_Source then
+ if Modification_Comes_From_Source
+ or else Alfa_Mode
+ then
Generate_Reference (Ent, Exp, 'm');
-- If the target of the assignment is the bound variable
