Frama-C Bug Tracking System - Frama-C
View Issue Details
0001647Frama-CPlug-in > wppublic2014-02-17 15:582015-03-17 22:17
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Sodium 
Summary0001647: compatibility between \null in ACSL and NULL in C in wp
DescriptionI have tried to prove properties involving NULL pointers, and I had problem to write the ACSL part. Here is and example:
    ensures e1: \result == \null;
    ensures e2: \result == 0;
    ensures e3: \result == (int *) \null;
    ensures e4: \result == (int *) 0;
    ensures e5: \result == (int *)((void *)0);
int * f (void) {
  return NULL;

None of the properties are proved with the default memory model.
I finally manage to prove them with: -wp-model Typed+cast

Since NULL is used very often in programs, even with a clean typing, maybe something could be done for this special case ? Just a suggestion... ;-)
TagsNo tags attached.
Attached Files

2014-06-02 13:58   
Fix committed to master branch.

Issue History
2014-02-17 15:58AnneNew Issue
2014-02-17 15:58AnneStatusnew => assigned
2014-02-17 15:58AnneAssigned To => correnson
2014-06-02 13:58corrensonSource_changeset_attached => framac master 300363a6
2014-06-02 13:58corrensonNote Added: 0005177
2014-06-02 13:58corrensonStatusassigned => resolved
2014-06-02 13:58corrensonResolutionopen => fixed
2015-03-17 22:17signolesFixed in Version => Frama-C Sodium
2015-03-17 22:17signolesStatusresolved => closed