"pointer comparison" warning emitted for "p==NULL"
ID0002256: This issue was created automatically from Mantis Issue 2256. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002256 | Frama-C | Plug-in > Eva | public | 2016-11-11 | 2017-12-17 |
| Reporter | Jochen | Assigned To | maroneze | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | xubuntu | OS Version | - |
| Product Version | Frama-C Aluminium | Target Version | Frama-C 15-Phosphorus | Fixed in Version | - |
Description :
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
- the type of parameter "name" is changed from "char*" to "char" both in "foo" and in "main", or
- 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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information