Frama-C Bug Tracking System - Frama-C
View Issue Details
0002387Frama-CPlug-in > wppublic2018-07-11 09:142018-09-05 16:29
closedno change required 
Frama-C 16-Sulfur 
0002387: WP is not able to validate a statically declared structure followed by a memset
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));
frama-c -wp-model typed_cast_ref -wp struc.c

No tags attached.
Issue History
2018-07-11 09:14pmoNew Issue
2018-07-11 09:14pmoStatusnew => assigned
2018-07-11 09:14pmoAssigned To => correnson
2018-07-23 14:13corrensonNote Added: 0006598
2018-07-23 14:15corrensonNote Added: 0006599
2018-07-23 14:19corrensonNote Added: 0006600
2018-07-23 14:19corrensonStatusassigned => resolved
2018-07-23 14:19corrensonResolutionopen => no change required
2018-09-05 16:29signolesStatusresolved => closed

2018-07-23 14:13   
According to the WP manual (ยง 2.4.3) using the `+cast` memory model is generally unsound.
When WP emits warnings, the user shall perform manual code review and check if the selected memory model still applies.

In this particular situation, there is no available memory model in WP that applies to memset pre-condition.
For the Typed memory model to be sound, objects in memory must be accessed with a unique single type.
By default, the memory model soundly generates stronger proof obligations on each cast, which generally makes properties unprovable (false negative) but never prove incorrect properties (false positive).

To account for necessary casts in C-programs, the memory model can be less restrictive with option -wp-model +cast. In this case, warnings are emitted on each casts, and the user shall verify by manual code review that actual memory access never change the type of the data.

In function 'notclean_but_valid', pointer b is allocated with an array of 8 chars, then casted into a pointer `stest *`, then casted back to `void *` by memset. There is no access to `(stest *)b`, and only to `(void *)(stest *)b`. Finally, b is always accessed as an array of char, hence this is OK for the memory model.

In function 'clean_but_invalid', b is allocated a single stest structure, and its address is casted into a pointer to `(void *)` and passed to memset. Finally, b is not always accessed with the same type, which is NOT OK for the memory model, and the WP results are inconsistent.
2018-07-23 14:15   
With default memory model, emitted warnings are :

[wp] work/memset.c:19: Warning:
  Cast with incompatible pointers types (source: __anonstruct_stest_1*)
     (target: sint8*)
[wp] work/memset.c:13: Warning:
  Cast with incompatible pointers types (source: __anonstruct_stest_1*)
     (target: sint8*)
[wp] work/memset.c:11: Warning:
  Cast with incompatible pointers types (source: sint8*)
     (target: __anonstruct_stest_1*)

Properties are *not* proved, and WP informs you that stronger proof obligations have been generated.
Remark that properties get status `Unknow` and not `Invalid`.
2018-07-23 14:19   
Wrong usage of memory model Typed+cast