From ba17b25f122ed8dda6471597638d5a9b37140d8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Apr 2018 16:33:25 +0200
Subject: [PATCH] =?UTF-8?q?[WP]=20automatically=20filter=20properties=20wi?=
=?UTF-8?q?th=20name=20=E2=80=98no=5Fwp:=E2=80=99?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/plugins/wp/Changelog | 3 +-
src/plugins/wp/doc/manual/wp_plugin.tex | 3 ++
src/plugins/wp/tests/wp_plugin/nowp.c | 7 +++
.../wp/tests/wp_plugin/nowp.c.0.report.json | 1 +
.../wp/tests/wp_plugin/oracle/nowp.res.oracle | 6 +++
.../wp_plugin/oracle_qualif/nowp.res.oracle | 9 ++++
src/plugins/wp/wpAnnot.ml | 2 +-
src/plugins/wp/wpPropId.ml | 51 +++++++++++--------
src/plugins/wp/wpPropId.mli | 6 ++-
9 files changed, 64 insertions(+), 24 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/nowp.c
create mode 100644 src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 65843136872..e949fb06f40 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,7 +20,8 @@
# <Prover>: prover
###############################################################################
- - Wp [2019/01/28] New floating-point model
+ - WP [2019/02/05] Auto filter properties with name "no_wp:"
+ - Wp [2019/01/28] New floating-point model
- WP [2018/02/16] Filter out some variables from separation
- TIP [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
- TIP [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 86bdae51f57..ab349e42530 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -762,6 +762,9 @@ interface of the programmatic API.
Properties can be prefixed with a minus sign to \emph{skip} the associated annotations.
For example \texttt{-wp-prop="-@assigns"} removes all \texttt{assigns}
and \texttt{loop assigns} properties from the selection.
+ \\
+ \textbf{Remark:} properties with name \verb+no_wp:+ are always and automatically
+ filtered and never proved by WP.
\item [\tt -wp-(no)-status-all] includes in the goal selection all properties
regardless of their current status (default is: \texttt{no}).
\item [\tt -wp-(no)-status-valid] includes in the goal selection those properties
diff --git a/src/plugins/wp/tests/wp_plugin/nowp.c b/src/plugins/wp/tests/wp_plugin/nowp.c
new file mode 100644
index 00000000000..c79a19034c7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nowp.c
@@ -0,0 +1,7 @@
+
+int main(int a) {
+ int b;
+ if (a) b = 42 + a;
+ //@ assert no_wp: \initialized(&b);
+ return b;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json b/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
new file mode 100644
index 00000000000..19765bd501b
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nowp.c.0.report.json
@@ -0,0 +1 @@
+null
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
new file mode 100644
index 00000000000..134cf5cfbb8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/nowp.res.oracle
@@ -0,0 +1,6 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] No proof obligations
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
new file mode 100644
index 00000000000..a36ba397028
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nowp.res.oracle
@@ -0,0 +1,9 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_plugin/nowp.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 0 goal scheduled
+[wp] Proved goals: 0 / 0
+[wp] Report 'tests/wp_plugin/nowp.c.0.report.json'
+-------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index cffa1268c68..b3e9f7e76b9 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -325,10 +325,10 @@ let filter_configstatus config pid =
let filter_asked config pid =
match config.asked_prop with
- | AllProps -> true
| IdProp idp -> Property.equal (WpPropId.property_of_id pid) idp
| CallPre (s_call, asked_pre) -> WpPropId.select_call_pre s_call asked_pre pid
| NamedProp names -> WpPropId.select_by_name names pid
+ | AllProps -> WpPropId.select_default pid
let rec filter config pid = function
| [] -> None
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7ee846ce041..43fc36f5e26 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -693,29 +693,38 @@ let is_loop_preservation p =
end
| _ -> None
-let select_by_name asked_names pid =
+let user_prop_pid pid =
let p_prop = match pid.p_kind with
| PKPre (_,_,p_prop) -> p_prop
- | _ -> property_of_id pid
- in
- let names = user_prop_names p_prop in
- let is_minus s = try s.[0] = '-' with _ -> false in
- let is_plus s = try s.[0] = '+' with _ -> false in
- let remove_first s = String.sub s 1 ((String.length s) -1) in
- let eval acc asked =
- let is_minus,a = match acc with
- | None -> if is_minus asked then true,true else false,false
- | Some a -> (is_minus asked),a
- in let eval () =
- let asked = if is_minus || (is_plus asked) then remove_first asked else asked
- in List.mem asked names
- in Some (if is_minus
- then a && (not (eval ()))
- else a || (eval ()))
- in
- match List.fold_left eval None asked_names with
- | Some false -> false
- | _ -> true
+ | _ -> property_of_id pid in
+ user_prop_names p_prop
+
+let select_default pid =
+ let names = user_prop_pid pid in
+ not (List.mem "no_wp" names)
+
+let select_by_name asked_names pid =
+ let names = user_prop_pid pid in
+ if List.mem "no_wp" names then false
+ else
+ let is_minus s = try s.[0] = '-' with _ -> false in
+ let is_plus s = try s.[0] = '+' with _ -> false in
+ let remove_first s = String.sub s 1 ((String.length s) -1) in
+ let eval acc asked =
+ let is_minus,a = match acc with
+ | None -> if is_minus asked then true,true else false,false
+ | Some a -> (is_minus asked),a
+ in let eval () =
+ let asked = if is_minus || (is_plus asked)
+ then remove_first asked else asked
+ in List.mem asked names
+ in Some (if is_minus
+ then a && (not (eval ()))
+ else a || (eval ()))
+ in
+ match List.fold_left eval None asked_names with
+ | Some false -> false
+ | _ -> true
let select_call_pre s_call asked_pre pid =
match pid.p_kind with
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 16b42ff8adc..5b143da7426 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -54,8 +54,12 @@ val is_assigns : prop_id -> bool
val is_requires : Property.t -> bool
val is_loop_preservation : prop_id -> stmt option
+(** test if the prop_id does not have a [no_wp:] in its name(s). *)
+val select_default : prop_id -> bool
+
(** test if the prop_id has to be selected for the asked name.
- * Also returns a debug message to explain then answer. *)
+ Also returns a debug message to explain then answer. Includes
+ a test for [no_wp:]. *)
val select_by_name : string list -> prop_id -> bool
(** test if the prop_id has to be selected when we want to select the call
--
GitLab