From 2c94b9114810ed0346b5119dbe79e45b28b98ad1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Mar 2019 16:04:39 +0100
Subject: [PATCH] [wp] The selection of check assertions complies with option
-wp-prop.
---
.../wp/tests/wp_acsl/oracle/checks.2.res.oracle | 10 ----------
src/plugins/wp/wpAnnot.ml | 15 +++++++--------
src/plugins/wp/wp_parameters.ml | 2 +-
3 files changed, 8 insertions(+), 19 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
index 669139a5ea8..db600bf51f7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -7,21 +7,11 @@
Function main
------------------------------------------------------------
-Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
-Prove: P_P.
-
-------------------------------------------------------------
-
Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
Prove: P_P.
------------------------------------------------------------
-Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
-Prove: true.
-
-------------------------------------------------------------
-
Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
Prove: true.
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 49d002429d5..5369d46e449 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -914,14 +914,13 @@ let get_stmt_annots config v s =
in (b_acc, (a_acc, e_acc))
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
- let kind =
- if kind = Check || Wp_parameters.Assert_check_only.get () then
- WpStrategy.Agoal
- else
- WpStrategy.Aboth (goal_to_select config id)
- in
- let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
- (b_acc, (a_acc, e_acc))
+ let check = kind = Check || Wp_parameters.Assert_check_only.get ()
+ and goal = goal_to_select config id in
+ if check && not goal then acc
+ else
+ let kind = WpStrategy.(if check then Agoal else Aboth goal) in
+ let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
+ (b_acc, (a_acc, e_acc))
in acc
| AAllocation (_b_list, _frees_allocates) ->
(* [PB] TODO *) acc
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 9222639296b..bd5be9fa57d 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -100,7 +100,7 @@ module Properties =
let arg_name = "p,..."
let help = "Select properties having the one of the given tagnames (defaults to all properties).\n\
You may also replace the tagname by '@category' for the selection of all properties of the given category.\n\
- Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors assert, invariant, variant, breaks, continues, returns.\n\
+ Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors, assert, check, invariant, variant, breaks, continues, returns.\n\
Starts by a minus character to remove properties from the selection."
end)
let () = on_reset Properties.clear
--
GitLab