Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001647Frama-CPlug-in > wppublic2014-02-17 15:582015-03-17 22:17
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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

- Relationships

-  Notes
(0005177)
correnson (manager)
2014-06-02 13:58

Fix committed to master branch.

- Issue History
Date Modified Username Field Change
2014-02-17 15:58 Anne New Issue
2014-02-17 15:58 Anne Status new => assigned
2014-02-17 15:58 Anne Assigned To => correnson
2014-06-02 13:58 correnson Note Added: 0005177
2014-06-02 13:58 correnson Status assigned => resolved
2014-06-02 13:58 correnson Resolution open => fixed
2015-03-17 22:17 signoles Fixed in Version => Frama-C Sodium
2015-03-17 22:17 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker