From d44a1535fa17b39690a0e1c184ed65b3298033c5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 2 Dec 2019 18:41:41 +0100
Subject: [PATCH] [e-acsl:archi] fix bug with initial environments of functions
---
src/plugins/e-acsl/src/code_generator/injector.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 8f220ac92b3..a6b0a343fbd 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -589,7 +589,7 @@ let add_malloc_and_free_stmts kf fundec =
to keep the corresponding entries in the table managing them. *)
At_with_lscope.Malloc.remove_all kf
-let inject_in_fundec env main fundec =
+let inject_in_fundec main fundec =
let vi = fundec.svar in
let kf = try Globals.Functions.get vi with Not_found -> assert false in
(* convert ghost variables *)
@@ -603,7 +603,7 @@ let inject_in_fundec env main fundec =
Options.feedback ~dkey ~level:2 "entering in function %a."
Kernel_function.pretty kf;
(* recursive visit *)
- let env = inject_in_block env kf fundec.sbody in
+ let env = inject_in_block Env.empty kf fundec.sbody in
Exit_points.clear ();
add_generated_variables_in_function env fundec;
add_malloc_and_free_stmts kf fundec;
@@ -657,7 +657,7 @@ let inject_in_global (env, main) = function
(* function definition *)
| GFun(fundec, _) ->
- inject_in_fundec env main fundec
+ inject_in_fundec main fundec
(* other globals: nothing to do *)
| GType _
@@ -783,6 +783,6 @@ let inject () =
(*
Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
End:
*)
--
GitLab