RTE assertion for signed right shift is wrong
ID0002354: This issue was created automatically from Mantis Issue 2354. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002354 | Frama-C | Plug-in > RTE | public | 2018-02-03 | 2018-11-30 |
| Reporter | xleroy | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | Frama-C 18-Argon |
Description :
Consider:
/*@ ensures \result == arg >> 2; */
int toto(int arg) { return arg >> 2; }
"frama-c -wp -wp-rte" fails to verify this rather tautological spec because the RTE pass inserts the assertion
/*@ assert rte: shift: 0 ≤ arg; */
I think this is an incorrect reading of the ISO C 90 and C 99 specs: right-shift of a signed integer expression that has a negative value is implementation-defined, but is not an undefined behavior. (See ISO C 99 section 6.5.7 item 5.)
I would suggest that WP and RTE accept the spec above, so that I can actually reason about the right shift, probably by adding axioms specifying how right shifts of negative numbers work on the platforms I am (and everyone is) interested in.