From 93d8d0ee23e6e2c299435440cbfb0ff0246695b8 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 4 Mar 2019 14:57:03 +0100
Subject: [PATCH] [wp] code annot names for -wp-prop option
---
src/plugins/wp/wpPropId.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index da2f5d78db1..c20fbae10bf 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -420,7 +420,8 @@ let ident_names names =
| _ as n -> '\"' <> (String.get n 0) ) names
let code_annot_names ca = match ca.annot_content with
- | AAssert (_, _, named_pred) -> "@assert"::(ident_names named_pred.pred_name)
+ | AAssert (_, Check, named_pred) -> "@check"::(ident_names named_pred.pred_name)
+ | AAssert (_, Assert, named_pred) -> "@assert"::(ident_names named_pred.pred_name)
| AInvariant (_,_,named_pred) -> "@invariant"::(ident_names named_pred.pred_name)
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,(_,name,_,_,_)) -> [Printf.sprintf "@%s" name]
--
GitLab