0001847: Problem with _Bool(when casting to int or with ?:)

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001847

Frama-C

Plug-in > wp

public

2014-07-21 10:06

Reporter

davyg

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

assigned

Resolution

open

Platform

OS Version

Product Version

Target Version

Fixed in Version

Summary

0001847: Problem with _Bool(when casting to int or with ?:)

Description

In this example the ensures seems to be impossible to prove whereas it should
be easy :

//@ensures (!\result) == (!x);
_Bool f(_Bool x) {
_Bool y;
return (y?x:x);
}

I put the bug in Wp category but it can be see as a framaC bug depending from where it comes from.

Additional Information

This must be due to the transformation of ?: into an if statement
with an int local variable which lead more or less to a function like
this that can't be proven :

//@ensures (!\result) == (!x);
_Bool g(_Bool x) {
int t = x;
return t;
}

This must be due to the lack of information about the cast.

I think that the transformation of ?: should use a _Bool temp
variable instead of an int. Or int cast should have a lemma like \forall _Bool x; (x != 0) <==> (((int) x) != 0);

Issue History
Date Modified	Username	Field	Change
2014-07-21 10:06	davyg	New Issue
2014-07-21 10:06	davyg	Status	new => assigned
2014-07-21 10:06	davyg	Assigned To	=> correnson

Relationships

Notes
There are no notes attached to this issue.