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

[wp-qualif] remove obsolete test

parent 34787ee2
No related branches found
No related tags found
No related merge requests found
/* 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 ;
}
*/
# 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%
------------------------------------------------------------
# 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%
------------------------------------------------------------
# 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%
------------------------------------------------------------
# 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%
------------------------------------------------------------
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