Skip to content

Very big integer constants

ID0000745: This issue was created automatically from Mantis Issue 745. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000745 Frama-C Kernel > ACSL implementation public 2011-03-04 2014-03-25
Reporter signoles Assigned To virgile Resolution fixed
Priority low Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version - Target Version - Fixed in Version Frama-C Oxygen-20120901

Description :

Integer constants are de facto limited to int64 by Cil. Should use Big_int to accept any constant.

Steps To Reproduce :

void main(void) { /*@ assert 0xfffffffffffffffff == 0xfffffffffffffffff; */ }

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information