Commit 4eec40e4 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix sort of floats

parent 9d602ef4
......@@ -165,8 +165,8 @@ let ext_compare a b = Datatype.Int.compare a.ext_id b.ext_id
let sort_of_object = function
| C_int _ -> Logic.Sint
| C_float _ -> Logic.Sreal
| C_pointer _ | C_comp _ | C_array _ -> Logic.Sdata
| C_float f -> Qed.Kind.of_tau (Context.get floats f)
let init_sort_of_object = function
| C_int _ | C_float _ | C_pointer _ -> Logic.Sbool
......
......@@ -8,9 +8,9 @@
------------------------------------------------------------
Goal Post-condition (file tests/wp_bts/issue_898.i, line 8) in 'job':
Let r = job_0.F1_S_value.
Assume { (* Pre-condition *) Have: is_finite_f64(r). }
Prove: eq_f64(r, r).
Let a = job_0.F1_S_value.
Assume { (* Pre-condition *) Have: is_finite_f64(a). }
Prove: eq_f64(a, a).
------------------------------------------------------------
......
......@@ -4,13 +4,12 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Failed
[Why3 Error] Type mismatch between ieee_float.Float64.t and real
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] [Qed] Goal typed_job_assigns : Valid
[wp] Proved goals: 1 / 2
[wp] Proved goals: 2 / 2
Qed: 1
Alt-Ergo: 0 (failed: 1)
Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 1 - 2 50.0%
job 1 1 2 100%
------------------------------------------------------------
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment