Commit 1d741169 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[WP] avoid using -wp-gen -wp-prover why3:xxx in tests on non-qualif config

parent 51e29781
/* run.config
OPT: -wp-prover alt-ergo -wp-gen
DONTRUN: only usable in qualif config
*/
/*@
logic boolean u8_continue_f(unsigned char b) =
......@@ -8,7 +8,7 @@ OPT: -wp-prover alt-ergo -wp-gen
/*@
assigns \nothing;
ensures u8_continue_f(b) == \result==1;
ensures u8_continue_f(b) == \result;
*/
int u8_is_continue(const unsigned char b)
{
......
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1,
"rank": 10 },
"qed": { "total": 3, "valid": 3 },
"wp:main": { "total": 4, "valid": 4, "rank": 10 } },
"wp:functions": { "u8_is_continue": { "u8_is_continue_assigns": { "qed":
{ "total": 3,
"valid": 3 },
"wp:main":
{ "total": 3,
"valid": 3 } },
"u8_is_continue_ensures": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"valid": 1,
"rank": 10 },
"wp:main":
{ "total": 1,
"valid": 1,
"rank": 10 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"valid": 1,
"rank": 10 },
"qed": { "total": 3,
"valid": 3 },
"wp:main": { "total": 4,
"valid": 4,
"rank": 10 } } } } }
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_u8_is_continue_ensures : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
[wp] Proved goals: 4 / 4
Qed: 3
Alt-Ergo 2.0.0: 1
[wp] Report in: 'tests/wp_acsl/oracle_qualif/boolean.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/boolean.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
u8_is_continue 3 1 (36..48) 4 100%
-------------------------------------------------------------
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment