Commit e6f1a2b8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

use checksum to check if transf did something

parent 06660d8b
......@@ -1232,7 +1232,15 @@ let transformation_on_goal g trans_name trans =
(fun subgoals ->
let b =
match subgoals with
| [task] -> task != g.Model.task
| [task] ->
let s1 = task_checksum g.Model.task in
let s2 = task_checksum task in
(*
eprintf "Transformation returned only one task. sum before = %s, sum after = %s@." (task_checksum g.Model.task) (task_checksum task);
eprintf "addresses: %x %x@." (Obj.magic g.Model.task) (Obj.magic task);
*)
s1 <> s2
(* task != g.Model.task *)
| _ -> true
in
if b then
......
......@@ -431,7 +431,7 @@ and wp_desc env e q = match e.expr_desc with
| Eany c ->
(* TODO: propagate call labels into c.c_post *)
let w = opaque_wp env c.c_effect c.c_post q in
let p = f_label_add (label ~loc:e.expr_loc "call pre") c.c_pre in
let p = f_label_add (label ~loc:e.expr_loc "Pre") c.c_pre in
wp_and p w
and wp_triple env (p, e, q) =
......
......@@ -121,8 +121,9 @@ theory Test
use Single
use Double
lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0
lemma Round_double_01: Double.round NearestTiesToEven 0.1 = 0x0.199999Ap0
lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x1.99999ap-4
lemma Round_double_01: Double.round NearestTiesToEven 0.1 = 0x1.999999999999ap-4
end
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