GitLab

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

---

Id	Project	Category	View	Due Date	Updated
ID0002344	Frama-C	Plug-in > wp	public	2018-01-19	2018-07-11

Reporter	abustany	Assigned To	correnson	Resolution	no change required
Priority	normal	Severity	minor	Reproducibility	always
Platform	x86_64	OS	Linux	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	Frama-C 17-Chlorine

Description :

FramaC version: Sulfur-20171101 (cannot select it in BTS because of #2343 (closed))

With the following C code:

---

#include <stdint.h> #include <string.h>

typedef struct { uint8_t a; uint8_t b; uint8_t c;

uint16_t d; uint16_t e; uint16_t f; char g[4086]; uint16_t h; } message_t;

/@ requires \valid(msg); @/ void reset_message(message_t *msg) { memset(msg, 0, sizeof(message_t)); }

---

Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c

produces the following unprovable goal:

---

Assume { (* Heap ) Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0). ( Pre-condition *) Have: valid_rw(Malloc_0, msg_0, 4093). } Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).

---

Using the Typed+cast model doesn't help.

I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.