A valid pointer to an empty struct generate a failure

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

---

Id	Project	Category	View	Due Date	Updated
ID0001700	Frama-C	Plug-in > E-ACSL	public	2014-03-14	2014-09-15

Reporter	ploc	Assigned To	guillaume-petiot	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Neon-20140301	Target Version	-	Fixed in Version	-

Description :

In memory_model/e_acsl_mmodel.c, line 328, you had assert(size > 0);

However if the struct is empty: struct toto {}; A valid pointer to toto will have size 0 but still be a valid use.

You should have assert(size >= 0);