diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
| commit | 271f87ba08f42340900378c0797511d4071fc1b8 (patch) | |
| tree | 8b861fa3221b179bb8e3ad339864cdb7c541d46a /test | |
| parent | e6a1df51a2a3d29c58d72453355e50a979e86297 (diff) | |
| download | compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.tar.gz compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.zip | |
BTL Scheduler oracle and some drafts
Diffstat (limited to 'test')
| -rwxr-xr-x | test/c/cscript.sh | 21 | ||||
| -rwxr-xr-x | test/c/cscript2.sh | 5 | ||||
| -rwxr-xr-x | test/c/pbcompare.sh | 18 |
3 files changed, 44 insertions, 0 deletions
diff --git a/test/c/cscript.sh b/test/c/cscript.sh new file mode 100755 index 00000000..f797df7b --- /dev/null +++ b/test/c/cscript.sh @@ -0,0 +1,21 @@ +#!/bin/bash + +CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others" +CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others" + +$CCREF nsieve.c > refout 2>&1 +mv a.out ref.out +$CCTEST nsieve.c > testout 2>&1 +#sort -k1 -n -t, refout -o refout +#sort -k1 -n -t, testout -o testout +qemu-riscv64 ref.out > logref 2>&1 +{ qemu-riscv64 a.out > logtest 2>&1; } 2> logtest +if cat logref | ack "Primes"; then + if cmp -s logref logtest; then + exit 1 + else + exit 0 + fi +else + exit 1 +fi diff --git a/test/c/cscript2.sh b/test/c/cscript2.sh new file mode 100755 index 00000000..350c392d --- /dev/null +++ b/test/c/cscript2.sh @@ -0,0 +1,5 @@ +#/bin/bash + +/home/gourdinl/Work/VERIMAG/Compcert_riscv_third/ccomp -static -fprepass= revlist -U__GNUC__ -stdlib ../../runtime -dclight -dasm -c qsort.c > log 2>&1 + +cat log | ack "instead of Some" diff --git a/test/c/pbcompare.sh b/test/c/pbcompare.sh new file mode 100755 index 00000000..b47c83c4 --- /dev/null +++ b/test/c/pbcompare.sh @@ -0,0 +1,18 @@ +#!/bin/bash + +CCREF="/home/yuki/Work/VERIMAG/Compcert_riscv_bis/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_bis/runtime -fno-expanse-rtlcond -fno-expanse-others" +CCTEST="/home/yuki/Work/VERIMAG/Compcert_riscv_third/ccomp -static -S -stdlib /home/yuki/Work/VERIMAG/Compcert_riscv_third/runtime -fno-expanse-rtlcond -fno-expanse-others" + +for prog in *.c; do + $CCREF $prog > refout 2>&1 + $CCTEST $prog > testout 2>&1 + sort -k1 -n -t, refout -o refout + sort -k1 -n -t, testout -o testout + if cmp -s refout testout; then + echo "$prog passed" + else + echo "$prog failed" + diff -y refout testout + exit 1 + fi +done |