From f4e86d8b87c2d9fe3da024d4c7565b9c5f8416bf Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 16:35:35 +0200
Subject: [PATCH] [wp] do not put 'check lemma' in environment.
---
src/plugins/wp/wpAnnot.ml | 5 +-
src/plugins/wp/wpStrategy.ml | 14 +--
tests/spec/generalized_check.i | 4 +-
.../spec/oracle/generalized_check.res.oracle | 100 +++++++++++++++++-
4 files changed, 108 insertions(+), 15 deletions(-)
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index e68b7671388..c7b32888e74 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -1122,8 +1122,9 @@ let add_global_annotations annots =
"Global invariant not handled yet ('%s' ignored)"
linfo.l_var_info.lv_name;
()
- | Dlemma (name,_,_,_,_,_,_) ->
- WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
+ | Dlemma (name,_,_,_,p,_,_) ->
+ if not (p.tp_only_check) then
+ WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
and do_globals gs = List.iter do_global gs in
(*[LC]: forcing order of iteration: hash is not the same on 32 and 64 bits *)
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index b76d3460d67..2e794fbc65e 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -163,13 +163,13 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
let add_prop_fct_pre acc kind kf bhv ~assumes pre =
if pre.ip_content.tp_only_check then acc else begin
- let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
- let labels = NormAtLabels.labels_fct_pre in
- let p = Logic_const.pred_of_id_pred pre in
- let p = Logic_const.(pat (p,pre_label)) in
- let p = normalize id ?assumes labels p in
- add_prop acc kind id p
-end
+ let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
+ let labels = NormAtLabels.labels_fct_pre in
+ let p = Logic_const.pred_of_id_pred pre in
+ let p = Logic_const.(pat (p,pre_label)) in
+ let p = normalize id ?assumes labels p in
+ add_prop acc kind id p
+ end
let add_prop_fct_post acc kind kf bhv tkind post =
let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 856e33415fc..06d4c500341 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,7 +1,7 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key no-time-info -print
+OPT: -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
*/
-/*@ check lemma tauto: \true ==> \true; */
+/*@ check lemma easy_proof: \false; */ // should not be put in any environment
/*@ check requires \valid(x);
assigns *x;
diff --git a/tests/spec/oracle/generalized_check.res.oracle b/tests/spec/oracle/generalized_check.res.oracle
index e8a2ec027c9..bb54dad662f 100644
--- a/tests/spec/oracle/generalized_check.res.oracle
+++ b/tests/spec/oracle/generalized_check.res.oracle
@@ -1,17 +1,109 @@
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
[wp] Running WP plugin...
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] take f_assigns *x;
+[wp:strategy] [add_node_annots] on <stmt-1>
+[wp:strategy] [add_node_annots] on <stmt-2>
+[wp:strategy] [add_node_annots] on <stmt-10>
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] [add_node_annots] on <stmt-5>
+[wp:strategy] [add_node_annots] on <callIn-6>
+[wp:strategy] take main_assigns *x;
+[wp:strategy] [add_node_annots] on <callIn-6>
+[wp:strategy] [add_node_annots] on <stmt-7>
+[wp:strategy] [add_node_annots] on <stmt-8>
+[wp:strategy] [add_node_annots] on <stmt-12>
[wp] Warning: Missing RTE guards
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check
[wp] [Qed] Goal typed_f_ensures : Valid
-[wp] [Qed] Goal typed_lemma_tauto : Valid
+[wp] [Failed] Goal typed_lemma_easy_proof
[wp] [Qed] Goal typed_main_call_f_requires : Valid
[wp] [Failed] Goal typed_main_check
-[wp] Proved goals: 4 / 6
- Qed: 4
+[wp] Proved goals: 3 / 6
+ Qed: 3
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'f' is NOT the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
+[wp:strategy] 'main' is the main entry point
/* Generated by Frama-C */
-/*@ check lemma tauto: \true;
+/*@ check lemma easy_proof: \false;
*/
/*@ check requires \valid(x);
check ensures *\old(x) ≡ 0;
--
GitLab