0000744: Too much type promotion for terms - 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

0000744

Frama-C

Kernel > ACSL implementation

public

2011-03-04 16:58

2014-03-25 14:17

Reporter

signoles

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000744: Too much type promotion for terms

Description

on the above example, C typing rules should apply. Thus no logic term should be logic integer. Unfortunately, in the current implementation, all of them are integer.

void main(void) {
  int x = 0, y = 0;
  long z = 0L;
  /*@ assert x == y; */ // x and y are promoted to integer; should be promoted to int instead
  /*@ assert x == z; */ // x and z are promoted to integer. x should be promoted to long instead
}

Tags

No tags attached.

Relationships

Notes
(0001557) virgile (developer) 2011-03-08 10:33	Agreed for the comparison between x and y as they are both int. For the comparison between x and z, they have distinct type and are both promoted to integer. The user still can cast x to long if ey want to do the comparison at this level.

(0001561) signoles (manager) 2011-03-08 11:08	In the same way, in the example below "x" is promoted to integer bug not "(int)z". Quite strange. /@ assert x == (int) z; /

(0004824) 2014-02-12 16:59	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2011-03-04 16:58	signoles	New Issue
2011-03-04 16:58	signoles	Status	new => assigned
2011-03-04 16:58	signoles	Assigned To	=> virgile
2011-03-04 17:09	svn	Checkin
2011-03-08 10:12	signoles	Description Updated
2011-03-08 10:33	virgile	Note Added: 0001557
2011-03-08 10:34	virgile	Status	assigned => acknowledged
2011-03-08 11:08	signoles	Note Added: 0001561
2011-03-08 11:14	svn	Checkin
2011-03-08 11:28	svn	Checkin
2011-03-10 16:39	svn	Checkin
2011-03-10 16:39	svn	Status	acknowledged => resolved
2011-03-10 16:39	svn	Resolution	open => fixed
2011-10-10 14:13	signoles	Fixed in Version	=> Frama-C Nitrogen-20111001
2011-10-10 14:14	signoles	Status	resolved => closed
2014-02-12 16:59		Note Added: 0004824
2014-02-12 16:59		Status	closed => resolved

Copyright © 2000 - 2017 MantisBT Team