From a06abeb41d1f39285f62f805aea7f404b1a1c928 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 6 Oct 2020 15:26:42 +0200
Subject: [PATCH] [wp] Do not warn on unused functions prototypes
---
src/plugins/wp/WpTarget.ml | 23 ++++--
.../wp_bts/oracle/issue-684-exit.res.oracle | 72 -------------------
.../oracle_qualif/issue-684-exit.res.oracle | 72 -------------------
3 files changed, 17 insertions(+), 150 deletions(-)
diff --git a/src/plugins/wp/WpTarget.ml b/src/plugins/wp/WpTarget.ml
index 4dc9ae541c5..10d122bee5a 100644
--- a/src/plugins/wp/WpTarget.ml
+++ b/src/plugins/wp/WpTarget.ml
@@ -52,11 +52,22 @@ let calls_visitor callees = object(self)
| _ -> Cil.SkipChildren
end
-let add_with_dependencies kf =
+(** Note: we add the kf received in parameter in the set only if it has a
+ definition (and thus if it does not have one, we add nothing as it has
+ no visible callee).
+
+ This prevent to warn on prototypes that have a contract but are unused. If
+ the function is used, it will be added to the set via its caller(s) if they
+ are under verification.
+*)
+let add_with_callees kf =
let component kf =
- let set = ref (Fct.singleton kf) in
- ignore (Visitor.visitFramacKf (calls_visitor set) kf) ;
- !set
+ if Kernel_function.has_definition kf then begin
+ let set = ref (Fct.singleton kf) in
+ ignore (Visitor.visitFramacKf (calls_visitor set) kf) ;
+ !set
+ end else
+ Fct.empty
in
Fct.iter TargetKfs.add (component kf)
@@ -147,10 +158,10 @@ let check_properties behaviors props kf =
let add_with_behaviors behaviors props kf =
if behaviors = [] && props = [] then
- add_with_dependencies kf
+ add_with_callees kf
else begin
try check_properties behaviors props kf
- with Found -> add_with_dependencies kf
+ with Found -> add_with_callees kf
end
let compute model =
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
index f5c27f43319..cb499212b74 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
@@ -25,75 +25,3 @@ Goal Assigns nothing in 'inconditional_exit':
Prove: true.
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'seed48':
- /*@
- behavior typed:
- requires
- \separated(
- seed16v + (..), (unsigned short *)__fc_random48_counter + (..),
- &__fc_random48_init, &__fc_p_random48_counter
- );
- */
- extern unsigned short *seed48(unsigned short * /*[3]*/ seed16v);
-[wp] Warning: Memory model hypotheses for function 'lcong48':
- /*@
- behavior typed:
- requires
- \separated(
- param + (..), (unsigned short *)__fc_random48_counter + (..),
- &__fc_random48_init
- );
- */
- extern void lcong48(unsigned short * /*[7]*/ param);
-[wp] Warning: Memory model hypotheses for function 'erand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern double erand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'nrand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern long nrand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'jrand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern long jrand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'getenv':
- /*@
- behavior typed:
- requires \separated(name + (..), (char **)__fc_env + (..));
- */
- extern char *getenv(char const *name);
-[wp] Warning: Memory model hypotheses for function 'putenv':
- /*@
- behavior typed:
- requires \separated(string + (..), (char **)__fc_env + (..));
- */
- extern int putenv(char *string);
-[wp] Warning: Memory model hypotheses for function 'setenv':
- /*@
- behavior typed:
- requires
- \separated((char **)__fc_env + (..), {name + (..), value + (..)});
- */
- extern int setenv(char const *name, char const *value, int overwrite);
-[wp] Warning: Memory model hypotheses for function 'unsetenv':
- /*@
- behavior typed:
- requires \separated(name + (..), (char **)__fc_env + (..));
- */
- extern int unsetenv(char const *name);
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
index 4301abb0fa7..be5d63c71f6 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
@@ -13,75 +13,3 @@
Functions WP Alt-Ergo Total Success
inconditional_exit 4 - 4 100%
------------------------------------------------------------
-[wp] Warning: Memory model hypotheses for function 'seed48':
- /*@
- behavior typed:
- requires
- \separated(
- seed16v + (..), (unsigned short *)__fc_random48_counter + (..),
- &__fc_random48_init, &__fc_p_random48_counter
- );
- */
- extern unsigned short *seed48(unsigned short * /*[3]*/ seed16v);
-[wp] Warning: Memory model hypotheses for function 'lcong48':
- /*@
- behavior typed:
- requires
- \separated(
- param + (..), (unsigned short *)__fc_random48_counter + (..),
- &__fc_random48_init
- );
- */
- extern void lcong48(unsigned short * /*[7]*/ param);
-[wp] Warning: Memory model hypotheses for function 'erand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern double erand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'nrand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern long nrand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'jrand48':
- /*@
- behavior typed:
- requires
- \separated(
- xsubi + (..), (unsigned short *)__fc_random48_counter + (..)
- );
- */
- extern long jrand48(unsigned short * /*[3]*/ xsubi);
-[wp] Warning: Memory model hypotheses for function 'getenv':
- /*@
- behavior typed:
- requires \separated(name + (..), (char **)__fc_env + (..));
- */
- extern char *getenv(char const *name);
-[wp] Warning: Memory model hypotheses for function 'putenv':
- /*@
- behavior typed:
- requires \separated(string + (..), (char **)__fc_env + (..));
- */
- extern int putenv(char *string);
-[wp] Warning: Memory model hypotheses for function 'setenv':
- /*@
- behavior typed:
- requires
- \separated((char **)__fc_env + (..), {name + (..), value + (..)});
- */
- extern int setenv(char const *name, char const *value, int overwrite);
-[wp] Warning: Memory model hypotheses for function 'unsetenv':
- /*@
- behavior typed:
- requires \separated(name + (..), (char **)__fc_env + (..));
- */
- extern int unsetenv(char const *name);
--
GitLab