Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
frama-c
Commits
51e29781
Commit
51e29781
authored
Dec 19, 2019
by
Virgile Prevosto
Browse files
[WP] add test to check goal for #775 is correctly generated by Why3 API
parent
951c5398
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/plugins/wp/tests/wp_acsl/boolean.i
0 → 100644
View file @
51e29781
/* run.config
OPT: -wp-prover alt-ergo -wp-gen
*/
/*@
logic boolean u8_continue_f(unsigned char b) =
0x80<=b && 0xC0 > b;
*/
/*@
assigns \nothing;
ensures u8_continue_f(b) == \result==1;
*/
int
u8_is_continue
(
const
unsigned
char
b
)
{
return
b
>=
0x80
&
&
b
<=
0xBF
;
}
src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
0 → 100644
View file @
51e29781
# 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] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
[wp] 4 goals generated
------------------------------------------------------------
Function u8_is_continue
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/boolean.i, line 11) in 'u8_is_continue':
Assume {
Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
If 128 <= b
Then {
If b <= 191
Then { Have: u8_is_continue_0 = 1. }
Else { Have: u8_is_continue_0 = 0. }
}
Else { Have: u8_is_continue_0 = 0. }
}
Prove: (u8_is_continue_0 = 1) /\
((L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0)).
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (1/3):
Effect at line 15
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (2/3):
Effect at line 15
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (3/3):
Effect at line 15
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment