0000745: Very big integer constants - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000745

Frama-C

Kernel > ACSL implementation

public

2011-03-04 17:22

2014-03-25 14:17

Reporter

signoles

Assigned To

virgile

Priority

low

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000745: Very big integer constants

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

Tags

No tags attached.

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 - 2020 MantisBT Team