Frama-C Bug Tracking System - Frama-C
View Issue Details
0002256Frama-CPlug-in > Evapublic2016-11-11 14:232017-12-17 21:03
Jochen 
maroneze 
normalminoralways
assignedopen 
xubuntu
Frama-C Aluminium 
Frama-C 15-Phosphorus 
0002256: "pointer comparison" warning emitted for "p==NULL"
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.
No tags attached.
c ptrcmp3.c (178) 2016-11-11 14:23
https://bts.frama-c.com/file_download.php?file_id=1125&type=bug
Issue History
2016-11-11 14:23JochenNew Issue
2016-11-11 14:23JochenStatusnew => assigned
2016-11-11 14:23JochenAssigned To => yakobowski
2016-11-11 14:23JochenFile Added: ptrcmp3.c
2017-03-06 11:15yakobowskiNote Added: 0006372
2017-03-06 11:35yakobowskiTarget Version => Frama-C 15-Phosphorus
2017-12-17 21:02yakobowskiNote Added: 0006488
2017-12-17 21:02yakobowskiAssigned Toyakobowski => maroneze
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0006372)
yakobowski   
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.
(0006488)
yakobowski   
2017-12-17 21:02   
Still not done in Sulfur.