diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-25 08:14:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-25 08:14:11 +0200 |
| commit | 4e89be4cf2de3585092fdd1631bed8ba6ed83bce (patch) | |
| tree | 131c1cf88cbe3224cd1a8f607426ff3992d6e6a9 /test/monniaux | |
| parent | 2ff9a87d3603f010e7831e9d0a8d5c029dcd4846 (diff) | |
| download | compcert-kvx-4e89be4cf2de3585092fdd1631bed8ba6ed83bce.tar.gz compcert-kvx-4e89be4cf2de3585092fdd1631bed8ba6ed83bce.zip | |
improved testcmp: detect maybe uninitialized
Diffstat (limited to 'test/monniaux')
| -rwxr-xr-x | test/monniaux/picosat-965/onefile/testcmp.sh | 26 |
1 files changed, 20 insertions, 6 deletions
diff --git a/test/monniaux/picosat-965/onefile/testcmp.sh b/test/monniaux/picosat-965/onefile/testcmp.sh index bab609e2..bfcc7e7f 100755 --- a/test/monniaux/picosat-965/onefile/testcmp.sh +++ b/test/monniaux/picosat-965/onefile/testcmp.sh @@ -2,15 +2,20 @@ 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" +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 ! $HOSTCC1 $CFILES -o picosat.cc0.host ; +then exit 30 ; +fi + if ! $HOSTCC1 $CFILES -o picosat.cc1.host ; then exit 31 ; fi @@ -31,6 +36,11 @@ 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 ; @@ -61,6 +71,10 @@ if [ $? -ge 100 ]; then exit 45 ; fi +if ! cmp picosat.cc0.out picosat.cc1.out ; +then exit 60 ; +fi + if ! cmp picosat.cc1.out picosat.cc1.valgrind.out ; then exit 61 ; fi |