Skip to content
Snippets Groups Projects
Commit 1a11dfa8 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] test for fixed non-terminating strategy

parent 679edcaf
No related branches found
No related tags found
No related merge requests found
# frama-c -wp [...]
[kernel] Parsing terminating.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
[wp] [Unsuccess] typed_lemma_dummy (Tactics 2) (Qed)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
Global
------------------------------------------------------------
Goal Lemma 'dummy':
Assume { Have: i < 0. }
Prove: j < 0.
Prover Alt-Ergo returns Unsuccess
Prover Script returns Unsuccess
------------------------------------------------------------
Subgoal 1/1:
- Lemma 'dummy'
- Filter (Filter)
- Filter (Filter)
Goal Wp.Tactical.typed_lemma_dummy-1 (generated):
Prove: j < 0.
------------------------------------------------------------
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma - - 1 0.0%
------------------------------------------------------------
/* run.config
DONTRUN:
*/
/* run.config_qualif
OPT: -wp-status -wp-prover tip -wp-script dry
*/
/*@ lemma dummy: \forall integer i,j; i < 0 ==> j < 0; */
/*@
strategy FastAltErgo: \prover("alt-ergo", 1); // run Alt-Ergo for 1 sec.
strategy EagerAltErgo: \prover("alt-ergo",10); // run Alt-Ergo for 10 sec.
strategy FilterProver:
FastAltErgo,
\tactic("Wp.filter"
,\goal(_)
,\children(EagerAltErgo)
),
EagerAltErgo;
proof FilterProver: dummy;
*/
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