From 3718f2f520fc9a4dec2e9c1ac6eaf71f36f4f8a1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 20 Mar 2019 12:25:02 +0100
Subject: begin float division

---
 backend/SelectDiv.vp | 6 +++---
 mppa_k1c/SelectOp.vp | 4 ++++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index 6ddcd6ac..662162e8 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -309,20 +309,20 @@ Definition modls (e1 e2: expr) :=
       end
   | _, _ => modls_base e1 e2
   end.
-
+  
 (** Floating-point division by a constant can also be turned into a FP
     multiplication by the inverse constant, but only for powers of 2. *)
 
 Definition divfimm (e: expr) (n: float) :=
   match Float.exact_inverse n with
   | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil)
-  | None    => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil)
+  | None    => divfbase e (Eop (Ofloatconst n) Enil)
   end.
 
 Nondetfunction divf (e1: expr) (e2: expr) :=
   match e2 with
   | Eop (Ofloatconst n2) Enil => divfimm e1 n2
-  | _ => Eop Odivf (e1 ::: e2 ::: Enil)
+  | _ => divfbase e1 e2
   end.
 
 Definition divfsimm (e: expr) (n: float32) :=
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index b2ce1fef..80eb641c 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -535,4 +535,8 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
+(* float division *)
+
+Definition divfbase (e1: expr) (e2: expr) :=
+  Eop Odivf (e1 ::: e2 ::: Enil).
 End SELECT.
-- 
cgit