From dd19f8fdd15b73a62695aabee649680332c7ff9a Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 7 Jun 2021 18:18:45 +0200
Subject: [PATCH] [eacsl] Generate memory model updates for libc functions
Manually update E-ACSL memory model when calling certain libc functions.
---
.../e-acsl/src/code_generator/injector.ml | 19 +++++++++++++++++--
1 file changed, 17 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index edd21f3ac73..d43acb78c5b 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -88,7 +88,7 @@ let rec inject_in_init env kf_opt vi off = function
in
CompoundInit(typ, List.rev l), env
-let inject_in_local_init loc env kf vi = function
+let inject_in_local_init ~loc ~stmt env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* add a store statement when creating a variable length array *)
@@ -99,6 +99,13 @@ let inject_in_local_init loc env kf vi = function
| ConsInit (caller, args, kind) ->
let args, env = replace_literal_strings_in_args env (Some kf) args in
let caller, args = rename_caller ~loc caller args in
+ let _, env =
+ if Libc.is_writing_memory caller then begin
+ let result = Var vi, NoOffset in
+ Libc.update_memory_model ~loc ~stmt env kf ~result caller args
+ end else
+ None, env
+ in
ConsInit(caller, args, kind), env
| AssignInit init ->
@@ -153,6 +160,14 @@ let inject_in_instr env kf stmt = function
Cil.evar fvi, args
| _ -> caller, args
in
+ (* if this is a call to a libc function that writes into a memory block then
+ manually update the memory model *)
+ let result, env =
+ match caller.enode with
+ | Lval (Var cvi, _) when Libc.is_writing_memory cvi ->
+ Libc.update_memory_model ~loc ~stmt env kf ?result cvi args
+ | _ -> result, env
+ in
(* add statement tracking initialization of return values *)
let env =
match result with
@@ -177,7 +192,7 @@ let inject_in_instr env kf stmt = function
| Local_init(vi, linit, loc) ->
let lv = Var vi, NoOffset in
let env = add_initializer loc ~vi lv ~post:true stmt env kf in
- let linit, env = inject_in_local_init loc env kf vi linit in
+ let linit, env = inject_in_local_init ~loc ~stmt env kf vi linit in
Local_init(vi, linit, loc), env
(* nothing to do: *)
--
GitLab