Validation fails when predicate is used with implicit type conversion.
ID0002229: This issue was created automatically from Mantis Issue 2229. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002229 | Frama-C | Plug-in > wp | public | 2016-05-31 | 2016-05-31 |
| Reporter | Ian | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Ubuntu | OS | - | OS Version | - |
| Product Version | Frama-C Magnesium | Target Version | - | Fixed in Version | - |
Description :
When there is an implicit type conversion on a parameter, and the value is checked by a predicate, validation fails when it should succeed.
In the example below, the functions foo and foo_pred have the same precondition, except foo_pred has the statement in a predicate. foo validates while foo_pred does not.
run2 validates the assertion, showing the precondition should be true, but foo_pred still fails.
run3 is similar to run2 except a ghost variable is used. This causes foo_pred to validate.
Steps To Reproduce :
File foo.c (attached): /*@ predicate bar_req(int i) = ((unsigned char) i) == i; */
//@ requires ((unsigned char) i) == i; void foo(int i) { }
//@ requires bar_req(i); void foo_pred(int i) { }
void run(char c) { unsigned char uc = c; foo(uc); // Valid foo_pred(uc); // Fails }
void run2(char c) { unsigned char uc = c; //@ assert ((unsigned char) ((int) uc)) == uc; foo_pred(uc); // Fails }
void run3(char c) { unsigned char uc = c; //@ ghost int ic = uc; //@ assert ((unsigned char) ic) == uc; foo_pred(uc); // Valid }
Run command: frama-c foo.c -wp -wp-prover why3:alt-ergo -wp-model=typed+Cast
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing foo.c (with preprocessing) [wp] warning: Missing RTE guards [wp] 6 goals scheduled [wp] [alt-ergo] Goal typed_cast_run2_call_foo_pred_pre : Unknown (158ms) [wp] [alt-ergo] Goal typed_cast_run_call_foo_pred_pre : Unknown (Qed:0.54ms) (157ms) [wp] Proved goals: 4 / 6 Qed: 3 alt-ergo: 1 (10ms) (unknown: 2)