Invalid sizeof(struct) calculation in Sulfur
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.