Frama-C Bug Tracking System - Frama-C
View Issue Details
0002327Frama-CPlug-in > E-ACSLpublic2017-08-24 15:502019-01-25 10:55
kvorobyov 
signoles 
normalminoralways
assignedopen 
 
 
0002327: Failure to detect overflows into an allocated area within a struct
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.

No tags attached.
Issue History
2017-08-24 15:50kvorobyovNew Issue
2017-08-24 15:50kvorobyovStatusnew => assigned
2017-08-24 15:50kvorobyovAssigned To => signoles
2017-08-24 15:50kvorobyovSummaryInability to detect overflows into allocated areas within a struct => Failure to detect overflows into an allocated area within a struct
2018-02-22 10:34signolesAssigned Tosignoles => fmaurica
2019-01-25 10:55signolesAssigned Tofmaurica => signoles

There are no notes attached to this issue.