[wp] do not put 'check lemma' in environment.

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 *)

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

tests/spec/generalized_check.i

 /* 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;

tests/spec/oracle/generalized_check.res.oracle

 [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;