Skip to content
Snippets Groups Projects
Commit 965fb25a authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[wp] added @check category to -wp-prop

parent fd1eb2c7
No related branches found
No related tags found
No related merge requests found
......@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
- Wp [2020-09-09] Support for generalized @check ACSL annotations
#########################
Plugin WP <next-release>
#########################
......
/* 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
......
......@@ -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} ->
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment