From c6f390beecfbd8d749d06e8d9b86a7754a2239c5 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 12 Jun 2020 18:06:50 +0100
Subject: Add matrix test

---
 test/matrix.c | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test/matrix.c

diff --git a/test/matrix.c b/test/matrix.c
new file mode 100644
index 0000000..2a1a6b7
--- /dev/null
+++ b/test/matrix.c
@@ -0,0 +1,21 @@
+void matrix_multiply(int first[][2], int second[][2], int multiply[][2], int m, int q, int p) {
+    int sum = 0;
+    for (int c = 0; c < m; c++) {
+        for (int d = 0; d < q; d++) {
+            for (int k = 0; k < p; k++) {
+                sum = sum + first[c][k]*second[k][d];
+            }
+            multiply[c][d] = sum;
+            sum = 0;
+        }
+    }
+}
+
+int main() {
+    int f[2][2] = {{1, 2}, {3, 4}};
+    int s[2][2] = {{1, 2}, {3, 4}};
+    int m[2][2] = {{0, 0}, {0, 0}};
+
+    matrix_multiply(f, s, m, 2, 2, 2);
+    return m[1][1];
+}
-- 
cgit 


From 8e3c89bad3a20c0bb9c88b83d966565d79822ff1 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 12 Jun 2020 19:05:34 +0100
Subject: Update matrix and use 32 bit

---
 Makefile      |  6 +++---
 _CoqProject   |  2 +-
 test/matrix.c | 18 ++++++++++--------
 3 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/Makefile b/Makefile
index 42e6a45..0167a78 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,12 @@
 UNAME_S := $(shell uname -s)
 ifeq ($(UNAME_S),Linux)
-	ARCH := x86_64-linux
+	ARCH := x86_32-linux
 endif
 ifeq ($(UNAME_S),Darwin)
-	ARCH := x86_64-macosx
+	ARCH := x86_32-macosx
 endif
 
-COMPCERTRECDIRS := lib common x86_64 x86 backend cfrontend driver flocq exportclight \
+COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
   MenhirLib cparser
 
 COQINCLUDES := -R src/common coqup.common -R src/verilog coqup.verilog \
diff --git a/_CoqProject b/_CoqProject
index 7b2f864..a1026ed 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,4 +14,4 @@
 -R lib/CompCert/flocq compcert.flocq
 -R lib/CompCert/lib compcert.lib
 -R lib/CompCert/x86 compcert.x86
--R lib/CompCert/x86_64 compcert.x86_64
+-R lib/CompCert/x86_32 compcert.x86_64
diff --git a/test/matrix.c b/test/matrix.c
index 2a1a6b7..d612734 100644
--- a/test/matrix.c
+++ b/test/matrix.c
@@ -1,8 +1,10 @@
-void matrix_multiply(int first[][2], int second[][2], int multiply[][2], int m, int q, int p) {
+#define N 4
+
+void matrix_multiply(int first[][N], int second[][N], int multiply[][N]) {
     int sum = 0;
-    for (int c = 0; c < m; c++) {
-        for (int d = 0; d < q; d++) {
-            for (int k = 0; k < p; k++) {
+    for (int c = 0; c < N; c++) {
+        for (int d = 0; d < N; d++) {
+            for (int k = 0; k < N; k++) {
                 sum = sum + first[c][k]*second[k][d];
             }
             multiply[c][d] = sum;
@@ -12,10 +14,10 @@ void matrix_multiply(int first[][2], int second[][2], int multiply[][2], int m,
 }
 
 int main() {
-    int f[2][2] = {{1, 2}, {3, 4}};
-    int s[2][2] = {{1, 2}, {3, 4}};
-    int m[2][2] = {{0, 0}, {0, 0}};
+    int f[N][N] = {{1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}, {1, 2, 3, 4}};
+    int s[N][N] = {{5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}, {5, 6, 7, 8}};
+    int m[N][N] = {{0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}, {0, 0, 0, 0}};
 
-    matrix_multiply(f, s, m, 2, 2, 2);
+    matrix_multiply(f, s, m);
     return m[1][1];
 }
-- 
cgit