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