use of void* leads to type error in the PO generation
ID0002078: This issue was created automatically from Mantis Issue 2078. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002078 | Frama-C | Plug-in > wp | public | 2015-02-16 | 2016-01-26 |
| Reporter | virgile | Assigned To | correnson | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Magnesium |
Description :
In the attached file, a function ptr is returning a void* value. This function is used to obtain pointers to int in various contexts (there was initially a difference between them, see issue 1945). WP does not generate any proof obligation, and outputs a warning saying
Cast with incompatible pointers types (source: sint8*) (target: sint32*)
I guess the problem is that void* gets converted to char* somehow (changing machine.sizeof_void for the current architecture does not modify the error message)