From 82398fdafa14ea0aca9aab000272bda9bb2f3cda Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 11 Oct 2019 14:52:43 +0200
Subject: [PATCH] [cil] fixes scope of ghost variables under \at

---
 src/kernel_internals/typing/cabs2cil.ml            | 4 +++-
 tests/syntax/oracle/ghost_local_capture.res.oracle | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index ccf88a9025f..f56d457bb9e 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -866,6 +866,8 @@ let global_env = Datatype.String.Hashtbl.create 307
 (* ghost global environment: superset of global and subset of ghost *)
 let ghost_global_env = Datatype.String.Hashtbl.create 307
 
+(* maps a C label to the ghost environment of variables in scope
+   at this program point. Used for typing \at() terms and predicates. *)
 let label_env = Datatype.String.Hashtbl.create 307
 
 let add_label_env lab =
@@ -876,7 +878,7 @@ let add_label_env lab =
     | _ -> map
   in
   let open Datatype.String.Hashtbl in
-  let lab_env = fold add_if_absent env Datatype.String.Map.empty in
+  let lab_env = fold add_if_absent ghost_env Datatype.String.Map.empty in
   add label_env lab lab_env
 
 let remove_label_env lab =
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index 28e38a724bb..dc24b079c5a 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -10,7 +10,7 @@ void titi(void)
     c = 2;
     /*@ assert c_0 ≡ 1; */ ;
     /*@ assert \at(c,L0) ≡ 0; */ ;
-    /*@ assert \at(c,L1) ≡ 1; */ ;
+    /*@ assert \at(c_0,L1) ≡ 1; */ ;
   }
   /*@ assert c ≡ 2; */ ;
   return;
-- 
GitLab