From 2638a022276c932ed00dc3f64b0e58bc0114a3d7 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 20 Mar 2019 12:55:03 +0100
Subject: la division flottante fonctionne

---
 runtime/mppa_k1c/Makefile   |  3 ++-
 runtime/mppa_k1c/i64_sdiv.c | 10 ++++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'runtime')

diff --git a/runtime/mppa_k1c/Makefile b/runtime/mppa_k1c/Makefile
index 9f2ba980..4e47f567 100644
--- a/runtime/mppa_k1c/Makefile
+++ b/runtime/mppa_k1c/Makefile
@@ -11,4 +11,5 @@ all: $(SFILES)
 .SECONDARY:
 %.s: %.c $(CCOMPPATH)
 	$(CCOMP) $(CFLAGS) -S $< -o $@
-	sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' $@
+	sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' \
+               -e 's/f64_/__compcert_f64_/g' -e 's/f32_/__compcert_f32_/g' $@
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index e312f6e8..0b281d3e 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -40,4 +40,14 @@ int i32_sdiv (int a, int b)
 {
   return __divdi3 (a, b);
 }
+
+extern double __divdf3(double, double);
+double f64_div(double a, double b) {
+  return __divdf3(a, b);
+}
+
+extern float __divsf3(float, float);
+float f32_div(float a, float b) {
+  return __divsf3(a, b);
+}
 #endif
-- 
cgit