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-07-02 11:40
Reporterflorian 
Assigned Tocorrenson 
PrioritynormalSeverityblockReproducibilityalways
StatusassignedResolutionopen 
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 https://gitlab.inria.fr/why3/why3/blob/master/stdlib/ieee_float.mlw [^] 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
(0006806)
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.


- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker