From 2638a022276c932ed00dc3f64b0e58bc0114a3d7 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 20 Mar 2019 12:55:03 +0100 Subject: la division flottante fonctionne --- backend/SelectDiv.vp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/SelectDiv.vp') diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 662162e8..7241d028 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -316,25 +316,25 @@ Definition modls (e1 e2: expr) := Definition divfimm (e: expr) (n: float) := match Float.exact_inverse n with | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil) - | None => divfbase e (Eop (Ofloatconst n) Enil) + | None => divf_base e (Eop (Ofloatconst n) Enil) end. Nondetfunction divf (e1: expr) (e2: expr) := match e2 with | Eop (Ofloatconst n2) Enil => divfimm e1 n2 - | _ => divfbase e1 e2 + | _ => divf_base e1 e2 end. Definition divfsimm (e: expr) (n: float32) := match Float32.exact_inverse n with | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil) - | None => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil) + | None => divfs_base e (Eop (Osingleconst n) Enil) end. Nondetfunction divfs (e1: expr) (e2: expr) := match e2 with | Eop (Osingleconst n2) Enil => divfsimm e1 n2 - | _ => Eop Odivfs (e1 ::: e2 ::: Enil) + | _ => divfs_base e1 e2 end. End SELECT. \ No newline at end of file -- cgit