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)...