Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002078Frama-CPlug-in > wppublic2015-02-16 14:502016-01-26 08:52
Assigned Tocorrenson 
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002078: use of void* leads to type error in the PO generation
DescriptionIn 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)
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (366 bytes) 2015-02-16 17:58 [Show Content]

- Relationships

-  Notes
correnson (manager)
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.
correnson (manager)
2015-06-29 17:15

Use -wp-model and check for dynamic type with another plug-in.

- Issue History
Date Modified Username Field Change
2015-02-16 14:50 virgile New Issue
2015-02-16 14:50 virgile Status new => assigned
2015-02-16 14:50 virgile Assigned To => correnson
2015-02-16 14:51 virgile Relationship added child of 0001945
2015-02-16 17:58 virgile File Added: foo.c
2015-04-15 18:41 virgile Relationship added child of 0001743
2015-06-29 17:15 correnson Note Added: 0005959
2015-06-29 17:15 correnson Note Added: 0005960
2015-06-29 17:15 correnson Status assigned => resolved
2015-06-29 17:15 correnson Resolution open => no change required
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker