diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 4403e5e4eef2e4ee947a64d63a0f6fb1a25b4b35..4029b3829485231a6aee7a24913a591c026babe0 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -126,7 +126,7 @@ and identified_lemma = {
il_name : string;
il_labels : logic_label list;
il_args : string list;
- il_pred : predicate;
+ il_pred : toplevel_predicate;
il_loc : location
}
@@ -418,8 +418,13 @@ include Datatype.Make_with_collections
type t = identified_property
let name = "Property.t"
- let reprs = [IPAxiom {il_name="";il_labels=[];il_args=[];
- il_pred=Logic_const.ptrue;il_loc=Location.unknown}]
+ let reprs = [
+ IPAxiom {
+ il_name="";il_labels=[];il_args=[];
+ il_pred=Logic_const.(toplevel_predicate ptrue);
+ il_loc=Location.unknown
+ }]
+
let mem_project = Datatype.never_any_project
let pp_active fmt active =
@@ -837,7 +842,7 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string il_name
(Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
(Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
- Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_toplevel_predicate il_pred
Cil_types_debug.pp_location il_loc
| IPAxiomatic {iax_name; iax_props} ->
Format.fprintf fmt "IPAxiomatic(%a,%a)"
@@ -848,7 +853,7 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string il_name
(Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
(Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
- Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_toplevel_predicate il_pred
Cil_types_debug.pp_location il_loc
| IPTypeInvariant {iti_name; iti_type; iti_pred; iti_loc} ->
Format.fprintf fmt "IPTypeInvariant(%a,%a,%a,%a)"
@@ -1028,10 +1033,10 @@ struct
| IPDecrease {id_kf=kf; id_variant=variant} ->
(kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
| IPAxiom {il_name=name; il_pred} ->
- Format.asprintf "axiom_%s%a" name pp_names il_pred.pred_name
+ Format.asprintf "axiom_%s%a" name pp_names il_pred.tp_statement.pred_name
| IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
| IPLemma {il_name=name; il_pred} ->
- Format.asprintf "lemma_%s%a" name pp_names il_pred.pred_name
+ Format.asprintf "lemma_%s%a" name pp_names il_pred.tp_statement.pred_name
| IPTypeInvariant {iti_name; iti_pred} ->
Format.asprintf "type_invariant_%s%a"
iti_name pp_names iti_pred.pred_name
@@ -1150,17 +1155,35 @@ struct
| IPPredicate {ip_kind=PKAssumes bhv; ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "assumes" ; I ip ]
| IPPredicate {ip_kind=PKRequires bhv; ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "requires" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_requires" else "requires"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Normal); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "ensures" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_ensures" else "ensures"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Exits); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "exits" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_exits" else "exits"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Breaks); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "breaks" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_breaks" else "breaks"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Continues); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "continues" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_continues" else "continues"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Returns); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "returns" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_returns" else "returns"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKTerminates; ip_kf=kf; ip_pred=ip} ->
[ K kf ; A "terminates" ; I ip ]
@@ -1195,9 +1218,15 @@ struct
let a = if p.tp_only_check then "check" else "assert" in
[K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
- [K kf ; A "loop_invariant" ; P p.tp_statement ]
- | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, false, p)}} ->
- [K kf ; A "invariant" ; P p.tp_statement ]
+ let a =
+ if p.tp_only_check then "check_loop_invariant" else "loop_invariant"
+ in
+ [K kf ; A a ; P p.tp_statement ]
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_,false, p)}} ->
+ let a =
+ if p.tp_only_check then "check_invariant" else "invariant"
+ in
+ [K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AVariant (e, _)}} ->
[K kf ; A "loop_variant" ; T e ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssigns _}} ->
@@ -1223,7 +1252,8 @@ struct
| IPAxiomatic _
| IPAxiom _ -> []
| IPLemma {il_name=name; il_pred=p} ->
- [ A "lemma" ; A name ; P p ]
+ let a = if p.tp_only_check then "check_lemma" else "lemma" in
+ [ A a ; A name ; P p.tp_statement ]
| IPTypeInvariant {iti_name=name}
| IPGlobalInvariant {igi_name=name} ->
@@ -1511,10 +1541,8 @@ let ip_of_global_annotation a =
let iax_props = List.fold_left aux [] l in
IPAxiomatic {iax_name; iax_props} :: (iax_props @ acc)
| Dlemma(il_name, true, il_labels, il_args, il_pred, _, il_loc) ->
- let il_pred = il_pred.tp_statement in
ip_axiom {il_name; il_labels; il_args; il_pred; il_loc} :: acc
| Dlemma(il_name, false, il_labels, il_args, il_pred, _, il_loc) ->
- let il_pred = il_pred.tp_statement in
ip_lemma {il_name; il_labels; il_args; il_pred; il_loc} :: acc
| Dinvariant(l, igi_loc) ->
let igi_pred = match l.l_body with
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 48549e11c1dbb99c1dd2dde43c348a4d2e90e21f..395250cf2e30de409e5fe3ae29b9477a97acaf05 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -156,7 +156,7 @@ and identified_lemma = {
il_name : string;
il_labels : logic_label list;
il_args : string list;
- il_pred : predicate;
+ il_pred : toplevel_predicate;
il_loc : location
}
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index c9f1318b512cc8430d085f7c53b4fb8392bcb099..b64e8fbfebde6a2bb71a95224180bbcdb9f135ac 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -135,6 +135,7 @@ val pp_quantifiers : Format.formatter -> Cil_types.quantifiers -> unit
val pp_relation : Format.formatter -> Cil_types.relation -> unit
val pp_predicate_node : Format.formatter -> Cil_types.predicate_node -> unit
val pp_identified_predicate : Format.formatter -> Cil_types.identified_predicate -> unit
+val pp_toplevel_predicate: Format.formatter -> Cil_types.toplevel_predicate -> unit
val pp_predicate : Cil_types.predicate Pretty_utils.formatter
val pp_spec : Format.formatter -> Cil_types.spec -> unit
val pp_acsl_extension : Format.formatter -> Cil_types.acsl_extension -> unit
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index eef3d6be8629ac500382c25f452dd6c543efb235..1058d7ffa962fa3063fd853fc8039e5a8aa9450c 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -194,10 +194,16 @@ let pp_profile fmt l =
let ip_lemma l =
let open Property in
- (if l.lem_kind = `Axiom then Property.ip_axiom else Property.ip_lemma)
+ let mk_prop, only_check =
+ match l.lem_kind with
+ | `Axiom -> Property.ip_axiom, false
+ | `Lemma -> Property.ip_lemma, false
+ | `Check -> Property.ip_lemma, true
+ in
+ mk_prop
{il_name = l.lem_name; il_labels = l.lem_labels;
il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
- il_pred = l.lem_property}
+ il_pred = Logic_const.toplevel_predicate ~only_check l.lem_property}
let lemma_of_global ~context = function
| Dlemma(name,axiom,labels,types,pred,_,loc) ->
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 4858d59ff064165d03b16879580ad7d93f8cc400..6b9f147e04d1b375eb23857ca8d50d2f335e331b 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -500,7 +500,8 @@ let user_prop_names p =
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
- let names = "@lemma"::a::(ident_names l.pred_name)
+ let cat = if l.tp_only_check then "@check" else "@lemma" in
+ let names = cat::a::(ident_names l.tp_statement.pred_name)
in begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
@@ -657,7 +658,7 @@ let property_hints hs =
let open Property in function
| IPAxiom {il_name; il_pred}
| IPLemma {il_name; il_pred} ->
- List.iter (add_required hs) (il_name::il_pred.pred_name)
+ List.iter (add_required hs) (il_name::il_pred.tp_statement.pred_name)
| IPBehavior _ -> ()
| IPComplete {ic_bhvs} | IPDisjoint {ic_bhvs} ->
List.iter (add_required hs) ic_bhvs
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
index a9fee931026eb5fffce6a0946da5835fe5d74b7a..7f7128dfa8d7a982a69817b1f63a4e4ef677a02b 100644
--- a/tests/spec/oracle/generalized_check.0.res.oracle
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -10,13 +10,13 @@
[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check_f_valid_ko
-[wp] [Qed] Goal typed_f_ensures_f_init_x : Valid
-[wp] [Failed] Goal typed_lemma_easy_proof
+[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
+[wp] [Failed] Goal typed_check_lemma_easy_proof
[wp] [Qed] Goal typed_loop_loop_assigns : Valid
[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
-[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_established
-[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_preserved
-[wp] [Failed] Goal typed_main_call_f_requires_f_valid_x
+[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
+[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
+[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko
[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] Proved goals: 3 / 11