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
ReporterJochen 
Assigned Toyakobowski 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
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<p) in line 11; similar for (NULL<=p) in line 21.

Astree warns "ALARM(C): comparing pointers on different memory blocks {NULL} and {a}" in this case.

Gcc doesn't warn at all; it generates the same code for (NULL<p) in line 11 as for (NULL!=p) in line 16, and translates (NULL<=p) in line 21 as (true); i.e. gcc tacitly assumes that pointer adresses are not negative. The hex constants in the printf-s serve to recognize the branches in the translated machine code program.

The C99 standard (http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1539.pdf [^]) seems to say in sect.5 that (NULL<p) is undefined. Therefor, any behavior of the value-analysis plugin is admissible.

However, when pointers are compared (p<q), the programmer usually intends both p and q to be non-null. If in fact one of them may be null, this is probably a bug . Value-analysis could help to find such bugs.
TagsNo tags attached.
Attached Filesc file icon memory_framac.c [^] (464 bytes) 2011-06-29 14:41 [Show Content]

- Relationships

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

See also http://blog.frama-c.com/index.php?post/2011/06/04/Valid-compare-pointers [^]
(0002002)
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<p) comparison would have helped me to detect my bug.
In my opinion, it is good programming style to use (<) or (<=) only on non-null pointers; this conforms to the C99 standard. If the case p==NULL is to be included, this can be done explicitly by (p==NULL||p<q), which is more understandable than (p<q). Note that the case q==NULL has to be written explicitly, anyway.
The compiler should optimize (p==NULL||p<q) to (p<q); however, gcc-4.1.2 doesn't do this yet.

By the way: NULL being represented as 0x0 is neither necessary nor sufficient for (\forall void *p;NULL<=p) to hold. You need in addition that pointer comparison is implemented by unsigned comparison to make it sufficient. Another (unusual) sufficient combination is e.g.: NULL as 0x80000000, and pointer comparison implemented by signed 32-bit comparison.
(0002003)
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).
(0006089)
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 - 2018 MantisBT Team
Powered by Mantis Bugtracker