diff --git a/src/plugins/wp/tests/wp_acsl/issue_A228.c b/src/plugins/wp/tests/wp_acsl/issue_A228.c new file mode 100644 index 0000000000000000000000000000000000000000..42d685b222fe18da00e9ca126b96c194e4da1cc5 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/issue_A228.c @@ -0,0 +1,34 @@ +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); +} 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 new file mode 100644 index 0000000000000000000000000000000000000000..e1e22036ebeeb00c2a9180ae68268033e3304f15 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle @@ -0,0 +1,11 @@ +# 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. diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e1e22036ebeeb00c2a9180ae68268033e3304f15 --- /dev/null +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle @@ -0,0 +1,11 @@ +# 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.