Frama-C Bug Tracking System - Frama-C
View Issue Details
0000875Frama-CPlug-in > Evapublic2011-06-29 14:412016-01-26 08:43
Jochen 
yakobowski 
normalfeaturealways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Magnesium 
0000875: suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null
In the attached program, Frama-C could issue a warning for the comparison (NULL
No tags attached.
c memory_framac.c (464) 2011-06-29 14:41
https://bts.frama-c.com/file_download.php?file_id=237&type=bug
Issue History
2011-06-29 14:41JochenNew Issue
2011-06-29 14:41JochenStatusnew => assigned
2011-06-29 14:41JochenAssigned To => pascal
2011-06-29 14:41JochenFile Added: memory_framac.c
2011-06-29 18:49pascalRelationship addedrelated to 0000855
2011-06-29 19:08pascalNote Added: 0002000
2011-06-29 19:08pascalStatusassigned => feedback
2011-06-29 19:10pascalNote Added: 0002001
2011-07-01 16:50JochenNote Added: 0002002
2011-07-01 23:11pascalNote Added: 0002003
2015-10-23 15:17yakobowskiAssigned Topascal => yakobowski
2015-10-23 15:17yakobowskiStatusfeedback => assigned
2015-10-23 15:17yakobowskiNote Added: 0006089
2015-10-23 15:17yakobowskiStatusassigned => resolved
2015-10-23 15:17yakobowskiFixed in Version => Frama-C Magnesium
2015-10-23 15:17yakobowskiResolutionopen => fixed
2016-01-26 08:43signolesStatusresolved => closed
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002000)
pascal   
2011-06-29 19:08   
"not warning about < comparison of a valid pointer to NULL" is a feature wish that goes in the same category as "not assuming that NULL type-puned to an integer is zero". It doesn't really make sense to make one hypothesis and avoid the other, because they are on the same level. They are also related in that these assumptions are made because of the same practical representation of addresses. Unfortunately, it would be very hard not to assume that NULL is not zero. because that assumption goes deep inside the analysis' abstract representations. QuickLZ needs these assumptions to be verified (note, by the way, that is it very hard to explain to programmers why < between pointers is dangerous at all, even when it is dangerous for reasons other than one pointer is NULL and the other is valid). Did you encounter program(s) where you would have liked to see the warning for comparing with < NULL to a valid address?
(0002001)
pascal   
2011-06-29 19:10   
See also http://blog.frama-c.com/index.php?post/2011/06/04/Valid-compare-pointers
(0002002)
Jochen   
2011-07-01 16:50   
The kind of program I have in mind is like the following. void reportPathKind(const char *path) { const char * const p = strchr(path,'/'); if (p != NULL) { const char * const q = strchr(path,'.'); if (q < p) printf("A '.' occurs in the directory prefix\n"); // FIXME: or no '.' occurs at all, if q==NULL else printf("A '.' occurs only in the final file name\n"); } else { printf("Only a file name was given\n"); } } Here, I had forgotten to catch the case q==NULL explicitly. A warning about the (q
(0002003)
pascal   
2011-07-01 23:11   
- CIL inserts casts to unsigned int when pointers are compared as part of its normalization. A plugin can always ignore them, but if casts to unsigned int were part if the original program, making it unsafe, the plugin will then fail to warn about it. The last time I heard, this was still true and Jessie for instance contained cases for ignoring these casts. - the argument "the value analysis could find a functional bug in program X if it warned about Y" is not always receivable: I need to write a blog post about this. The title will be "Frama-C's value analysis is not Lint". The value analysis' goals do not include finding functional bugs based on the shape of the code. It will for instance never warn about i-i where i is an integer variable, because although this expression is always 0 and could indicate a typo, it is also always well defined. If the programmer wants to compute i-i, who are we to judge? Similarly, perhaps his pointer comparison was designed to take NULL into account (assuming it to compare lower to valid pointers). - this said, since pointer comparisons are being revamped for the next release, I can see if many of the alarms being emited would be false alarms (QuickLZ will count as one false alarm).
(0006089)
yakobowski   
2015-10-23 15:17   
This will be flagged as an alarm in Magnesium.