Update lu.c and update Makefile with extraction

2 files changed, 35 insertions, 40 deletions

diff --git a/Makefile b/Makefile
index ee111eb..f8a3328 100644
--- a/Makefile
+++ b/Makefile
@@ -33,7 +33,7 @@ all: lib/COMPCERTSTAMP
 
 lib/COMPCERTSTAMP:
 	(cd lib/CompCert && ./configure --ignore-coq-version $(ARCH))
-	$(MAKE) -C lib/CompCert
+	$(MAKE) extraction -C lib/CompCert
 	touch $@
 
 install:
diff --git a/benchmarks/polybench-syn/linear-algebra/solvers/lu.c b/benchmarks/polybench-syn/linear-algebra/solvers/lu.c
index 56dadd7..d925db8 100644
--- a/benchmarks/polybench-syn/linear-algebra/solvers/lu.c
+++ b/benchmarks/polybench-syn/linear-algebra/solvers/lu.c
@@ -13,27 +13,26 @@
 //#include <unistd.h>
 //#include <string.h>
 //#include <math.h>
+#include <stdio.h>
 
 #include "../../include/misc.h"
 
-#define plus(i) i = i + ONE
+#define plus(n) ((n = n + 1))
 
 static
 void init_array (int n,
-   int A[40][40])
+                 int A[40][40])
 {
-  int ONE = 1;
   int i, j;
 
-  for (i = 0; i < n; plus(i))
-    {
-      for (j = 0; j <= i; plus(j))
- A[i][j] = sdivider(smodulo(-j, n), n) + ONE;
-      for (j = plus(i); j < n; plus(j)) {
- A[i][j] = 0;
-      }
-      A[i][i] = 1;
+  for (i = 0; i < n; i++)  {
+    for (j = 0; j <= i; j++)
+      A[i][j] = (-j % n) / n + 1;
+    for (j = i+1; j < n; j++) {
+      A[i][j] = 0;
     }
+    A[i][i] = 1;
+  }
 
 
 
@@ -45,63 +44,61 @@ void init_array (int n,
   for (t = 0; t < n; plus(t))
     for (r = 0; r < n; plus(r))
       for (s = 0; s < n; plus(s))
- B[r][s] += A[r][t] * A[s][t];
-    for (r = 0; r < n; plus(r))
-      for (s = 0; s < n; plus(s))
- A[r][s] = B[r][s];
+        B[r][s] += A[r][t] * A[s][t];
+  for (r = 0; r < n; plus(r))
+    for (s = 0; s < n; plus(s))
+      A[r][s] = B[r][s];
   //free((void*)B);;
 
 }
 
 
 
-/*
-static
-void print_array(int n,
-   int A[ 40 + 0][40 + 0])
+/*static
+  void print_array(int n,
+  int A[ 40 + 0][40 + 0])
 
-{
+  {
   int i, j;
 
   fprintf(stderr, "==BEGIN DUMP_ARRAYS==\n");
   fprintf(stderr, "begin dump: %s", "A");
   for (i = 0; i < n; i++)
-    for (j = 0; j < n; j++) {
-      if ((i * n + j) % 20 == 0) fprintf (stderr, "\n");
-      fprintf (stderr, "%d ", A[i][j]);
-    }
+  for (j = 0; j < n; j++) {
+  if ((i * n + j) % 20 == 0) fprintf (stderr, "\n");
+  fprintf (stderr, "%d ", A[i][j]);
+  }
   fprintf(stderr, "\nend   dump: %s\n", "A");
   fprintf(stderr, "==END   DUMP_ARRAYS==\n");
-}
+  }
 */
 
 
-
 static
 void kernel_lu(int n,
-        int A[ 40][40])
+               int A[ 40][40])
 {
   int i, j, k;
   int ONE = 1;
 
- for (i = 0; i < n; plus(i)) {
+  for (i = 0; i < n; plus(i)) {
     for (j = 0; j <i; plus(j)) {
-       for (k = 0; k < j; plus(k)) {
-          A[i][j] -= A[i][k] * A[k][j];
-       }
-        A[i][j] = sdivider(A[i][j], A[j][j]);
+      for (k = 0; k < j; plus(k)) {
+        A[i][j] -= A[i][k] * A[k][j];
+      }
+      A[i][j] = A[i][j] / A[j][j];
     }
-   for (j = i; j < n; plus(j)) {
-       for (k = 0; k < i; plus(k)) {
-          A[i][j] -= A[i][k] * A[k][j];
-       }
+    for (j = i; j < n; plus(j)) {
+      for (k = 0; k < i; plus(k)) {
+        A[i][j] -= A[i][k] * A[k][j];
+      }
     }
   }
 }
 
 static
 int check_array(int n,
-   int A[40][40])
+                int A[40][40])
 {
   int res = 0;
   int i, j;
@@ -130,9 +127,7 @@ int main()
 
   kernel_lu (n, A);
 
-
   return check_array(n, A);
-  return 0;
 
   //free((void*)A);;
 }