Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000875Frama-CPlug-in > Evapublic2011-06-29 14:412016-01-26 08:43
Assigned Toyakobowski 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0000875: suggest to issue a warning on (<)-comparisons between pointers, unless both are non-null
DescriptionIn the attached program, Frama-C could issue a warning for the comparison (NULL
TagsNo tags attached.
Attached Filesc file icon memory_framac.c [^] (464 bytes) 2011-06-29 14:41 [Show Content]

- Relationships

-  Notes
pascal (reporter)
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?
pascal (reporter)
2011-06-29 19:10

See also
Jochen (reporter)
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
pascal (reporter)
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).
yakobowski (manager)
2015-10-23 15:17

This will be flagged as an alarm in Magnesium.

- Issue History
Date Modified Username Field Change
2011-06-29 14:41 Jochen New Issue
2011-06-29 14:41 Jochen Status new => assigned
2011-06-29 14:41 Jochen Assigned To => pascal
2011-06-29 14:41 Jochen File Added: memory_framac.c
2011-06-29 18:49 pascal Relationship added related to 0000855
2011-06-29 19:08 pascal Note Added: 0002000
2011-06-29 19:08 pascal Status assigned => feedback
2011-06-29 19:10 pascal Note Added: 0002001
2011-07-01 16:50 Jochen Note Added: 0002002
2011-07-01 23:11 pascal Note Added: 0002003
2015-10-23 15:17 yakobowski Assigned To pascal => yakobowski
2015-10-23 15:17 yakobowski Status feedback => assigned
2015-10-23 15:17 yakobowski Note Added: 0006089
2015-10-23 15:17 yakobowski Status assigned => resolved
2015-10-23 15:17 yakobowski Fixed in Version => Frama-C Magnesium
2015-10-23 15:17 yakobowski Resolution open => fixed
2016-01-26 08:43 signoles Status resolved => closed
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker