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) ## Attachments - [foo.c](/uploads/ff75a74dfb2d281e05cd41c69a1d20d5/foo.c)