| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 0002327 | Frama-C | Plug-in > E-ACSL | public | 2017-08-24 15:50 | 2019-01-25 10:55 | ||||||||
| Reporter | kvorobyov | ||||||||||||
| Assigned To | signoles | ||||||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||||||
| Status | assigned | Resolution | open | ||||||||||
| Product Version | |||||||||||||
| Target Version | Fixed in Version | ||||||||||||
| Summary | 0002327: Failure to detect overflows into an allocated area within a struct | ||||||||||||
| Description | Presently E-ACSL treats structs as single units of program allocation issuing one call to `store_block` per struct. Such an approach fails to detect overflows within structs. Consider, for instance, the following program: int main() { struct node { char buf1[8]; char buf2[8]; } n; /*@assert manual_assertion: \valid(&n.buf1[12]); */ n.buf1[12] = '0'; return 0; } This program results in an overflow via assignment n.buf1[12] = '0'; that accesses buffer n.buf2 via n.buf1. However, since E-ACSL treats n as a single memory block the issue is not detected. | ||||||||||||
| Tags | No tags attached. | ||||||||||||
| Attached Files |
| ||||||||||||
 Relationships |
|
 Relationships |
| Notes |
|
| There are no notes attached to this issue. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2017-08-24 15:50 | kvorobyov | New Issue | |
| 2017-08-24 15:50 | kvorobyov | Status | new => assigned |
| 2017-08-24 15:50 | kvorobyov | Assigned To | => signoles |
| 2017-08-24 15:50 | kvorobyov | Summary | Inability to detect overflows into allocated areas within a struct => Failure to detect overflows into an allocated area within a struct |
| 2018-02-22 10:34 | signoles | Assigned To | signoles => fmaurica |
| 2019-01-25 10:55 | signoles | Assigned To | fmaurica => signoles |
| Issue History |