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
Reportervirgile 
Assigned Tocorrenson 
PrioritynormalSeverityminorReproducibilityalways
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
(0005959)
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.
(0005960)
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 - 2017 MantisBT Team
Powered by Mantis Bugtracker