Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001066Frama-CPlug-in > Evapublic2012-01-19 13:082014-02-12 16:58
ReporterJochen 
Assigned Topascal 
PrioritynormalSeveritytrivialReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
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 Filesc file icon exm4.c [^] (86 bytes) 2012-01-19 13:08 [Show Content]

- 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.

- 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 Checkin
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
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker