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:502017-08-25 10:37
Reporterkvorobyov 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker