2021-01-24 22:30 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000745Frama-CKernel > ACSL implementationpublic2014-03-25 14:17
Reportersignoles 
Assigned Tovirgile 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002051

yakobowski (manager)

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)

You're not missing anything.

~0003467

signoles (manager)

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

-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
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
2014-03-25 14:17 signoles Source_changeset_attached => e-acsl stable/neon 6a33844f
+Issue History