aboutsummaryrefslogtreecommitdiffstats
path: root/test/monniaux/picosat-965
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-07-24 18:21:26 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-07-24 18:21:26 +0200
commit01478f937f0f97f78f793c6b037b5ab4b57388c2 (patch)
tree3959f8e7ba45ab3e4a8ad977295653b8f2bfa065 /test/monniaux/picosat-965
parent2fa48a42bea76b7220329d6a291411810e852d11 (diff)
downloadcompcert-kvx-01478f937f0f97f78f793c6b037b5ab4b57388c2.tar.gz
compcert-kvx-01478f937f0f97f78f793c6b037b5ab4b57388c2.zip
for reducing
Diffstat (limited to 'test/monniaux/picosat-965')
-rw-r--r--test/monniaux/picosat-965/onefile/picosat.c2
-rwxr-xr-xtest/monniaux/picosat-965/onefile/testcmp.sh123
2 files changed, 124 insertions, 1 deletions
diff --git a/test/monniaux/picosat-965/onefile/picosat.c b/test/monniaux/picosat-965/onefile/picosat.c
index b255f3ee..4f8ee768 100644
--- a/test/monniaux/picosat-965/onefile/picosat.c
+++ b/test/monniaux/picosat-965/onefile/picosat.c
@@ -6243,7 +6243,7 @@ flbcp (PS * ps)
#endif
}
-inline static INLINE int
+inline static int
cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b)
{
(void) ps;
diff --git a/test/monniaux/picosat-965/onefile/testcmp.sh b/test/monniaux/picosat-965/onefile/testcmp.sh
new file mode 100755
index 00000000..ffeb5e03
--- /dev/null
+++ b/test/monniaux/picosat-965/onefile/testcmp.sh
@@ -0,0 +1,123 @@
+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 -Werror $DEFINES"
+HOSTCC1="gcc -O -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC2="gcc -O -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+HOSTCC3="gcc -O3 -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC4="clang -O -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC5="clang -O -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+CFILES="picosat.c"
+SIMU="kvx-cluster --timeout=100000 -- "
+
+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.cc1.host $DATA 2>&1 | tee picosat.cc1.out
+if [ $? -ge 100 ];
+then exit 41 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc1.valgrind.log ./picosat.cc1.host $DATA 2>&1 | tee picosat.cc1.valgrind.out
+if [ $? -ge 100 ];
+then exit 51 ;
+fi
+
+timeout 1 ./picosat.cc2.host $DATA 2>&1 | tee picosat.cc2.out
+if [ $? -ge 100 ];
+then exit 42 ;
+fi
+
+timeout 1 ./picosat.cc3.host $DATA 2>&1 | tee picosat.cc3.out
+if [ $? -ge 100 ];
+then exit 43 ;
+fi
+
+timeout 1 ./picosat.cc4.host $DATA 2>&1 | tee picosat.cc4.out
+if [ $? -ge 100 ];
+then exit 44 ;
+fi
+
+timeout 1 ./picosat.cc5.host $DATA 2>&1 | tee picosat.cc5.out
+if [ $? -ge 100 ];
+then exit 45 ;
+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 | tee 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 | tee 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 | tee picosat.prepass.out
+if [ $? -ge 100 ];
+then exit 0 ;
+fi
+
+if cmp picosat.gcc.out picosat.prepass.out ;
+then exit 7 ;
+fi
+
+exit 0