From 965fb25ae4cbed8602b8cc0e143874385904fcdc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 9 Sep 2020 18:17:00 +0200
Subject: [PATCH] [wp] added @check category to -wp-prop
---
src/plugins/wp/Changelog | 2 ++
src/plugins/wp/tests/wp_acsl/checks.i | 2 +-
src/plugins/wp/wpPropId.ml | 13 +++++++------
src/plugins/wp/wp_parameters.ml | 2 +-
4 files changed, 11 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 7f362c71486..536b85c8130 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
+- Wp [2020-09-09] Support for generalized @check ACSL annotations
+
#########################
Plugin WP <next-release>
#########################
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index 1a1174504f7..f3fdcbfcab8 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,7 +1,7 @@
/* run.config
OPT: -eva -load-module scope,eva,report -then -report
OPT: -wp-prop=@check
- OPT: -wp-prop=@assert
+ OPT: -wp-prop=-@check
*/
/* run.config_qualif
OPT: -load-module report -wp-steps 5 -then -report
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 77400497f4d..4858d59ff06 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -465,12 +465,13 @@ let ident_names names =
List.filter (function "" -> true
| _ as n -> '\"' <> (String.get n 0) ) names
+let pred_names p =
+ let p_names = ident_names p.tp_statement.pred_name in
+ if p.tp_only_check then "@check"::p_names else p_names
+
let code_annot_names ca = match ca.annot_content with
- | AAssert (_, pred) ->
- let cat = if pred.tp_only_check then "@check" else "@assert" in
- cat::(ident_names pred.tp_statement.pred_name)
- | AInvariant (_,_,named_pred) ->
- "@invariant"::(ident_names named_pred.tp_statement.pred_name)
+ | AAssert (_, pred) -> "@assert" :: pred_names pred
+ | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> [] (* TODO : add some more names ? *)
@@ -481,7 +482,7 @@ let user_prop_names p =
let open Property in match p with
| IPPredicate {ip_kind; ip_pred} ->
Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
- ip_pred.ip_content.tp_statement.pred_name
+ pred_names ip_pred.ip_content
| IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
| IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
| IPComplete {ic_bhvs} ->
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 448ff335f59..c37830d4ebb 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -98,7 +98,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, check, invariant, variant, breaks, continues, returns.\n\
+ Accepted categories are: checks, 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