Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000376Frama-CPlug-in > jessiepublic2010-01-19 17:142010-04-13 15:33
ReporterMikhail Pritula 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090902 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000376: unsigned long long constant becomes signed
DescriptionI have newest why and jessie and simple sample .c file: /*@ ensures \result == 1; @ */ int always_one(unsigned long long a) { if (a <= 0xFFFFFFFFFFFFFFFFull) return 1; return 0; } I run following command line: $ frama-c -jessie -jessie-atp simplify ull_constant.c which produces incorrect lemmas because this big constant becomes -1
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000663)
cmarche (developer)
2010-02-03 14:14

 Fixed in Frama-C kernel (cil/src/cil.ml, function parseInt): integer constants (constructor CInt64) now keep their original string representation

- Issue History
Date Modified Username Field Change
2010-01-19 17:14 Mikhail Pritula New Issue
2010-01-19 17:14 Mikhail Pritula Status new => assigned
2010-01-19 17:14 Mikhail Pritula Assigned To => cmarche
2010-02-03 14:14 cmarche Note Added: 0000663
2010-02-03 14:14 cmarche Status assigned => resolved
2010-02-03 14:14 cmarche Resolution open => fixed
2010-04-13 15:30 signoles Status resolved => new
2010-04-13 15:31 signoles Status new => closed
2010-04-13 15:33 signoles Fixed in Version => Frama-C Boron

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker