Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002459Frama-CPlug-in > wppublic2019-07-02 10:292019-10-17 17:57
Assigned Tocorrenson 
PlatformanyOSanyOS Versionany
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002459: floating-point support is somwhat incomplete
DescriptionHi! Maybe I am doing something fundamentally wrong, but I've tried some simple programs and I don't get anywhere. For example: /*@ requires x >= 0.0f && x <= 100.0f; */ void float_fun(float x) { float y = x + 1.0f; //@ assert y >= 1.0f; } I've had a look in share/frama-c/wp/why3/Cfloat.why and I'm not surprised nothing works, the axiomatisation is very incomplete, compared to the current stuff in why3. Could you please port to and then use a SMT solver by default that supports it natively (i.e. CVC4 or Z3)? I know this is a bit of a drastic change, but as it stands WP is not overly useful for anyone trying to do anything with floats (e.g. control systems)...
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
correnson (manager)
2019-07-02 11:39
edited on: 2019-07-02 11:40

This is not a so easy design and, generally speaking, SMT solvers are not very strong when dealing with floats, even CVC4 and Z3. Frama-C/WP was never designed to support float in a short term basis, and we decided to switch from the naive real model to some non-interpreted float model just to preserve soundness and prevent unadvertised users to prove wrong facts about floats with it. Moreover, with Frama-C/WP up to Potassium, we don't necessarily go through Why-3 and we still have tu support native output for Alt-Ergo and Coq, and including a reasonable axiomatics for IEEE floats for them is a challenge. But in the next release of Frama-C/WP, the Why-3 output will be the only one provided and this typically will be enhanced. However, we are still working on different bindings of the float API to SMT libs. If you want to experiment on your own, you can still make use of Frama-C/WP drivers, see documentation ยง 2.4.10 p. 39 Better, you are kindly encouraged to submit a pull request on GitHub with an alternative default WP driver ! Regards, L.
correnson (manager)
2019-10-17 14:32

The float model of Frama-C/WP has evolved in the next (coming soon) Calcium release, thanks to closer integration with why-3.
correnson (manager)
2019-10-17 14:48

Research project
correnson (manager)
2019-10-17 14:53

On the roadmap. Feel free to participate in.

- Issue History
Date Modified Username Field Change
2019-07-02 10:29 florian New Issue
2019-07-02 10:29 florian Status new => assigned
2019-07-02 10:29 florian Assigned To => correnson
2019-07-02 11:39 correnson Note Added: 0006806
2019-07-02 11:40 correnson Note Edited: 0006806 View Revisions
2019-07-02 11:40 correnson Note Edited: 0006806 View Revisions
2019-10-17 14:32 correnson Note Added: 0006884
2019-10-17 14:48 correnson Note Added: 0006886
2019-10-17 14:48 correnson Status assigned => acknowledged
2019-10-17 14:53 correnson Note Added: 0006891
2019-10-17 14:53 correnson Status acknowledged => resolved
2019-10-17 14:53 correnson Resolution open => suspended
2019-10-17 17:57 signoles Status resolved => closed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker