Skip to content
Snippets Groups Projects
Commit 3f20b135 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

[WP] fixes smp_eq_with_lor (adds an integrity test)

parent 1a0a1a72
No related branches found
No related tags found
No related merge requests found
Bool A, B;
/*@
ensures GOAL: \result ≡ 255;
*/
unsigned job(void)
{
_Bool a0;
_Bool a1;
_Bool a2;
_Bool a3;
_Bool a4;
_Bool a5;
_Bool a6;
_Bool a7;
a0 = 1;
a1 = 1;
a2 = 1;
a4 = 1;
a3 = 1;
a5 = 1;
a6 = A;
a7 = B;
//*integrity_tests =
return
((unsigned int)a0 << 0) |
((unsigned int)a1 << 1) |
((unsigned int)a2 << 2) |
((unsigned int)a3 << 3) |
((unsigned int)a4 << 4) |
((unsigned int)a5 << 5) |
((unsigned int)a6 << 6) |
((unsigned int)a7 << 7);
}
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing)
[kernel] :0:
syntax error:
Location: between <unknown> and 1:5, before or at token: A
1 Bool A, B;
2
3 /*@
[kernel] Frama-C aborted: invalid user input.
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing)
[kernel] :0:
syntax error:
Location: between <unknown> and 1:5, before or at token: A
1 Bool A, B;
2
3 /*@
[kernel] Frama-C aborted: invalid user input.
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