diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-24 18:21:26 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-24 18:21:26 +0200 |
commit | 01478f937f0f97f78f793c6b037b5ab4b57388c2 (patch) | |
tree | 3959f8e7ba45ab3e4a8ad977295653b8f2bfa065 /test | |
parent | 2fa48a42bea76b7220329d6a291411810e852d11 (diff) | |
download | compcert-kvx-01478f937f0f97f78f793c6b037b5ab4b57388c2.tar.gz compcert-kvx-01478f937f0f97f78f793c6b037b5ab4b57388c2.zip |
for reducing
Diffstat (limited to 'test')
-rw-r--r-- | test/monniaux/picosat-965/onefile/picosat.c | 2 | ||||
-rwxr-xr-x | test/monniaux/picosat-965/onefile/testcmp.sh | 123 |
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 |