|Anonymous | Login | Signup for a new account||2019-05-21 16:12 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002256||Frama-C||Plug-in > Eva||public||2016-11-11 14:23||2017-12-17 21:03|
|Product Version||Frama-C Aluminium|
|Target Version||Frama-C 15-Phosphorus||Fixed in Version|
|Summary||0002256: "pointer comparison" warning emitted for "p==NULL"|
|Description||Running "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.
|Tags||No tags attached.|
|Attached Files||ptrcmp3.c [^] (178 bytes) 2016-11-11 14:23 [Show Content]|
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.
|Still not done in Sulfur.|
|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|