ID0002394: **This issue was created automatically from Mantis Issue 2394. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002394 | Frama-C | Plug-in > wp | public | 2018-08-23 | 2020-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | timourf | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | x86_64 | **OS** | GNU/Linux | **OS Version** | Debian 9 | | **Product Version** | Frama-C 17-Chlorine | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium | ### Description : 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). ### Additional Information : why3 0.88.3 frama-c chlorine 20180502 ### Steps To Reproduce : see attached file "buggy.c" run: > frama-c -wp -wp-prover "why3:XXX" buggy.c where XXX is any prover installed with why3 ## Attachments - [buggy.c](/uploads/323bd028ec39d43d549eae1d88957797/buggy.c)