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 |
|
![]() |
|||
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 |