Skip to content
Snippets Groups Projects
Commit 6e8d16b9 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[wp] restores a test

parent fa9e5f6e
No related branches found
No related tags found
No related merge requests found
/* run.config_qualif /* run.config_qualif
DONTRUN: [PB] temporary removed since a difference has to be validated.
*/
/* run.config_qualif
MODULE: @PTEST_DIR@/@PTEST_NAME@
OPT: -wp-par 1 OPT: -wp-par 1
*/ */
/* ZD : this should not be here such as it cannot be tested by all frama-c
developer
*/
/*@ axiomatic A { /*@ axiomatic A {
@ predicate P(int x); @ predicate P(int x);
......
# frama-c -wp [...]
[kernel] Parsing combined.c (with preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_assert : Unsuccess
[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_job_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_2_established : Valid
[wp] [Alt-Ergo] Goal typed_job_loop_invariant_3_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_3_established : Valid
[wp] [Alt-Ergo] Goal typed_job_assert_2 : Valid
[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_job_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_job_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_job_loop_assigns_2_part1 : Valid
[wp] [Qed] Goal typed_job_loop_assigns_2_part2 : Valid
[wp] [Alt-Ergo] Goal typed_job_loop_assigns_2_part3 : Valid
[wp] Proved goals: 13 / 14
Qed: 9
Alt-Ergo: 4 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 9 4 14 92.9%
------------------------------------------------------------
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