diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 3a3a514868d559a4d55b82c994f4547fd8d887ed..668e159b2153a8a3d9f4cbd54ddf31d211de7160 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 246dd0b7c06fada5a1b973f8160e64a15e7051cf..07d9a21b6a174aa2badfe63aa534e16f4e17cb98 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 ba19b9099225af2b839a2a14c018b5f39699ccca..05f454908d76b6ccdce88fb4efb8568681792c7c 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 ../../../../.."