View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001647 | Frama-C | Plug-in > wp | public | 2014-02-17 15:58 | 2015-03-17 22:17 | ||||
Reporter | Anne | ||||||||
Assigned To | correnson | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Fixed in Version | Frama-C Sodium | |||||||
Summary | 0001647: compatibility between \null in ACSL and NULL in C in wp | ||||||||
Description | I 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... ;-) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|||
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 | Source_changeset_attached | => framac master 300363a6 |
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 |