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.
|ID0002078||Frama-C||Plug-in > wp||public||2015-02-16||2016-01-26|
|Reporter||virgile||Assigned To||correnson||Resolution||no change required|
|Product Version||Frama-C GIT, precise the release id||Target Version||-||Fixed in Version||Frama-C Magnesium|
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)