diff --git a/src/plugins/wp/tests/inexistant-prover b/src/plugins/wp/tests/inexistant-prover deleted file mode 100644 index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000 diff --git a/src/plugins/wp/tests/wp_bts/issue_143.i b/src/plugins/wp/tests/wp_bts/issue_143.i deleted file mode 100644 index 555cbcb5b0889741e7ebe50de2d0713662fb9934..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/issue_143.i +++ /dev/null @@ -1,22 +0,0 @@ -/* run.config - DONTRUN: -*/ -/* run.config_qualif - EXECNOW: chmod a-x ./tests/inexistant-prover - OPT: -wp - OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo ./tests/inexistant-prover -wp-coqc ./tests/inexistant-prover - OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo ./tests/inexistant-prover - OPT: -wp -wp-prover "native:coq" -wp-coqc ./tests/inexistant-prover -*/ - -/*@ - axiomatic A { - lemma ok_because_inconsistent: \forall integer x; x > 0 ==> x < 0 ==> x == 0 ; - } -*/ - -/*@ - axiomatic B { - lemma ok_because_consistent: \forall integer x; x > 0 ==> x*x > 0 ; - } -*/ diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle deleted file mode 100644 index 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle +++ /dev/null @@ -1,14 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) -[wp] Running WP plugin... -[wp] 2 goals scheduled -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid -[wp] Proved goals: 2 / 2 - Qed: 0 - Alt-Ergo: 2 ------------------------------------------------------------- - Axiomatics WP Alt-Ergo Total Success - Axiomatic A - 1 1 100% - Axiomatic B - 1 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle deleted file mode 100644 index 08841f4f3a5743e7882829ae4b5b2530c704ef60..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle +++ /dev/null @@ -1,15 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: native support for coq is deprecated, use tip instead -[wp] 2 goals scheduled -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid -[wp] Proved goals: 2 / 2 - Qed: 0 - Alt-Ergo: 2 ------------------------------------------------------------- - Axiomatics WP Alt-Ergo Total Success - Axiomatic A - 1 1 100% - Axiomatic B - 1 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle deleted file mode 100644 index 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle +++ /dev/null @@ -1,14 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) -[wp] Running WP plugin... -[wp] 2 goals scheduled -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid -[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid -[wp] Proved goals: 2 / 2 - Qed: 0 - Alt-Ergo: 2 ------------------------------------------------------------- - Axiomatics WP Alt-Ergo Total Success - Axiomatic A - 1 1 100% - Axiomatic B - 1 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle deleted file mode 100644 index d2311a420b88dbc7cde3277638eeb95b8c6327b0..0000000000000000000000000000000000000000 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle +++ /dev/null @@ -1,16 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: native support for coq is deprecated, use tip instead -[wp] 2 goals scheduled -[wp] [Coq (native)] Goal typed_lemma_ok_because_consistent : Failed - Permission denied (./tests/inexistant-prover) -[wp] [Coq (native)] Goal typed_lemma_ok_because_inconsistent : Failed - Permission denied (./tests/inexistant-prover) -[wp] Proved goals: 0 / 2 - Coq (native): 0 (failed: 2) ------------------------------------------------------------- - Axiomatics WP Alt-Ergo Total Success - Axiomatic A - - 1 0.0% - Axiomatic B - - 1 0.0% -------------------------------------------------------------