From 15fe85abd3bb9d44e3b9716b3fb9b362962e25b6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Wed, 9 Sep 2020 15:25:57 +0200 Subject: [PATCH] [spec] remove wp debug infos from check test --- tests/spec/generalized_check.i | 2 +- .../oracle/generalized_check.0.res.oracle | 255 ------------------ 2 files changed, 1 insertion(+), 256 deletions(-) diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i index e65573c0233..a343867864c 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 eca824fbeed..96bfee08bea 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; */ -- GitLab