Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000336Frama-CPlug-in > jessiepublic2009-11-20 16:012010-01-22 19:28
Reporterdpariente 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in Version 
Summary0000336: cast between homogenous struct and array
DescriptionEnsures PO generated by "frama-c -jessie" on this example code can not be discharged: float v; typedef struct {float f0;float f1;float f2;} ts; typedef ts las; /*@ requires \valid_range(d,0,2); assigns v; ensures v == d[1]; */ void f(float d[]) { v = d[1]; } //@ ensures v==9.0; void main() { las x; x.f1 = 9.0; f(&x); } ANSI C allows this "transparent" casting between homogenously typed structure and array. Simulating the cast by means of an additional C function and predicate (with its axiomatization) - a solution previously proposed Frama-C team - works well but entails modifying the source code!
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000649)
dpariente (reporter)
2010-01-22 19:28

The case of struct of struct ... should also be taken into account for "transparent" casting towards array type. Typically, modifying slightly the example above, one could have the following annotated code: float v; typedef struct {float f0;float f1;float f2;} ts2; typedef struct {ts2 f0;ts2 f1;ts2 f2;} ts; typedef ts las; /*@ requires \valid_range(d,0,8); assigns v; ensures v == d[1]; */ void f(float d[]) { v = d[1]; } //@ ensures v==9.0; void main() { las x; x.f0.f1 = 9.0; f(&x); }

- Issue History
Date Modified Username Field Change
2009-11-20 16:01 dpariente New Issue
2009-12-08 16:35 signoles Status new => assigned
2009-12-08 16:35 signoles Assigned To => cmarche
2010-01-22 19:28 dpariente Note Added: 0000649


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker