Commit 9054b48a authored by Martin Spiessl's avatar Martin Spiessl

Fix typo and ensure hash checking is disabled

parent 4dc4876f
......@@ -74,11 +74,11 @@ echo "task is $name"
echo "generating residual program from task and witness"
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"
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."
# 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 |grep -q "ARCHITECTUREWARNING" ; then
if eval $TRANSFORMERCMD 2>&1 1>/dev/null |grep -q "$ARCHITECTUREWARNING" ; then
$TRANSFORMERCMD -64 1>/dev/null
fi
......
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