Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002256Frama-CPlug-in > Evapublic2016-11-11 14:232017-12-17 21:03
Assigned Tomaroneze 
PlatformOSxubuntuOS Version
Product VersionFrama-C Aluminium 
Target VersionFrama-C 15-PhosphorusFixed in Version 
Summary0002256: "pointer comparison" warning emitted for "p==NULL"
DescriptionRunning "frama-c -val -val-warn-undefined-pointer-comparison=pointer ptrcmp3.c" on the attached file results in a warning:

ptrcmp3.c:10:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)p, (void *)0);

The warning disappears if
1. the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
2. the "assigns" clause for "foo" is deleted.

The warning seems strange by itself, as every pointer should be comparable to NULL. The changes that make the warning disappear (in particular 1.) support the hypothesis that this is a bug.
TagsNo tags attached.
Attached Filesc file icon ptrcmp3.c [^] (178 bytes) 2016-11-11 14:23 [Show Content]

- Relationships

-  Notes
yakobowski (manager)
2017-03-06 11:15

Indeed. \pointer_comparable actually means 2 things:
1. the comparison of the two pointer values is valid according to the C standard
2. the pointer values themselves are valid or "past-one".

Here, the second check fails, and the predicate returns Unknown. This is not really satisfactory, as we should emit a specific alarm about this somewhere else (probably at the call-site of 'foo'), and dedicate \pointer_comparable to comparisons only. However, this comes with its own set of problems...

In Phosphorus, we are however going to change the default modelisation for functions returning a pointer. So you won't get a garbled mix here, and the comparison should be flagged as ok.
yakobowski (manager)
2017-12-17 21:02

Still not done in Sulfur.

- Issue History
Date Modified Username Field Change
2016-11-11 14:23 Jochen New Issue
2016-11-11 14:23 Jochen Status new => assigned
2016-11-11 14:23 Jochen Assigned To => yakobowski
2016-11-11 14:23 Jochen File Added: ptrcmp3.c
2017-03-06 11:15 yakobowski Note Added: 0006372
2017-03-06 11:35 yakobowski Target Version => Frama-C 15-Phosphorus
2017-12-17 21:02 yakobowski Note Added: 0006488
2017-12-17 21:02 yakobowski Assigned To yakobowski => maroneze
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker