Failure to detect overflows into an allocated area within a struct
ID0002327: This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002327 | Frama-C | Plug-in > E-ACSL | public | 2017-08-24 | 2019-01-25 |
| Reporter | kvorobyov | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
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.