[eacsl] Remove "annotating undefined function" warning for supported functions

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

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

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 ../../../../.."