Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002394Frama-CPlug-in > wppublic2018-08-23 14:122018-08-23 14:12
Assigned Tocorrenson 
Platformx86_64OSGNU/LinuxOS VersionDebian 9
Product VersionFrama-C 17-Chlorine 
Target VersionFixed in Version 
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"
> 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 Filesc file icon buggy.c [^] (320 bytes) 2018-08-23 14:12 [Show Content]

- Relationships

-  Notes
There are no notes attached to this issue.

- 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

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker