0000751: Promotion from integer to boolean - 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

0000751

Frama-C

Kernel > ACSL implementation

public

2011-03-11 09:54

2014-02-12 16:59

Reporter

signoles

Assigned To

virgile

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Nitrogen-20111001

Summary

0000751: Promotion from integer to boolean

Description

At this day, in the predicate or term "0 == !1", 0 is an integer while !1 is a boolean. Both members of the equality should have the same type (boolean). Thus a solution could be that the normalization translates "0 == !1" to "(0 == 0) == (0 == !1)".

Tags

No tags attached.

Relationships

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

Issue History
Date Modified	Username	Field	Change
2011-03-11 09:54	signoles	New Issue
2011-03-11 09:54	signoles	Status	new => assigned
2011-03-11 09:54	signoles	Assigned To	=> virgile
2011-03-11 09:58	virgile	Status	assigned => acknowledged
2011-06-29 18:34	svn	Checkin
2011-06-29 18:34	svn	Status	acknowledged => resolved
2011-06-29 18:34	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: 0004768
2014-02-12 16:59		Status	closed => resolved

Copyright © 2000 - 2017 MantisBT Team