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);