From 44f156cd60c1b661f1420d3b2eb8634ff73548ce Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Mon, 2 Oct 2023 09:53:00 +0200
Subject: [PATCH] Add attribute `goblint_cil_nested` to local `varinfo`s that
 are not declared at top scope (#155)

---
 src/frontc/cabs2cil.ml  | 22 +++++++++++++++++++---
 src/frontc/cabs2cil.mli |  6 ++++++
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 52d3a2c3f..616669caa 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -75,6 +75,12 @@ let nocil: int ref = ref (-1)
     *)
 let alwaysGenerateVarDecl = false
 
+(** Add an attribute to all variables which are not declared at the top scope,
+    so tools building on CIL can know which variables were pulled up.
+    Should be disabled when printing CIL code, as compilers will warn about this attribute.
+*)
+let addNestedScopeAttr = ref false
+
 (** Indicates whether we're allowed to duplicate small chunks. *)
 let allowDuplication: bool ref = ref true
 
@@ -557,9 +563,19 @@ let alphaConvertVarAndAddToEnv (addtoenv: bool) (vi: varinfo) : varinfo =
   in
   (* Store all locals in the slocals (in reversed order). We'll reverse them
      and take out the formals at the end of the function *)
-  if not vi.vglob then
-    !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals;
-
+  if not vi.vglob then (
+    (if !addNestedScopeAttr then
+      (* two scopes implies top-level scope in the function, one is created for the FUNDEF (includes formals etc),
+         one for the body which is a block *)
+      match !scopes with
+      | _::_::_::_ ->
+        (* i.e.  List.length scopes > 2 *)
+        newvi.vattr <- Attr("goblint_cil_nested", []) :: newvi.vattr
+      | _ -> ()
+    );
+    !currentFunctionFDEC.slocals <- newvi :: !currentFunctionFDEC.slocals
+  )
+  ;
   (if addtoenv then
     if vi.vglob then
       addGlobalToEnv vi.vname (EnvVar newvi)
diff --git a/src/frontc/cabs2cil.mli b/src/frontc/cabs2cil.mli
index e2e2a4843..b7b6c719c 100644
--- a/src/frontc/cabs2cil.mli
+++ b/src/frontc/cabs2cil.mli
@@ -45,6 +45,12 @@ val forceRLArgEval: bool ref
    -1 to disable *)
 val nocil: int ref
 
+(** Add an attribute to all variables which are not declared at the top scope,
+    so tools building on CIL can know which variables were pulled up.
+    Should be disabled when printing CIL code, as compilers will warn about this attribute.
+*)
+val addNestedScopeAttr: bool ref
+
 (** Indicates whether we're allowed to duplicate small chunks of code. *)
 val allowDuplication: bool ref