2021-03-05 01:34 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002327Frama-CPlug-in > E-ACSLpublic2019-01-25 10:55
Assigned Tosignoles 
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


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
+Issue History