From d3b4c45a25f55bb125499689a1b6ad325c44cd0d Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Thu, 1 Sep 2022 11:10:32 +0200
Subject: [PATCH] [e-acsl] bugfix: name conflict between functions
---
src/plugins/e-acsl/src/code_generator/logic_functions.ml | 2 +-
src/plugins/e-acsl/src/project_initializer/prepare_ast.ml | 4 +++-
2 files changed, 4 insertions(+), 2 deletions(-)
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 861672fca4f..f4d82960780 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 f28a37a3eb5..d3b9353faf6 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
--
GitLab