From e180a589ebb5b92c1d26ac221b4a78c014929ce1 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 8 Jun 2021 15:40:01 +0200
Subject: [PATCH] [eacsl] Remove "annotating undefined function" warning for
supported functions
---
src/plugins/e-acsl/src/code_generator/libc.ml | 3 +++
.../e-acsl/src/project_initializer/prepare_ast.ml | 11 ++++++++++-
.../e-acsl/src/project_initializer/prepare_ast.mli | 6 ++++++
3 files changed, 19 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 3a3a514868d..668e159b215 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -67,6 +67,9 @@ let is_writing_memory caller =
| _ -> false
+let () =
+ Prepare_ast.is_libc_writing_memory_ref := is_writing_memory
+
(** [get_result_var ~loc ~name kf ty env result_opt] returns an lvalue
representing the result of the call to the libc function. If [result_opt]
is [Some var] then this lvalue is directly returned, but if the return value
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 246dd0b7c06..07d9a21b6a1 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.ml
@@ -25,6 +25,13 @@ open Cil_datatype
let dkey = Options.dkey_prepare
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+let is_libc_writing_memory_ref: (varinfo -> bool) ref =
+ Extlib.mk_fun "is_libc_writing_memory_ref"
+
(* ********************************************************************** *)
(* Environment *)
(* ********************************************************************** *)
@@ -414,7 +421,9 @@ let prepare_global (globals, new_defs) = function
let new_vi = Dup_functions.generate_vi vi in
if Kernel_function.is_definition kf then
prepare_fundec kf
- else
+ else if not (!is_libc_writing_memory_ref vi) then
+ (* Only display the warning for functions where E-ACSL does not
+ explicitely update its memory model. *)
(* TODO: this warning could be more precise if emitted during code
generation; see also E-ACSL issue #85 about partial verdicts *)
Options.warning
diff --git a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
index ba19b909922..05f454908d7 100644
--- a/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
+++ b/src/plugins/e-acsl/src/project_initializer/prepare_ast.mli
@@ -37,6 +37,12 @@ val sound_verdict: unit -> varinfo
(** @return the [varinfo] representing the E-ACSL global variable that indicates
whether the verdict emitted by E-ACSL is sound. *)
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+
+val is_libc_writing_memory_ref: (varinfo -> bool) ref
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
--
GitLab