diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-26 10:26:11 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-26 10:26:11 +0200 |
commit | a7ba9012a490f44976d4301fdc602be27ac5eb02 (patch) | |
tree | 10ac16e4b2b9f69b79bf91fa93f7626506d2ae0a /test | |
parent | 373c56a41c4e8fdb12ec4d56aed03a268503603b (diff) | |
parent | 2ff9a87d3603f010e7831e9d0a8d5c029dcd4846 (diff) | |
download | compcert-kvx-a7ba9012a490f44976d4301fdc602be27ac5eb02.tar.gz compcert-kvx-a7ba9012a490f44976d4301fdc602be27ac5eb02.zip |
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
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..bab609e2 --- /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 > 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 > 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.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 |