From e1baea7beb62a661026f94d83eea346dc9889586 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 26 Mar 2014 16:11:02 +0100
Subject: [PATCH] remove a spurious warning when an annotated function is first
declared, then defined
---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/pre_visit.ml | 4 +++-
2 files changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 6a9b2d8ec1a..9d22701682e 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 b9af8ff1b5d..3ccbd55728b 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.@]"
--
GitLab