Frama-C Bug Tracking System - Frama-C
View Issue Details
0000945Frama-CPlug-in > Evapublic2011-09-01 19:592017-12-17 21:39
pascal 
maroneze 
lowminorhave not tried
assignedopen 
Frama-C Carbon-20110201 
 
0000945: Should warn for overlapping lv=lv; assignments
Frama-C should warn for this program: struct S { int x; int y; }; struct T { int z; struct S s; }; union U { struct S f ; struct T g; } u; main(){ u.f = u.g.s; return 0; } 6.5.16.1 3: If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined.
No tags attached.
Issue History
2011-09-01 19:59pascalNew Issue
2011-09-03 22:09pascalAssigned To => pascal
2011-09-03 22:09pascalStatusnew => confirmed
2011-09-03 22:09pascalCategoryKernel => Plug-in > value analysis
2011-10-10 15:11pascalNote Added: 0002389
2016-07-05 18:08yakobowskiNote Added: 0006232
2016-07-05 18:08yakobowskiAssigned Topascal => maroneze
2016-07-05 18:08yakobowskiStatusconfirmed => assigned
2017-01-12 14:43yakobowskiNote Added: 0006331
2018-01-12 14:26signolesCategoryPlug-in > value analysis => Plug-in > Eva

Notes
(0002389)
pascal   
2011-10-10 15:11   
Partially fixed in Nitrogen (alarm emitted when the lvalues are known precisely enough).
(0006232)
yakobowski   
2016-07-05 18:08   
Compatibility of types is never tested, but then effectives types are mostly ignored by Value everywhere. The current detection is done only when the lvalue is "larger enough" (strictly larger than an int). The effect of relaxing this condition must be evaluated.
(0006331)
yakobowski   
2017-01-12 14:43   
Two updates from a PhD student currently very busy writing slides (or not): - the case where both locations are imprecise (=intervals) is not handled at all - due to changes in EVA (option -val-warn-copy-indeterminate), this alarm is no longer emitted most of the time.