Skip to content
Snippets Groups Projects
Commit b6323d44 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] update test case for generalized check

parent 5901dc9f
No related branches found
No related tags found
No related merge requests found
/* run.config
OPT: -wp -wp-prover qed -wp-msg-key no-time-info -print
*/
/*@ check lemma tauto: \true ==> \true; */
/*@ check requires \valid(x);
......
[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Qed] Goal typed_f_check : Valid
[wp] [Qed] Goal typed_f_ensures : Valid
[wp] [Qed] Goal typed_lemma_tauto : Valid
[wp] [Qed] Goal typed_main_call_f_requires : Valid
[wp] [Failed] Goal typed_main_check
[wp] Proved goals: 5 / 6
Qed: 5
/* Generated by Frama-C */
/*@ check lemma tauto: \true;
*/
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment