suggest to use "NULL" rather than "&NULL" for null pointer
ID0001066: This issue was created automatically from Mantis Issue 1066. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001066 | Frama-C | Plug-in > Eva | public | 2012-01-19 | 2014-02-12 |
| Reporter | Jochen | Assigned To | pascal | Resolution | fixed |
| Priority | normal | Severity | trivial | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | Frama-C Oxygen-20120901 |
Description :
Running "frama-c -val exm4.c -no-unicode" on the attached program produces an output "p IN {{ &NULL ; &n }}", which is unusual and confusing for a C-programmer. I'd prefer to get "p IN {{ NULL ; &n }}" instead, which also resembles the C code in line 4 of the program.
From p.26 of file "value-analysis-Nitrogen-20111001.pdf", I understand that (void*)0, which I consider an absolute address, handled in the 2nd item under "A set of addresses", should be denoted as "NULL+0". The notation "&NULL", on the other hand, could be subsumed only under the 1st item on p.26, which seems to indicate that "NULL" denotes some variable. So I consider the output on exm4.c to be inconsistent with the explanations on p.26. The same applies to the use of "&NULL" on p.51 and later in the manual.