Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000945Frama-CPlug-in > Evapublic2011-09-01 19:592017-12-17 21:39
Reporterpascal 
Assigned Tomaroneze 
PrioritylowSeverityminorReproducibilityhave not tried
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in Version 
Summary0000945: Should warn for overlapping lv=lv; assignments
DescriptionFrama-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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002389)
pascal (reporter)
2011-10-10 15:11

Partially fixed in Nitrogen (alarm emitted when the lvalues are known precisely enough).
(0006232)
yakobowski (manager)
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 (manager)
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.

- Issue History
Date Modified Username Field Change
2011-09-01 19:59 pascal New Issue
2011-09-03 22:09 pascal Assigned To => pascal
2011-09-03 22:09 pascal Status new => confirmed
2011-09-03 22:09 pascal Category Kernel => Plug-in > value analysis
2011-10-10 15:11 pascal Note Added: 0002389
2016-07-05 18:08 yakobowski Note Added: 0006232
2016-07-05 18:08 yakobowski Assigned To pascal => maroneze
2016-07-05 18:08 yakobowski Status confirmed => assigned
2017-01-12 14:43 yakobowski Note Added: 0006331
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker