2020-12-05 00:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002394Frama-CPlug-in > wppublic2020-02-17 18:08
Reportertimourf 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSGNU/LinuxOS VersionDebian 9
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in VersionFrama-C 20-Calcium 
Summary0002394: conditional input annotations result in why3 type errors
DescriptionI 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).
Steps To Reproducesee attached file "buggy.c"
run:
> frama-c -wp -wp-prover "why3:XXX" buggy.c
where XXX is any prover installed with why3
Additional Informationwhy3 0.88.3
frama-c chlorine 20180502
TagsNo tags attached.
Attached Files
  • c file icon buggy.c (320 bytes) 2018-08-23 14:12 -
    /*@ requires 0 <= t <= 1;
      @ ensures t == 1.f ==> \result == b;
      @ ensures t == 0.f ==> \result == a;
      @ ensures \min(a,b) <= \result <= \max(a,b);
      @ assigns \nothing;
     */
    float interpolate(float a, float b, float t) {
        float t2 = 1.0f - t;
        float left = a*t2;
        float right = b*t;
        return left+right;
    }
    
    c file icon buggy.c (320 bytes) 2018-08-23 14:12 +

-Relationships
+Relationships

-Notes

~0006950

signoles (manager)

Fixed in Frama-C 20.0 (Calcium).
+Notes

-Issue History
Date Modified Username Field Change
2018-08-23 14:12 timourf New Issue
2018-08-23 14:12 timourf Status new => assigned
2018-08-23 14:12 timourf Assigned To => correnson
2018-08-23 14:12 timourf File Added: buggy.c
2019-10-17 17:05 correnson Status assigned => resolved
2019-10-17 17:05 correnson Fixed in Version => Frama-C 20-Calcium
2019-10-17 17:05 correnson Resolution open => fixed
2020-02-17 18:08 signoles Status resolved => closed
2020-02-17 18:08 signoles Note Added: 0006950
+Issue History