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);