diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml index 861672fca4f8924e8b715a2947c25673ab164c1d..f4d829607802c9a7b5dae8a120efeb8bb531d150 100644 --- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml +++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml @@ -495,7 +495,7 @@ let app_to_exp ~adata ~loc ?tapp kf env ?eargs li targs = fname in let gen_fname = - Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname) + Varname.get ~scope:Global (Functions.RTL.mk_gen_name fname) in let profile = Profile.make li.l_profile params_ival in let profile = Interval.get_widened_profile profile li in diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml index f28a37a3eb525a806a694efb4a6cfc7200ac0e5f..d3b9353faf697321bb3adfffba751e16d49373a2 100644 --- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml +++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml @@ -47,7 +47,9 @@ end = struct (* assume [vi] is not already in [tbl] *) let generate_vi vi = - let new_name = Functions.RTL.mk_gen_name vi.vname in + let new_name = Varname.get ~scope:Global + (Functions.RTL.mk_gen_name vi.vname) + in let new_vi = Cil.makeGlobalVar ~referenced:vi.vreferenced