ID0000875: **This issue was created automatically from Mantis Issue 875. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0000875 | Frama-C | Plug-in > Eva | public | 2011-06-29 | 2016-01-26 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed | | **Priority** | normal | **Severity** | feature | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium | ### Description : In 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. ## Attachments - [memory_framac.c](/uploads/f7afdc1411ad0657ad58e63f9ea192cd/memory_framac.c)