aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/Makefile
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-07-18 17:53:35 +0200
committerCyril SIX <cyril.six@kalray.eu>2019-07-18 17:53:35 +0200
commit9bc337d05eed466e2bfc9b18aa35fac34d3954a9 (patch)
tree57c1fa289e10d9d5c134cb27dace1391c98396f3 /test/monniaux/Makefile
parentc57baa03fa83d1295a3ba622986a02bd2fa6476f (diff)
downloadcompcert-kvx-9bc337d05eed466e2bfc9b18aa35fac34d3954a9.tar.gz
compcert-kvx-9bc337d05eed466e2bfc9b18aa35fac34d3954a9.zip
Fixing the generation of verifier_times.txt and oracle_times.txt
Diffstat (limited to 'test/monniaux/Makefile')
-rw-r--r--test/monniaux/Makefile10
1 files changed, 5 insertions, 5 deletions
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
index 12f2bfe2..a6b19891 100644
--- a/test/monniaux/Makefile
+++ b/test/monniaux/Makefile
@@ -2,20 +2,20 @@
CCOMP?=ccomp
-#all: compile_times.pdf measure_times.k1c.pdf
+#all: verifier_times.txt oracle_times.txt measures.csv
all: measures.csv
verifier_times.txt: Asmblockdeps.patch
- (cd ../../ && make -j20)
+ (cd ../../ && make -j20 && make install)
patch $(realpath ../../extraction/Asmblockdeps.ml) < $<
- (cd ../../ && make -j20); patch -R $(realpath ../../extraction/Asmblockdeps.ml) < $<
+ (cd ../../ && make -j20 && make install); patch -R $(realpath ../../extraction/Asmblockdeps.ml) < $<
bash clean_benches.sh
bash build_benches.sh $@
oracle_times.txt: PostpassSchedulingOracle.patch
- (cd ../../ && make -j20)
+ (cd ../../ && make -j20 && make install)
patch $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
- (cd ../../ && make -j20); patch -R $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
+ (cd ../../ && make -j20 && make install); patch -R $(realpath ../../mppa_k1c/PostpassSchedulingOracle.ml) < $<
bash clean_benches.sh
bash build_benches.sh $@