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-01-19 17:13
Reporterabustany 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionno change required 
Platformx86_64OSLinuxOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
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
(0006509)
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.
(0006510)
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker