GitLab

ID0002327: This issue was created automatically from Mantis Issue 2327. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002327	Frama-C	Plug-in > E-ACSL	public	2017-08-24	2019-01-25

Reporter	kvorobyov	Assigned To	signoles	Resolution	open
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	-

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.