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

[WP] fixes a typo in a test.

parent 086dbf67
No related branches found
No related tags found
No related merge requests found
Bool A, B; _Bool A, B;
/*@ /*@
ensures GOAL: \result ≡ 255; ensures GOAL: \result ≡ 255;
......
# frama-c -wp [...] # frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing) [kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing)
[kernel] :0: [wp] Running WP plugin...
syntax error: [wp] Warning: Missing RTE guards
Location: between <unknown> and 1:5, before or at token: A ------------------------------------------------------------
Function job
1 Bool A, B; ------------------------------------------------------------
2 Goal Post-condition 'GOAL' in 'job':
3 /*@ Assume { Type: is_bool(A) /\ is_bool(B). }
[kernel] Frama-C aborted: invalid user input. Prove: land(-64, lor(to_uint32(lsl(A, 6)), to_uint32(lsl(B, 7)))) = 192.
------------------------------------------------------------
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