0000376: unsigned long long constant becomes signed - Frama-C Bug Tracking System

Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

ID

Project

Category

View Status

Date Submitted

Last Update

0000376

Frama-C

Plug-in > jessie

public

2010-01-19 17:14

2010-04-13 15:33

Reporter

Mikhail Pritula

Assigned To

cmarche

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Frama-C Beryllium-20090902

Target Version

Fixed in Version

Frama-C Boron-20100401

Summary

0000376: unsigned long long constant becomes signed

Description

I have newest why and jessie and simple sample .c file:
/*@ ensures \result == 1;
  @ */
int always_one(unsigned long long a) {
    if (a <= 0xFFFFFFFFFFFFFFFFull)
        return 1;
    return 0;
}
I run following command line:
$ frama-c -jessie -jessie-atp simplify ull_constant.c
which produces incorrect lemmas because this big constant becomes -1

Tags

No tags attached.

Relationships

Notes
(0000663) cmarche (developer) 2010-02-03 14:14	Fixed in Frama-C kernel (cil/src/cil.ml, function parseInt): integer constants (constructor CInt64) now keep their original string representation

Issue History
Date Modified	Username	Field	Change
2010-01-19 17:14	Mikhail Pritula	New Issue
2010-01-19 17:14	Mikhail Pritula	Status	new => assigned
2010-01-19 17:14	Mikhail Pritula	Assigned To	=> cmarche
2010-02-03 14:14	cmarche	Note Added: 0000663
2010-02-03 14:14	cmarche	Status	assigned => resolved
2010-02-03 14:14	cmarche	Resolution	open => fixed
2010-04-13 15:30	signoles	Status	resolved => new
2010-04-13 15:31	signoles	Status	new => closed
2010-04-13 15:33	signoles	Fixed in Version	=> Frama-C Boron

Copyright © 2000 - 2019 MantisBT Team