remove a spurious warning when an annotated function is first declared, then defined

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.

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.@]"