Skip to content

Commit

Permalink
fix theta-start.sh
Browse files Browse the repository at this point in the history
leventeBajczi committed Nov 20, 2024
1 parent e11abb6 commit 50f43fe
Showing 1 changed file with 4 additions and 2 deletions.
6 changes: 4 additions & 2 deletions scripts/theta-start.sh
Original file line number Diff line number Diff line change
@@ -45,21 +45,23 @@ echo "Verifying input '$IN' with property '$property' using arguments '$modified
if [ "$(basename "$property")" == "termination.prp" ]; then
transformed_property=$(dirname "$property")/unreach-call.prp
echo "Mapping property '$property' to '$transformed_property'"
TMPFILE=$(mktemp -d $PWD)
TMPFILE=$(mktemp -p $PWD)
sed 's/__VERIFIER_assert/__OLD_VERIFIER_assert/g;s/reach_error/old_reach_error/g' "$IN" > "$TMPFILE"
python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property termination --to-property reachability --algorithm InstrumentationOperator "$TMPFILE"
#"$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
modified_args="$modified_args --input-file-for-witness $IN"
IN="output/transformed_program.c"
rm "$TMPFILE"
elif [ "$(basename "$property")" == "no-overflow.prp" ]; then
transformed_property=$(dirname "$property")/unreach-call.prp
echo "Mapping property '$property' to '$transformed_property'"
TMPFILE=$(mktemp -d $PWD)
TMPFILE=$(mktemp -p $PWD)
sed 's/__VERIFIER_assert/__OLD_VERIFIER_assert/g;s/reach_error/old_reach_error/g' "$IN" > "$TMPFILE"
python3 "$scriptdir"/specification-transformation/src/specification-transformation.py --from-property no-overflow --to-property reachability --algorithm InstrumentationOperator "$TMPFILE"
#"$scriptdir"/offset.sh "$IN" "output/transformed_program.c" > witness-mapping.yml
modified_args="$modified_args --input-file-for-witness $IN"
IN="output/transformed_program.c"
rm "$TMPFILE"
else
transformed_property="$property"
fi

0 comments on commit 50f43fe

Please sign in to comment.