4 files changed, 24 insertions, 26 deletions
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 8e00dc99..3529a36f 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -180,4 +180,4 @@ Proof.
   { apply Z_div_pos; omega. }
   pose proof modulus_fits_64.
   omega.
-Qed.
-\ No newline at end of file
+Qed.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 6adcebe5..c4b01d89 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -423,7 +423,11 @@ Definition mods_base (e1: expr) (e2: expr) :=
   Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).
 
 Definition divu_base (e1: expr) (e2: expr) :=
-  Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
+  Eop Olowlong
+     ((Eexternal i64_udiv sig_ll_l
+       ((Eop Ocast32unsigned (e1 ::: Enil)):::
+       (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
+      :::Enil).
   
 Definition modu_base (e1: expr) (e2: expr) :=
   Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 9e2eec8b..2730ee91 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -872,8 +872,24 @@ Theorem eval_divu_base:
     Val.divu x y = Some z ->
     exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold divu_base.
-  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+  intros until z.
+  intros Hax Hby Hdiv. unfold divu_base.
+  pose proof (divu_is_divlu x y) as DIVU.
+  destruct (Val.divlu (Val.longofintu x) (Val.longofintu y))
+    as [ ql | ] eqn:Ediv.
+  { TrivialExists.
+    { econstructor. eapply eval_helper_2; eauto.
+      { econstructor. econstructor. eassumption.
+       constructor. simpl. reflexivity. }
+      { econstructor. econstructor. eassumption.
+        constructor. simpl. reflexivity. }
+      { DeclHelper. }
+      { UseHelper. }
+      constructor. }
+    simpl.
+    congruence.
+  }
+  congruence.
 Qed.
 
 Theorem eval_modu_base:
diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/mppa_k1c/i64_udiv.c
index ce14464d..e69de29b 100644
--- a/runtime/mppa_k1c/i64_udiv.c
+++ b/runtime/mppa_k1c/i64_udiv.c
@@ -1,22 +0,0 @@
-#ifdef COMPLIQUE
-unsigned long long
-udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
-
-unsigned long long i64_udiv (unsigned long long a, unsigned long long b)
-{
-  return udivmoddi4 (a, b, 0);
-}
-
-#else
-extern long __udivdi3 (long a, long b);
-
-unsigned long i64_udiv (unsigned long a, unsigned long b)
-{
-  return __udivdi3 (a, b);
-}
-
-unsigned int i32_udiv (unsigned int a, unsigned int b)
-{
-  return __udivdi3 (a, b);
-}
-#endif