Skip to content
Snippets Groups Projects
Commit 137b8fd6 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Removes a test related to native Alt-Ergo

parent 60782321
No related branches found
No related tags found
No related merge requests found
...@@ -4,7 +4,6 @@ ...@@ -4,7 +4,6 @@
/* run.config_qualif /* run.config_qualif
OPT: -wp-timeout 1 OPT: -wp-timeout 1
OPT: -wp-prover native:alt-ergo -wp-timeout 1
OPT: -wp-prover native:coq OPT: -wp-prover native:coq
*/ */
......
# frama-c -wp -wp-timeout 1 [...] # frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing) [kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
[wp] Running WP plugin... [wp] Running WP plugin...
[wp] Warning: Missing RTE guards [wp] Warning: Missing RTE guards
[wp] Warning: native support for alt-ergo is deprecated, use why3 instead [wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled [wp] 1 goal scheduled
[wp] [Alt-Ergo (native)] Goal typed_foo_assert_ko : Unsuccess [wp] [Coq] Goal typed_foo_assert_ko : Default tactic
[wp] [Coq (native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1 [wp] Proved goals: 0 / 1
Alt-Ergo (native): 0 (unsuccess: 1) Coq (native): 0 (unsuccess: 1)
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
foo - - 1 0.0% foo - - 1 0.0%
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/bts_2471.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 1 goal scheduled
[wp] [Coq] Goal typed_foo_assert_ko : Default tactic
[wp] [Coq (native)] Goal typed_foo_assert_ko : Unsuccess
[wp] Proved goals: 0 / 1
Coq (native): 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 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