[Ada] Store read/write through explicit dereference in ALFA mode

[Arnaud Charlet <charlet at adacore dot com>]

Formal verification relies on a computation of effects based on the local
effects generated in ALFA sections in ALI files. These effects should mention
explicitly all read/writes to memory through explicit dereferences. This is
now done with a special "HEAP" variable.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-08-29  Yannick Moy  <moy@adacore.com>

	* alfa.ads (Name_Of_Heap_Variable): New constant name.
	* lib-xref-alfa.adb, lib-xref.adb, lib-xref.ads (Drefs): New global
	table to hold dereferences.
	(Add_ALFA_Xrefs): Take into account dereferences as special
	reads/writes to the variable "HEAP".
	(Enclosing_Subprogram_Or_Package): Move subprogram here.
	(Generate_Dereference): New procedure to store a read/write dereferencew
	in the table Drefs.
	* put_alfa.adb (Put_ALFA): Use different default than (0,0) used for
	the special "HEAP" var.
	* sem_ch4.adb (Analyze_Explicit_Dereference): Store read dereference
	in ALFA mode.
	* sem_util.adb (Note_Possible_Modification): Store write dereference
	in ALFA mode.

Attachment: difs
Description: Text document