. lib/flavour vanilla
. lib/testcase

EXTRA_FILES=
FLAGS=
. $1
if test -z $TESTCASE; then
    TESTCASE=$(basename $1 | sed 's/^[0-9u].\([^.]*\)\..*$/\1/')
fi

cat > unittest.cpp <<EOF
#define BRICK_UNITTEST_MAIN
#include <brick-unittest>
#undef BRICK_UNITTEST_MAIN

#include <$TESTCASE>
EOF

TESTFILE=$SRC_ROOT/$TESTCASE
test -f $TESTFILE || TESTFILE="$SRC_ROOT/bricks/$TESTCASE"

TESTNS=`grep 'namespace t_' $TESTFILE | sed 's/^.*\(t_[^ ]*\).*$/\1/'` \
    || exit 200 # skip if there is not test in the file

divine cc -std=c++14 -DBRICK_UNITTEST_REG -DNVALGRIND -I$SRC_ROOT/bricks $FLAGS $EXTRA_FILES unittest.cpp -o unittest.bc
for NS in $TESTNS; do
    divine verify --threads 1 --num-callers 65536 -o nofail:malloc unittest.bc $NS | tee verify.out
done

check verify "$1"

# vim: syntax=sh