Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001001Frama-CPlug-in > value analysispublic2011-10-27 12:542012-09-19 17:16
Reporteryakobowski 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001001: Invalid handling of shift of pointer address
DescriptionThe behavior of the value analysis is incorrect on the following example, which is valid according to the norm.

char t[10];

int main () {
  int r = (unsigned long)t << 8;
  return r;
}
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002430)
pascal (reporter)
2011-10-27 18:04

Fixed in 15961

- Issue History
Date Modified Username Field Change
2011-10-27 12:54 yakobowski New Issue
2011-10-27 12:54 yakobowski Status new => assigned
2011-10-27 12:54 yakobowski Assigned To => pascal
2011-10-27 18:04 pascal Note Added: 0002430
2011-10-27 18:04 pascal Status assigned => resolved
2011-10-27 18:04 pascal Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker