diff mbox

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

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

Commit Message

Arnaud Charlet Nov. 7, 2011, 4:25 p.m. UTC 
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.
diff mbox

Patch

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