Value abort because of Zero-sized location

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

---

Id	Project	Category	View	Due Date	Updated
ID0001907	Frama-C	Plug-in > Eva	public	2014-08-08	2015-03-17

Reporter	Anne	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Sodium

Description :

Value usually support structure types holding an array field with an undefined size, but in the attached case, it aborts with:

user error: Zero-sized location S_buf[0].chunk (type 'int []'). 
            Probably empty struct.
            Aborting

• Notice that the size of buf is defined since it is only a pointer.
• If buf is defined instead of just declared extern, the problem disappear.

Steps To Reproduce :

$ frama-c -val struct.c

Attachments

• struct.c