| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0002354 | Frama-C | Plug-in > RTE | public | 2018-02-03 12:15 | 2018-11-30 10:07 | ||||
| Reporter | xleroy | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C 16-Sulfur | ||||||||
| Target Version | Fixed in Version | Frama-C 18-Argon | |||||||
| Summary | 0002354: RTE assertion for signed right shift is wrong | ||||||||
| 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. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
signoles (manager) 2018-10-15 17:17 |
A new kernel option (-warn-right-shift-negative) has been introduced for controlling this behaviour. It is deactivated by default (while -warn-left-shift-negative is activated by default), hence no assertion is now emitted by default on your example. This option is supported by plug-ins Eva and RTE. The assertions generated by RTE impact plug-ins E-ACSL and WP. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2018-02-03 12:15 | xleroy | New Issue | |
| 2018-02-03 12:15 | xleroy | Status | new => assigned |
| 2018-02-03 12:15 | xleroy | Assigned To | => signoles |
| 2018-10-15 17:17 | signoles | Note Added: 0006664 | |
| 2018-10-15 17:17 | signoles | Status | assigned => resolved |
| 2018-10-15 17:17 | signoles | Resolution | open => fixed |
| 2018-11-30 10:07 | signoles | Fixed in Version | => Frama-C 18-Argon |
| 2018-11-30 10:07 | signoles | Status | resolved => closed |
| Issue History |