floating-point support is somwhat incomplete
ID0002459: This issue was created automatically from Mantis Issue 2459. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002459 | Frama-C | Plug-in > wp | public | 2019-07-02 | 2019-10-17 |
| Reporter | florian | Assigned To | correnson | Resolution | suspended |
| Priority | normal | Severity | block | Reproducibility | always |
| Platform | any | OS | any | OS Version | any |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
Hi!
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)...