Skip to content
Snippets Groups Projects
Commit 15fe85ab authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[spec] remove wp debug infos from check test

parent cbed8092
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/spec/generalized_check.i
+ 1
− 1
View file @ 15fe85ab
/* 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
......
tests/spec/oracle/generalized_check.0.res.oracle
+ 0
− 255
View file @ 15fe85ab
[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;
*/
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment