[Ada] In Alfa mode, record also modifications not coming from source

Submitted by Arnaud Charlet on Nov. 7, 2011, 4:25 p.m.


Message ID 20111107162552.GA21262@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Nov. 7, 2011, 4:25 p.m.
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  <moy@adacore.com>

	* sem_util.adb (Note_Possible_Modification): In Alfa mode,
	generate a reference for a modification even when the modification
	does not come from source.

Patch hide | download patch | download mbox

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