Skip to content

Commit

Permalink
Verus error handling
Browse files Browse the repository at this point in the history
Ignore `_opam`
  • Loading branch information
JonasAlaif committed Dec 29, 2024
1 parent 2e04489 commit 381e647
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 1 deletion.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
*.log
_opam
7 changes: 6 additions & 1 deletion verus/run.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,16 @@ OUT="$(pwd)/$(echo "${OP[0]%.*}" | sed 's/ /_/g')/${OP[1]}"
mkdir -p "$(dirname "$OUT")"

cd "$(dirname "$0")/verus/source"
VARGO="../tools/vargo/target/release/vargo"
export VERUS_EXTRA_ARGS="--log-dir $OUT --log smt --rlimit $3"
export VARGO_IN_NEXTEST=true
TEST=($1)
FILE=${TEST[0]#$(pwd)/rust_verify_test/tests/}
vargo test --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact &> /dev/null || exit 1
OUTPUT=$($VARGO test --release --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact 2>&1)
if [ $? -ne 0 ]; then
echo "[ERROR] $OUTPUT"
exit 1
fi
if [ -f "$OUT/root.smt2" ]; then
mv "$OUT/root.smt2" "$OUT.smt2"
rmdir "$OUT" || true
Expand Down

0 comments on commit 381e647

Please sign in to comment.