diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 22:02:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 22:02:46 +0200 |
| commit | 7299996cac6c4747b6611b17f0af15fb08c6ee80 (patch) | |
| tree | 744b3f37834356ebb13c45097fc4740ffb4d16ea /test/monniaux/minisat/Makefile.profiled | |
| parent | 7d15566ad116730c1452364bc0fe3d2dc714e5ed (diff) | |
| download | compcert-kvx-7299996cac6c4747b6611b17f0af15fb08c6ee80.tar.gz compcert-kvx-7299996cac6c4747b6611b17f0af15fb08c6ee80.zip | |
fix reverse printing problem for hashes
Diffstat (limited to 'test/monniaux/minisat/Makefile.profiled')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index e66db1db..85e5c246 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -3,17 +3,17 @@ CFILES=main.c solver.c clock.c CCOMP=../../../ccomp -GCC=aarch64-linux-gnu-gcc -#GCC=k1-cos-gcc -EXECUTE=qemu-aarch64 +#GCC=aarch64-linux-gnu-gcc +GCC=k1-cos-gcc +#EXECUTE=qemu-aarch64 #EXECUTE=qemu-arm -#EXECUTE=k1-cluster -- +EXECUTE=k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- LIBS=-lm PROFILING_DAT=compcert_profiling.dat EXAMPLE=sudoku.sat -CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm +CCOMPFLAGS=-static -finline-asm -finline-auto-threshold 50 GCCFLAGS=-static ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log |