Frama-C Bug Tracking System - Frama-C
View Issue Details
0002078Frama-CPlug-in > wppublic2015-02-16 14:502016-01-26 08:52
closedno change required 
Frama-C GIT, precise the release id 
Frama-C Magnesium 
0002078: use of void* leads to type error in the PO generation
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)
No tags attached.
c foo.c (366) 2015-02-16 17:58
Issue History
2015-02-16 14:50virgileNew Issue
2015-02-16 14:50virgileStatusnew => assigned
2015-02-16 14:50virgileAssigned To => correnson
2015-02-16 14:51virgileRelationship addedchild of 0001945
2015-02-16 17:58virgileFile Added: foo.c
2015-04-15 18:41virgileRelationship addedchild of 0001743
2015-06-29 17:15corrensonNote Added: 0005959
2015-06-29 17:15corrensonNote Added: 0005960
2015-06-29 17:15corrensonStatusassigned => resolved
2015-06-29 17:15corrensonResolutionopen => no change required
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed

2015-06-29 17:15   
Need -wp-model cast to accept cast from different pointer types. However, this memory model is unsafe. It is unsound if you change the dynamic type of pointed values.
2015-06-29 17:15   
Use -wp-model and check for dynamic type with another plug-in.