Frama-C Bug Tracking System - Frama-C
View Issue Details
0002394Frama-CPlug-in > wppublic2018-08-23 14:122019-10-17 17:05
timourf 
correnson 
normalmajoralways
resolvedfixed 
x86_64GNU/LinuxDebian 9
Frama-C 17-Chlorine 
Frama-C 20-Calcium 
0002394: conditional input annotations result in why3 type errors
I am trying to put conditions on my function specification that specify return values conditioned on special input values. A minimal example is as follows: /*@ requires 0 <= t <= 1; @ ensures t == 1.f ==> \result == b; @ assigns \nothing */ float interpolate(float a, float b, float t) { ... } Why3 (stderr) reports: =================================================================================== File "/tmp/wp0a3ed9.dir/typed/interpolate_Why3_ide.why", line 20, characters 11-26: This term has type real -> real, but is expected to have type real =================================================================================== The "problem line" is "ensures t == 1.f ==> \result == b;" This seems to be a problem between wp and why3. The error persists with every external prover I use with why3. The list of provers I've tried is [Z3,CVC3,CVC4,Alt-Ergo,Gappa], and the only exception is why3:coq (see issue 0002389).
see attached file "buggy.c" run: > frama-c -wp -wp-prover "why3:XXX" buggy.c where XXX is any prover installed with why3
why3 0.88.3 frama-c chlorine 20180502
No tags attached.
c buggy.c (320) 2018-08-23 14:12
https://bts.frama-c.com/file_download.php?file_id=1282&type=bug
Issue History
2018-08-23 14:12timourfNew Issue
2018-08-23 14:12timourfStatusnew => assigned
2018-08-23 14:12timourfAssigned To => correnson
2018-08-23 14:12timourfFile Added: buggy.c
2019-10-17 17:05corrensonStatusassigned => resolved
2019-10-17 17:05corrensonFixed in Version => Frama-C 20-Calcium
2019-10-17 17:05corrensonResolutionopen => fixed

There are no notes attached to this issue.