From a61da6660902017311255d6594f55e6e70a241d1 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 4 Mar 2020 18:00:51 +0100
Subject: [PATCH] [eacsl:codegen] Change `memory_clean` insertion
Insert `memory_clean` at the end of main at the same time than
`memory_init` at the start of main.
---
.../e-acsl/src/code_generator/injector.ml | 61 ++++++++++---------
1 file changed, 33 insertions(+), 28 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index 044c88c46ec..efa4001dc97 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -812,35 +812,40 @@ let inject_global_initializer file main =
are addresses of program arguments or NULLs if [main] is declared without
arguments. *)
let inject_mmodel_initializer main =
- let loc = Location.unknown in
- let nulls = [ Cil.zero loc ; Cil.zero loc ] in
- let handle_main main =
- let fundec =
- try Kernel_function.get_definition main
- with _ -> assert false (* by construction, the main kf has a fundec *)
- in
- let args =
- (* record arguments only if the second has a pointer type, so argument
- strings can be recorded. This is sufficient to capture C99 compliant
- arguments and GCC extensions with environ. *)
- match fundec.sformals with
- | [] ->
- (* no arguments to main given *)
- nulls
- | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
- (* grab addresses of arguments for a call to the main initialization
- function, i.e., [__e_acsl_memory_init] *)
- List.map Cil.mkAddrOfVi fundec.sformals;
- | _ :: _ ->
- (* some non-standard arguments. *)
- nulls
+ (* Only inject memory init and memory clean if the memory model analysis is
+ running *)
+ if Mmodel_analysis.use_model () then begin
+ let loc = Location.unknown in
+ let nulls = [ Cil.zero loc ; Cil.zero loc ] in
+ let handle_main main =
+ let fundec =
+ try Kernel_function.get_definition main
+ with _ -> assert false (* by construction, the main kf has a fundec *)
+ in
+ let args =
+ (* record arguments only if the second has a pointer type, so argument
+ strings can be recorded. This is sufficient to capture C99 compliant
+ arguments and GCC extensions with environ. *)
+ match fundec.sformals with
+ | [] ->
+ (* no arguments to main given *)
+ nulls
+ | _argc :: argv :: _ when Cil.isPointerType argv.vtype ->
+ (* grab addresses of arguments for a call to the main initialization
+ function, i.e., [__e_acsl_memory_init] *)
+ List.map Cil.mkAddrOfVi fundec.sformals;
+ | _ :: _ ->
+ (* some non-standard arguments. *)
+ nulls
+ in
+ let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
+ let args = args @ [ ptr_size ] in
+ let init = Constructor.mk_rtl_call loc "memory_init" args in
+ let clean = Constructor.mk_rtl_call loc "memory_clean" [] in
+ surround_function_with main fundec init (Some clean)
in
- let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
- let args = args @ [ ptr_size ] in
- let init = Constructor.mk_rtl_call loc "memory_init" args in
- fundec.sbody.bstmts <- init :: fundec.sbody.bstmts
- in
- Extlib.may handle_main main
+ Extlib.may handle_main main
+ end
let inject_in_file file =
let _env, main =
--
GitLab