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:122019-10-17 17:05
Reportertimourf 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusresolvedResolutionfixed 
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 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
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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker