Frama-C (Value plug-in) generates nonsensical \pointer_comparable for non-pointer struct field
ID0002206: This issue was created automatically from Mantis Issue 2206. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002206 | Frama-C | Plug-in > Eva | public | 2016-02-03 | 2016-06-21 |
| Reporter | jochenam | Assigned To | yakobowski | Resolution | no change required |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | x86_64 | OS | Linux Mint | OS Version | 17.3 |
| Product Version | Frama-C Aluminium | Target Version | - | Fixed in Version | Frama-C Aluminium |
Description :
When a struct field of type int or similar (not a pointer) is compared to an int, Frama-C (seems to be the Value plug-in) generates a \pointer_comparable assertion. This effect only occurs when the field is accessed via a pointer to the struct obtained from a function whose body is not visible to Frama-C.
Steps To Reproduce :
With the attached main.c, run frama-c -val main.c
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information