From 87f6b633d385d38b5f2db72ca7b39c181695cacc Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 3 Aug 2020 12:13:13 +0200
Subject: [PATCH] [e-acsl] monitor neither *alloc nor free
---
.../e-acsl/src/project_initializer/prepare_ast.ml | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
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 2c2c73e7cb7..29f4c1df264 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -426,6 +426,12 @@ class prepare_visitor = object (self)
(Extlib.the self#current_kf)))
&& (* its annotations must be monitored *)
Functions.check kf))
+ && (* it is neither malloc nor free *)
+ (* [TODO:] this special case preserves the former behavior.
+ Should be generalized latter by considering only preconditions of
+ libc functions *)
+ vi.vname <> "malloc" && vi.vname <> "calloc" && vi.vname <> "realloc"
+ && vi.vname <> "free"
->
let name = Functions.RTL.mk_gen_name vi.vname in
let new_vi = Cil.makeGlobalVar name vi.vtype in
@@ -437,9 +443,7 @@ class prepare_visitor = object (self)
let kf = Extlib.the self#current_kf in
(match g with
| GFunDecl _ ->
- if not (Kernel_function.is_definition kf)
- && vi.vname <> "malloc" && vi.vname <> "free"
- then
+ if not (Kernel_function.is_definition kf) then
Options.warning
"@[annotating undefined function `%a':@ \
the generated program may miss memory instrumentation@ \
--
GitLab