diff --git a/.gitattributes b/.gitattributes index 5cb0f7baf1bc6167712307b9f68d40c9566937e7..85087c8e0fe5c13b5551e69e24c641fd9c5c1ee1 100644 --- a/.gitattributes +++ b/.gitattributes @@ -10,6 +10,9 @@ /bench/encoding/ export-ignore /examples/in_progress/ export-ignore +/examples/multiprecision/random/ export-ignore +/examples/multiprecision/bench-include/ export-ignore +/examples/multiprecision/mini-gmp/ export-ignore /misc/ export-ignore /opam/ export-ignore /tests/ export-ignore diff --git a/drivers/c.drv b/drivers/c.drv index c9b500be064cd614d298955995b543e615d4288e..1c18780597bdb2b060a49660db44ff62f1857e9c 100644 --- a/drivers/c.drv +++ b/drivers/c.drv @@ -252,7 +252,6 @@ module mach.int.UInt64GMP prelude " -#include \"config.h\" #include \"gmp.h\" #include \"gmp-impl.h\" #include \"longlong.h\" @@ -372,7 +371,6 @@ struct __lsld64_result lsld64(uint64_t x, uint64_t cnt) interface " -#include \"config.h\" #include \"gmp.h\" #include \"gmp-impl.h\" #include \"longlong.h\" diff --git a/examples/multiprecision/Makefile b/examples/multiprecision/Makefile index d871770b88f1470beeb64c776cbe3268b6ec38e6..ef9886c894aeeb8cf1719f417f4dbfe848820ddf 100644 --- a/examples/multiprecision/Makefile +++ b/examples/multiprecision/Makefile @@ -29,13 +29,13 @@ extract: why3 dir cfiles CFILES = build/uint64gmp.c build/div.c build/logical.c build/mul.c build/sub.c build/add.c build/compare.c build/util.c build/int32.c tests: extract check-gmp - gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 tests.c $(CFILES) -I$(GMP_DIR) -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o build/tests - gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 -DCOMPARE_MINI tests.c $(CFILES) -I$(GMP_DIR) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o build/minitests + gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 tests.c $(CFILES) -I$(GMP_DIR) -Irandom -L$(GMP_LIB) -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -lgmp -o build/tests + gcc -O2 -Wall -Wno-unused-function -g -std=gnu99 -DCOMPARE_MINI tests.c $(CFILES) -I$(GMP_DIR) -Irandom -Imini-gmp -fomit-frame-pointer -mtune=haswell -march=haswell -fno-tree-vectorize -o build/minitests ./build/tests ./build/minitests bench-tests: extract - gcc -O2 -Wall -g -std=gnu99 tests.c $(CFILES) -Ibench-include -fomit-frame-pointer -fno-tree-vectorize -lgmp -o build/bench-tests + gcc -O2 -Wall -g -std=gnu99 tests.c $(CFILES) -Ibench-include -Irandom -fomit-frame-pointer -fno-tree-vectorize -lgmp -o build/bench-tests build/why3%bench: extract check-gmp diff --git a/examples/multiprecision/mini-gmp.c b/examples/multiprecision/mini-gmp/mini-gmp.c similarity index 100% rename from examples/multiprecision/mini-gmp.c rename to examples/multiprecision/mini-gmp/mini-gmp.c diff --git a/examples/multiprecision/mini-gmp.h b/examples/multiprecision/mini-gmp/mini-gmp.h similarity index 100% rename from examples/multiprecision/mini-gmp.h rename to examples/multiprecision/mini-gmp/mini-gmp.h diff --git a/examples/multiprecision/mt19937-64.c b/examples/multiprecision/random/mt19937-64.c similarity index 100% rename from examples/multiprecision/mt19937-64.c rename to examples/multiprecision/random/mt19937-64.c