diff --git a/src/plugins/wp/tests/wp_acsl/issue_A228.c b/src/plugins/wp/tests/wp_acsl/issue_A228.c index 42d685b222fe18da00e9ca126b96c194e4da1cc5..6d970cf28e18bee00ab8f5c400e8cb30f63f446b 100644 --- a/src/plugins/wp/tests/wp_acsl/issue_A228.c +++ b/src/plugins/wp/tests/wp_acsl/issue_A228.c @@ -1,4 +1,4 @@ -Bool A, B; +_Bool A, B; /*@ ensures GOAL: \result ≡ 255; diff --git a/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle index e1e22036ebeeb00c2a9180ae68268033e3304f15..e06b9fc16c191c84b483440214cf11e0e8bcf83b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle @@ -1,11 +1,13 @@ # 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. + +------------------------------------------------------------