Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002327Frama-CPlug-in > E-ACSLpublic2017-08-24 15:502019-01-25 10:55
Assigned Tosignoles 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002327: Failure to detect overflows into an allocated area within a struct
DescriptionPresently 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- 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

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker