diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 6a9b2d8ec1a5b9cef6fd6526b9df967f5a1fd4d6..9d22701682e7afc273595c169b8368b86984744a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-  E-ACSL       [2014/03/26] Remove a spurious warning when an annotated
+	        function is first declared, then defined.
 -* E-ACSL       [2014/03/25] Fix bug #1716 with annotations in while(1).
 -* E-ACSL       [2014/03/25] Fix bug #1715 about -e-acsl-full-mmodel which
 	        generates incorrect code.
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index b9af8ff1b5d326af4d6845d550ddb03eb59d1000..3ccbd55728bc40ec321a60b0131e707e435269e5 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -301,7 +301,9 @@ class dup_functions_visitor prj = object (self)
       | [ GVarDecl(_, vi, _) | GFun({ svar = vi }, _) as g ] -> 
 	(match g with
 	| GVarDecl _ ->
-	  if vi.vname <> "malloc" && vi.vname <> "free" then
+	  if not (Kernel_function.is_definition (Extlib.the self#current_kf))
+            && vi.vname <> "malloc" && vi.vname <> "free" 
+          then
 	    Options.warning "@[annotating undefined function `%a':@ \
 the generated program may miss memory instrumentation@ \
 if there are memory-related annotations.@]"