diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i index e65573c02330b3aa9d5d5fd24a82f8e61cf555b2..a343867864c885583b62d5690fcd68a0f52852f2 100644 --- a/tests/spec/generalized_check.i +++ b/tests/spec/generalized_check.i @@ -1,5 +1,5 @@ /* run.config -OPT: -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print +OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info -print OPT: -eva -eva-use-spec f */ /*@ check lemma easy_proof: \false; */ // should not be put in any environment diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle index eca824fbeedb4d37a9498e1516b96a8492cfdfc0..96bfee08beaee612be122e2def628a9d06ad025e 100644 --- a/tests/spec/oracle/generalized_check.0.res.oracle +++ b/tests/spec/oracle/generalized_check.0.res.oracle @@ -1,257 +1,12 @@ [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-38> -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] [add_node_annots] on <stmt-17> -[wp:strategy] [add_node_annots] on <stmt-19> -[wp:strategy] [add_node_annots] on <testIn-22> -[wp:strategy] [add_node_annots] on <stmt-23> -[wp:strategy] [add_node_annots] on <stmt-25> -[wp:strategy] [add_node_annots] on <stmt-26> [wp] tests/spec/generalized_check.i:29: Warning: Unsupported generalized invariant, use loop invariant instead. Ignored invariant check invariant \true; -[wp:strategy] [add_node_annots] on <stmt-27> -[wp:strategy] [add_node_annots] on <testIn-30> -[wp:strategy] [add_node_annots] on <stmt-31> -[wp:strategy] [add_node_annots] on <stmt-33> -[wp:strategy] [add_node_annots] on <stmt-34> -[wp:strategy] [add_node_annots] on <stmt-35> -[wp:strategy] [add_node_annots] on <stmt-42> -[wp:strategy] [add_loop_annots] on <loop-20> -[wp:strategy] [add_loop_annots] 1 edges_to_head -[wp:strategy] [add_loop_annots] 2 edges_to_loop -[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges -[wp:strategy] [add_loop_annots on entry_edges ok] -[wp:strategy] [add_loop_annots on back_edges ok] -[wp:strategy] [add_loop_annots on edges_to_head ok] -[wp:strategy] take loop_loop_assigns i; -[wp:strategy] take loop_loop_assigns i; -[wp:strategy] [add_loop_annots] on <loop-20> -[wp:strategy] [add_loop_annots] 1 edges_to_head -[wp:strategy] [add_loop_annots] 2 edges_to_loop -[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges -[wp:strategy] [add_loop_annots on entry_edges ok] -[wp:strategy] [add_loop_annots on back_edges ok] -[wp:strategy] [add_loop_annots on edges_to_head ok] -[wp:strategy] [add_loop_annots] on <loop-27> -[wp:strategy] [add_loop_annots] 1 edges_to_head -[wp:strategy] [add_loop_annots] 2 edges_to_loop -[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges -[wp:strategy] [add_loop_annots on entry_edges ok] -[wp:strategy] [add_loop_annots on back_edges ok] -[wp:strategy] [add_loop_annots on edges_to_head ok] -[wp:strategy] [add_loop_annots] on <loop-27> -[wp:strategy] [add_loop_annots] 1 edges_to_head -[wp:strategy] [add_loop_annots] 2 edges_to_loop -[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges -[wp:strategy] [add_loop_annots on entry_edges ok] -[wp:strategy] [add_loop_annots on back_edges ok] -[wp:strategy] [add_loop_annots on edges_to_head ok] -[wp:strategy] [add_node_annots] on <blkIn-stmt:18> -[wp:strategy] 'main' is the main entry point -[wp:strategy] [add_node_annots] on <stmt-5> -[wp:strategy] [add_node_annots] on <stmt-6> -[wp:strategy] [add_node_annots] on <testIn-8> -[wp:strategy] [add_node_annots] on <stmt-9> -[wp:strategy] [add_node_annots] on <callIn-11> -[wp:strategy] take main_assigns *x; -[wp:strategy] [add_node_annots] on <callIn-11> -[wp:strategy] [add_node_annots] on <stmt-12> -[wp:strategy] [add_node_annots] on <stmt-13> -[wp:strategy] [add_node_annots] on <callIn-14> -[wp:strategy] [add_node_annots] on <callIn-14> -[wp:strategy] [add_node_annots] on <stmt-15> -[wp:strategy] [add_node_annots] on <stmt-40> [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] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point [wp] tests/spec/generalized_check.i:36: Warning: Missing assigns clause (assigns 'everything' instead) -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' 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: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] 11 goals scheduled [wp] [Qed] Goal typed_f_assigns : Valid [wp] [Failed] Goal typed_f_check_f_valid_ko @@ -266,16 +21,6 @@ [wp] [Failed] Goal typed_main_check_main_valid_ko [wp] Proved goals: 3 / 11 Qed: 3 -[wp:strategy] 'f' is NOT the main entry point -[wp:strategy] 'f' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' is NOT the main entry point -[wp:strategy] 'loop' 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 /* Generated by Frama-C */ /*@ check lemma easy_proof: \false; */