Frama-C Bug Tracking System

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 - 2018 MantisBT Team
Powered by Mantis Bugtracker