0002327: Failure to detect overflows into an allocated area within a struct

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002327

Frama-C

Plug-in > E-ACSL

public

2017-08-24 15:50

2018-02-22 10:34

Reporter

kvorobyov

Assigned To

fmaurica

Priority

normal

Severity

minor

Reproducibility

always

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0002327: Failure to detect overflows into an allocated area within a struct

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.

Tags

No 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