diff options
Diffstat (limited to 'test/mppa/check.sh')
| -rwxr-xr-x[-rw-r--r--] | test/mppa/check.sh | 34 |
1 files changed, 4 insertions, 30 deletions
diff --git a/test/mppa/check.sh b/test/mppa/check.sh index dd9691be..8db50f1b 100644..100755 --- a/test/mppa/check.sh +++ b/test/mppa/check.sh @@ -1,32 +1,6 @@ -# $1: binary file to check -# $2: output check token +#!/bin/bash +# Tests the execution of the binaries produced by CompCert -elffile="$1" -token="$2" +source do_test.sh -if [ ! -f $elffile ]; then - >&2 echo "ERROR: $elffile not found" - shift; continue -fi - -dir="$(dirname $elffile)" -elf="$(basename $elffile)" - -exp="$dir/../output/$elf.exp" -out="$dir/../output/$elf.out" -if [ ! -f $exp ]; then - >&2 echo "ERROR: $exp not found" - exit -fi - -k1-cluster -- $elffile > $out -echo $? >> $out - -if ! diff $exp $out; then - >&2 echo "ERROR: $exp and $out differ" - exit -fi - -echo "PASSED: $elf" -touch $token -#shift +do_test check |