Skip to content

Commit

Permalink
Add attribute goblint_cil_nested to local varinfos that are not d…
Browse files Browse the repository at this point in the history
…eclared at top scope (#155)
michael-schwarz authored Oct 2, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
1 parent 70a4198 commit 44f156c
Showing 2 changed files with 25 additions and 3 deletions.
22 changes: 19 additions & 3 deletions src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
@@ -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)
6 changes: 6 additions & 0 deletions src/frontc/cabs2cil.mli
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 44f156c

Please sign in to comment.