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

login
register
mail settings
Submitter Arnaud Charlet
Date Nov. 7, 2011, 4:25 p.m.
Message ID <20111107162552.GA21262@adacore.com>
Download mbox | patch
Permalink /patch/124128/
State New
Headers show

Comments

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

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