Commit 0668d534 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] run test for #775 also in plain config

parent 589e548c
/* run.config
DONTRUN: only usable in qualif config
OPT: -wp-gen -wp-prover why3
*/
/*@
logic boolean u8_continue_f(unsigned char b) =
0x80<=b && 0xC0 > b;
......
......@@ -12,7 +12,7 @@
Function u8_is_continue
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/boolean.i, line 11) in 'u8_is_continue':
Goal Post-condition (file tests/wp_acsl/boolean.i, line 12) in 'u8_is_continue':
Assume {
Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
If 128 <= b
......@@ -23,27 +23,26 @@ Assume {
}
Else { Have: u8_is_continue_0 = 0. }
}
Prove: (u8_is_continue_0 = 1) /\
((L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0)).
Prove: (L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0).
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (1/3):
Effect at line 15
Effect at line 16
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (2/3):
Effect at line 15
Effect at line 16
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (3/3):
Effect at line 15
Effect at line 16
Prove: true.
Prover Qed returns Valid
......
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