. lib/flavour vanilla
. lib/testcase

# This will run the .build script, which is supposed to compile everything
# needed for verification into main.bc and can optionally produce main.? files
# with test specifications. Each of these files can contain something like:
# ERRSPEC: error specification
# DIVINE_OPTS: divine flags
# PROGRAM_OPTS: program options and flags
# TYPE: verify | run
#
# Verify will be run for each of these specifications. If no specification is
# given, verify will run once without any additional options. Keys not found in
# the file behave as empty.
#
# You should refer files in the .data directory as ${DATA}file.

export DATA=$1/
export BUILD=$DATA/build.sh

echo 'FILE: main.bc' > check.default
bash -x $BUILD
test -e check.* || skip

SPECS=check.*

for i in $SPECS; do
    DIVINE_OPTS=
    PROGRAM_OPTS=
    TYPE=verify
    RESOURCES=
    FILE=main.bc

    eval `sed "s/:\(.*\)/='\1'"/ $i`

    if test "$TYPE" = verify; then
        test -z "$RESOURCES" && RESOURCES="--max-memory 4GiB --threads 1"
        test -z "$EXTRA" && EXTRA="--num-callers 65536"
    fi

    if echo "$DIVINE_OPTS" | grep -q "symbolic"; then
        z3 --version > /dev/null || skip
    fi

    test -e $FILE || skip

    divine $TYPE $RESOURCES $EXTRA \
           $DIVINE_OPTS $FILE $PROGRAM_OPTS | tee verify.out
done

# vim: syntax=sh