Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000745Frama-CKernel > ACSL implementationpublic2011-03-04 17:222014-03-25 14:17
Reportersignoles 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000745: Very big integer constants
DescriptionInteger constants are de facto limited to int64 by Cil. Should use Big_int to accept any constant.
Steps To Reproducevoid main(void) {
  /*@ assert 0xfffffffffffffffff == 0xfffffffffffffffff; */
}

$ frama-c a.c
a.c:1:[kernel] failure: Cannot represent on 64 bits the integer 0xfffffffffffffffff
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002051)
yakobowski (manager)
2011-07-25 22:29

I'm a bit lost concerning this issue. We have introduced support for long integers in the AST, but this bug is still not closed. Integers within ACSL terms require an ikind, which limit them to C representable integers. Do we need another constructor for overly long integers, or am I missing something?
(0002054)
monate (reporter)
2011-07-26 11:30

You're not missing anything.
(0003467)
signoles (manager)
2012-09-13 15:15

Fixed by commit r19874 (see its message ;-)).

- Issue History
Date Modified Username Field Change
2011-03-04 17:22 signoles New Issue
2011-03-04 17:22 signoles Status new => assigned
2011-03-04 17:22 signoles Assigned To => virgile
2011-03-04 17:23 svn Checkin
2011-07-25 22:29 yakobowski Note Added: 0002051
2011-07-26 11:30 monate Note Added: 0002054
2012-09-13 15:14 signoles Status assigned => resolved
2012-09-13 15:14 signoles Resolution open => fixed
2012-09-13 15:15 signoles Note Added: 0003467
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