0001066: suggest to use "NULL" rather than "&NULL" for null pointer

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001066

Frama-C

Plug-in > Eva

public

2012-01-19 13:08

2014-02-12 16:58

Reporter

Jochen

Assigned To

pascal

Priority

normal

Severity

trivial

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Nitrogen-20111001

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0001066: suggest to use "NULL" rather than "&NULL" for null pointer

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.

Tags

No tags attached.

Attached Files

exm4.c [^] (86 bytes) 2012-01-19 13:08 [Show Content] [Hide Content]

#define NULL	((void*)0)
void main (int n){
    int *p;
    p = (n < 0 ? NULL : &n);
}

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