2021-01-15 16:04 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001066Frama-CPlug-in > Evapublic2012-01-19 13:082014-02-12 16:58
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytrivialReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001066: suggest to use "NULL" rather than "&NULL" for null pointer
DescriptionRunning "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.
TagsNo tags attached.
Attached Files
  • c file icon exm4.c (86 bytes) 2012-01-19 13:08 - 
    #define NULL	((void*)0)
void main (int n){
    int *p;
    p = (n < 0 ? NULL : &n);
}
    c file icon exm4.c (86 bytes) 2012-01-19 13:08 +

-Relationships
+Relationships

-Notes

~0002594

pascal (reporter)

2012-01-19 13:58

 Thanks for the suggestion. Your example now shows:
          p IN {{ NULL ; &n }}

Note that the C programmer should still be careful, because the offsets that may be displayed do not correspond to pointer arithmetics: they always are in bytes.

~0004687

pascal (reporter)

2014-02-12 16:58

 Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-01-19 13:08 Jochen New Issue
2012-01-19 13:08 Jochen Status new => assigned
2012-01-19 13:08 Jochen Assigned To => pascal
2012-01-19 13:08 Jochen File Added: exm4.c
2012-01-19 13:58 pascal Note Added: 0002594
2012-01-19 13:59 svn
2012-01-19 13:59 svn Status assigned => resolved
2012-01-19 13:59 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:11 pascal Source_changeset_attached => framac master e57ce19f
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon e57ce19f
2014-02-12 16:58 pascal Note Added: 0004687
2014-02-12 16:58 pascal Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva
+Issue History