WP is not able to validate a statically declared structure followed by a memset
ID0002387: This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.
Id | Project | Category | View | Due Date | Updated |
---|---|---|---|---|---|
ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
Reporter | pmo | Assigned To | correnson | Resolution | no change required |
Priority | normal | Severity | major | Reproducibility | always |
Platform | - | OS | - | OS Version | - |
Product Version | Frama-C 16-Sulfur | Target Version | - | Fixed in Version | - |
Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct { int i; float f; } stest;
void notclean_but_valid() { char b[sizeof(stest)]; stest *s = b;
memset(s, 0, sizeof(stest)); }
void clean_but_invalid() { stest s;
memset(&s, 0, sizeof(stest)); }
Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.c