Frama-C Bug Tracking System - Frama-C
View Issue Details
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

Notes
(0002051)
yakobowski   
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   
2011-07-26 11:30   
You're not missing anything.
(0003467)
signoles   
2012-09-13 15:15   
Fixed by commit r19874 (see its message ;-)).

Issue History
2011-03-04 17:22signolesNew Issue
2011-03-04 17:22signolesStatusnew => assigned
2011-03-04 17:22signolesAssigned To => virgile
2011-03-04 17:23svn
2011-07-25 22:29yakobowskiNote Added: 0002051
2011-07-26 11:30monateNote Added: 0002054
2012-09-13 15:14signolesStatusassigned => resolved
2012-09-13 15:14signolesResolutionopen => fixed
2012-09-13 15:15signolesNote Added: 0003467
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-03-25 14:17signolesSource_changeset_attached => e-acsl stable/neon 6a33844f