diff options
| author | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-08-29 16:40:11 +0200 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2011-08-29 16:40:11 +0200 |
| commit | 226a7fa431fc3f9fd533abf6078a1aa9adb9a718 (patch) | |
| tree | e32b257f259965d95e0d8e66ce84cc867c98918a /gcc/ada/sem_ch4.adb | |
| parent | dfbcb149aa59ef88a254489d2c3aa9c105562490 (diff) | |
| download | gcc-226a7fa431fc3f9fd533abf6078a1aa9adb9a718.zip gcc-226a7fa431fc3f9fd533abf6078a1aa9adb9a718.tar.gz gcc-226a7fa431fc3f9fd533abf6078a1aa9adb9a718.tar.bz2 | |
[multiple changes]
2011-08-29 Robert Dewar <dewar@adacore.com>
* sem_ch10.adb, a-coorse.adb, exp_dist.adb, exp_ch3.adb: Minor
reformatting.
* gcc-interface/Make-lang.in: Update dependencies.
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.
From-SVN: r178252
Diffstat (limited to 'gcc/ada/sem_ch4.adb')
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 6b04598..62218c4 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -1761,6 +1761,13 @@ package body Sem_Ch4 is begin Check_SPARK_Restriction ("explicit dereference is not allowed", N); + -- In formal verification mode, keep track of all reads and writes + -- through explicit dereferences. + + if ALFA_Mode then + ALFA.Generate_Dereference (N); + end if; + Analyze (P); Set_Etype (N, Any_Type); |