Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002387Frama-CPlug-in > wppublic2018-07-11 09:142018-09-05 16:29
Reporterpmo 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C 16-Sulfur 
Target VersionFixed in Version 
Summary0002387: WP is not able to validate a statically declared structure followed by a memset
DescriptionBy 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));
}
Steps To Reproduceframa-c -wp-model typed_cast_ref -wp struc.c

TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006598)
correnson (manager)
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.
(0006599)
correnson (manager)
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`.
(0006600)
correnson (manager)
2018-07-23 14:19

Wrong usage of memory model Typed+cast

- Issue History
Date Modified Username Field Change
2018-07-11 09:14 pmo New Issue
2018-07-11 09:14 pmo Status new => assigned
2018-07-11 09:14 pmo Assigned To => correnson
2018-07-23 14:13 correnson Note Added: 0006598
2018-07-23 14:15 correnson Note Added: 0006599
2018-07-23 14:19 correnson Note Added: 0006600
2018-07-23 14:19 correnson Status assigned => resolved
2018-07-23 14:19 correnson Resolution open => no change required
2018-09-05 16:29 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker