From 226a7fa431fc3f9fd533abf6078a1aa9adb9a718 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 29 Aug 2011 16:40:11 +0200 Subject: [multiple changes] 2011-08-29 Robert Dewar * 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 * 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 --- gcc/ada/sem_ch4.adb | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'gcc/ada/sem_ch4.adb') 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); -- cgit v1.1