From 53e645b643a490f71c03a2def0d062bd4cdf30ad Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 4 Dec 2016 02:32:19 +0000 Subject: [PATCH] More flexible result checks In order to handle how 2LS lists the failed properties (in the format "[property-name] description: status"). --- tool-wrapper.inc | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/tool-wrapper.inc b/tool-wrapper.inc index 67b9fc8..d186aac 100755 --- a/tool-wrapper.inc +++ b/tool-wrapper.inc @@ -28,18 +28,20 @@ if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) { parse_result() { - if tail -n 50 $LOG.ok | grep -q "^[[:space:]]*__CPROVER_memory_leak == NULL$"\ - ; then + if tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)__CPROVER_memory_leak == NULL$" ; then echo 'FALSE(valid-memtrack)' - elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*dereference failure:" ; then + elif tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)dereference failure:" ; then echo 'FALSE(valid-deref)' - elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*double free$" ; then + elif tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)double free$" ; then echo 'FALSE(valid-free)' - elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*free argument has offset zero\ -$" ; then + elif tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)free argument has offset zero$" ; then echo 'FALSE(valid-free)' - elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*arithmetic overflow on signed\ -" ; then + elif tail -n 50 $LOG.ok | \ + grep -Eq "^(\[.*\] |[[:space:]]*)arithmetic overflow on signed" ; then echo 'FALSE(no-overflow)' elif [[ "$PROP" == "termination" ]]; then echo 'FALSE(termination)'