diff --git a/src/plugins/wp/tests/wp_acsl/issue_A228.c b/src/plugins/wp/tests/wp_acsl/issue_A228.c index 42d685b222fe18da00e9ca126b96c194e4da1cc5..b932e59a30de624d5d52ac91c69800c2769cddd6 100644 --- a/src/plugins/wp/tests/wp_acsl/issue_A228.c +++ b/src/plugins/wp/tests/wp_acsl/issue_A228.c @@ -1,4 +1,8 @@ -Bool A, B; +/* run.config_qualif + OPT: -wp-steps 100 + */ + +_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. + +------------------------------------------------------------ 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 index e1e22036ebeeb00c2a9180ae68268033e3304f15..8adf68309015606cea75c814a2fa5472a946b6c3 100644 --- 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 @@ -1,11 +1,12 @@ -# 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% +------------------------------------------------------------