diff --git a/src/plugins/wp/tests/wp_plugin/combined.c b/src/plugins/wp/tests/wp_plugin/combined.c index 3e0939d7e6c26c905132d3df106f33df59cd3f6d..5123a528dd6d8fb6a6ebf777cb0a997d2bb58d02 100644 --- a/src/plugins/wp/tests/wp_plugin/combined.c +++ b/src/plugins/wp/tests/wp_plugin/combined.c @@ -1,15 +1,15 @@ /* 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 */ -/* ZD : this should not be here such as it cannot be tested by all frama-c - developer - */ + + + + + + + + /*@ axiomatic A { @ predicate P(int x); diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..4cb64dc0e51cdf7abae9c230ef9a5ca1a218e650 --- /dev/null +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle @@ -0,0 +1,26 @@ +# 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% +------------------------------------------------------------