cast between homogenous struct and array
ID0000336: This issue was created automatically from Mantis Issue 336. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000336 | Frama-C | Plug-in > jessie | public | 2009-11-20 | 2010-01-22 |
| Reporter | dpariente | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090902 | Target Version | - | Fixed in Version | - |
Description :
Ensures 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!