Commit d9725c4f authored by Martin Spiessl's avatar Martin Spiessl

Fix improper result handling with newer BenchExec

The tool-info module of CPAchecker was changed and is
now giving the wrong result on older CPAchecker versions.
It outputs false when it should be false(unreach-call).
parent 1bc86df7
#!/bin/bash
if [ -f metaval.zip ]
then
rm metaval.zip
......
......@@ -2,7 +2,7 @@
set -e
count=0
name=""
VERSION="0.1.7"
VERSION="0.1.8"
if [ "$1" == "--version" ]
then
......@@ -74,9 +74,11 @@ echo "task is $name"
echo "generating residual program from task and witness"
echo $TRANSFORMERCMD
TRANSFORMERCMD="CPAchecker/scripts/cpa.sh -witness2reach -spec $witness $name -setprop witness.useInvariantsAsAssumptions=true -setprop witness.checkInvariantViolations=true -setprop cpa.arg.export.code.header=false -setprop witness.strictChecking=false -setprop witness.checkProgramHash=false"
ARCHITECTUREWARNING="Cannot parse witness: The architecture assumed for the given verification-task differs from the architecture assumed by the witness."
echo $TRANSFORMERCMD
# temporary workaround for the architecture (it is irrelevant for the transformation step, but CPAchecker still complains if it does not match).
if eval $TRANSFORMERCMD 2>&1 1>/dev/null | perl -pe "print STDERR $_;" | grep -q "$ARCHITECTUREWARNING" ; then
echo "architecture mismatch detected. This is irrelevant for program transformation, retrying with 64 bit:"
......@@ -88,4 +90,5 @@ cd "$verifier"
echo "$verifier"
echo $(pwd)
echo "$@"
exec "$@"
exec "$@" | sed --expression='s|__VERIFIER_error(); called in|unreach-call: __VERIFIER_error(); called in|g'
# sed is called to work around the fact that CPAchecker from SV-COMP'19 does not get handled properly by newer BenchExec versions
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment