Skip to content
Snippets Groups Projects
Commit 61445a7d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'feature/patrick/wp-fix-typo-in-test' into 'master'

[WP] fix typo in test

See merge request frama-c/frama-c!3048
parents 086dbf67 cf0e9471
No related branches found
No related tags found
No related merge requests found
Bool A, B;
/* run.config_qualif
OPT: -wp-steps 100
*/
_Bool A, B;
/*@
ensures GOAL: \result ≡ 255;
......
# 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.
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function job
------------------------------------------------------------
Goal Post-condition 'GOAL' in 'job':
Assume { Type: is_bool(A) /\ is_bool(B). }
Prove: land(-64, lor(to_uint32(lsl(A, 6)), to_uint32(lsl(B, 7)))) = 192.
------------------------------------------------------------
# frama-c -wp [...]
# frama-c -wp -wp-steps 100 [...]
[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.
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures_GOAL : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job - - 1 0.0%
------------------------------------------------------------
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