diff options
| -rw-r--r-- | Makefile | 6 | ||||
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | test/matrix.c | 23 |
3 files changed, 27 insertions, 4 deletions
@@ -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 new file mode 100644 index 0000000..d612734 --- /dev/null +++ b/test/matrix.c @@ -0,0 +1,23 @@ +#define N 4 + +void matrix_multiply(int first[][N], int second[][N], int multiply[][N]) { + int sum = 0; + 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; + sum = 0; + } + } +} + +int main() { + 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); + return m[1][1]; +} |