diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 12:25:31 +0100 |
commit | 73a83b969dbb6f4c419ebdcc663f463509b6d6e3 (patch) | |
tree | 259852cd3272f2f31a09d75ac24e31ec1aaa8d9e /test/monniaux/picosat-965/onefile/testcmp.sh | |
parent | 3570ba2827908b280315c922ba7e43289f6d802a (diff) | |
parent | 035a1a9f4b636206acbae4506c5fc4ef322de0c1 (diff) | |
download | compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.tar.gz compcert-kvx-73a83b969dbb6f4c419ebdcc663f463509b6d6e3.zip |
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
Diffstat (limited to 'test/monniaux/picosat-965/onefile/testcmp.sh')
-rwxr-xr-x | test/monniaux/picosat-965/onefile/testcmp.sh | 146 |
1 files changed, 146 insertions, 0 deletions
diff --git a/test/monniaux/picosat-965/onefile/testcmp.sh b/test/monniaux/picosat-965/onefile/testcmp.sh new file mode 100755 index 00000000..2228c675 --- /dev/null +++ b/test/monniaux/picosat-965/onefile/testcmp.sh @@ -0,0 +1,146 @@ +DEFINES="-DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG" +COMPCERT=/local/monniaux/Kalray/mppa-RTLpathSE-verif-hash-junk +DATA=$COMPCERT/test/monniaux/picosat-965/tiny.dat +CCOMP="$COMPCERT/ccomp -fbitfields -fduplicate 2 -fall-loads-nontrap $DEFINES" +GCC="kvx-cos-gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES" +HOSTCC0="gcc -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES" +HOSTCC1="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES" +HOSTCC2="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES" +HOSTCC3="gcc -O3 -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES" +HOSTCC4="clang -Wimplicit -Wuninitialized -Werror $DEFINES" +HOSTCC5="clang -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES" +CFILES="picosat.c" +SIMU="kvx-cluster --timeout=100000 -- " + +if ! $HOSTCC0 $CFILES -o picosat.cc0.host ; +then exit 30 ; +fi + +if ! $HOSTCC1 $CFILES -o picosat.cc1.host ; +then exit 31 ; +fi + +if ! $HOSTCC2 $CFILES -o picosat.cc2.host ; +then exit 32 ; +fi + +if ! $HOSTCC3 $CFILES -o picosat.cc3.host ; +then exit 33 ; +fi + +if ! $HOSTCC4 $CFILES -o picosat.cc4.host ; +then exit 34 ; +fi + +if ! $HOSTCC5 $CFILES -o picosat.cc5.host ; +then exit 35 ; +fi + +timeout 1 ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.out +if [ $? -ge 100 ]; +then exit 40 ; +fi + +timeout 1 ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.out +if [ $? -ge 100 ]; +then exit 41 ; +fi + +timeout 1 valgrind --log-file=picosat.cc0.valgrind.log ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.valgrind.out +if [ $? -ge 100 ]; +then exit 50 ; +fi + +timeout 1 valgrind --log-file=picosat.cc1.valgrind.log ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.valgrind.out +if [ $? -ge 100 ]; +then exit 51 ; +fi + +timeout 1 ./picosat.cc2.host $DATA 2>&1 > picosat.cc2.out +if [ $? -ge 100 ]; +then exit 42 ; +fi + +timeout 1 ./picosat.cc3.host $DATA 2>&1 > picosat.cc3.out +if [ $? -ge 100 ]; +then exit 43 ; +fi + +timeout 1 ./picosat.cc4.host $DATA 2>&1 > picosat.cc4.out +if [ $? -ge 100 ]; +then exit 44 ; +fi + +timeout 1 ./picosat.cc5.host $DATA 2>&1 > picosat.cc5.out +if [ $? -ge 100 ]; +then exit 45 ; +fi + +if ! cmp picosat.cc0.out picosat.cc1.out ; +then exit 60 ; +fi + +if ! cmp picosat.cc0.out picosat.cc0.valgrind.out ; +then exit 70 ; +fi + +if ! cmp picosat.cc1.out picosat.cc1.valgrind.out ; +then exit 61 ; +fi + +if ! cmp picosat.cc1.out picosat.cc2.out ; +then exit 62 ; +fi + +if ! cmp picosat.cc1.out picosat.cc3.out ; +then exit 63 ; +fi + +if ! $GCC $CFILES -o picosat.gcc.target ; +then exit 1 ; +fi + +if ! $CCOMP $CFILES -o picosat.ccomp.target ; +then exit 2 ; +fi + +if ! $CCOMP -fprepass -fprepass= list $CFILES -o picosat.prepass.target ; +then exit 3 ; +fi + +$SIMU ./picosat.gcc.target $DATA 2>&1 > picosat.gcc.out +if [ $? -ge 100 ]; +then exit 4 ; +fi + +if ! cmp picosat.gcc.out picosat.cc1.out ; +then exit 13 ; +fi + +if grep timeout picosat.gcc.out ; +then exit 8 ; +fi + +$SIMU ./picosat.ccomp.target $DATA 2>&1 > picosat.ccomp.out +if [ $? -ge 100 ]; +then exit 5 ; +fi + +if grep timeout picosat.ccomp.out ; +then exit 9 ; +fi + +if ! cmp picosat.gcc.out picosat.ccomp.out ; +then exit 6 ; +fi + +$SIMU ./picosat.prepass.target $DATA 2>&1 > picosat.prepass.out +if [ $? -ge 100 ]; +then exit 0 ; +fi + +if cmp picosat.gcc.out picosat.prepass.out ; +then exit 7 ; +fi + +exit 0 |