Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002344Frama-CPlug-in > wppublic2018-01-19 16:292018-07-11 15:40
Assigned Tocorrenson 
StatusclosedResolutionno change required 
Platformx86_64OSLinuxOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C 17-Chlorine 
Summary0002344: Invalid sizeof(struct) calculation in Sulfur
DescriptionFramaC version: Sulfur-20171101 (cannot select it in BTS because of 0002343)

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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
correnson (manager)
2018-01-19 17:10

You can not prove this function with the available memory models of the WP.

Using model Typed+Cast requires you to check that, when casting pointer types, memory writes are always re-read with exactly the same types.

However, the memset function typically violates this constraint : it writes *characters* but you want also to view the pointer as a struct.

To explain in further details :

The predicates valid_rw(...) of the Typed memory model compute sizes in number of _abstract cells_, not in term of characters. The struct contains 4093 individual cells (each is a mathematical integer), while its (void *) casted object contains 4098 individual cells (each is a mathematical integer representing a char).

Since you perform a pointer cast that violates the invariant of the Typed memory model, you face an inconsistency.
correnson (manager)
2018-01-19 17:13

For your information, we have lower-level memory models in development to address such an issue, but we have no release date for it. As a work around, you must annotate your code and call another function
with an ACSL contract that explicitly assigns 0 to all fields of the structure.

- Issue History
Date Modified Username Field Change
2018-01-19 16:29 abustany New Issue
2018-01-19 16:29 abustany Status new => assigned
2018-01-19 16:29 abustany Assigned To => correnson
2018-01-19 17:10 correnson Note Added: 0006509
2018-01-19 17:10 correnson Status assigned => resolved
2018-01-19 17:10 correnson Resolution open => no change required
2018-01-19 17:13 correnson Note Added: 0006510
2018-07-11 15:33 signoles Fixed in Version => Frama-C 16-Sulfur
2018-07-11 15:34 signoles Status resolved => closed
2018-07-11 15:34 signoles Note Added: 0006579
2018-07-11 15:35 signoles Note Deleted: 0006579
2018-07-11 15:35 signoles Fixed in Version Frama-C 16-Sulfur =>
2018-07-11 15:40 signoles Fixed in Version => Frama-C 17-Chlorine

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker