compatibility between \null in ACSL and NULL in C in wp
ID0001647: This issue was created automatically from Mantis Issue 1647. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001647 | Frama-C | Plug-in > wp | public | 2014-02-17 | 2015-03-17 |
| Reporter | Anne | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C Sodium |
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... ;-)