Skip to content

Commit 53e645b

Browse files
More flexible result checks
In order to handle how 2LS lists the failed properties (in the format "[property-name] description: status").
1 parent 5e479a5 commit 53e645b

File tree

1 file changed

+10
-8
lines changed

1 file changed

+10
-8
lines changed

tool-wrapper.inc

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -28,18 +28,20 @@ if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {
2828

2929
parse_result()
3030
{
31-
if tail -n 50 $LOG.ok | grep -q "^[[:space:]]*__CPROVER_memory_leak == NULL$"\
32-
; then
31+
if tail -n 50 $LOG.ok | \
32+
grep -Eq "^(\[.*\] |[[:space:]]*)__CPROVER_memory_leak == NULL$" ; then
3333
echo 'FALSE(valid-memtrack)'
34-
elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*dereference failure:" ; then
34+
elif tail -n 50 $LOG.ok | \
35+
grep -Eq "^(\[.*\] |[[:space:]]*)dereference failure:" ; then
3536
echo 'FALSE(valid-deref)'
36-
elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*double free$" ; then
37+
elif tail -n 50 $LOG.ok | \
38+
grep -Eq "^(\[.*\] |[[:space:]]*)double free$" ; then
3739
echo 'FALSE(valid-free)'
38-
elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*free argument has offset zero\
39-
$" ; then
40+
elif tail -n 50 $LOG.ok | \
41+
grep -Eq "^(\[.*\] |[[:space:]]*)free argument has offset zero$" ; then
4042
echo 'FALSE(valid-free)'
41-
elif tail -n 50 $LOG.ok | grep -q "^[[:space:]]*arithmetic overflow on signed\
42-
" ; then
43+
elif tail -n 50 $LOG.ok | \
44+
grep -Eq "^(\[.*\] |[[:space:]]*)arithmetic overflow on signed" ; then
4345
echo 'FALSE(no-overflow)'
4446
elif [[ "$PROP" == "termination" ]]; then
4547
echo 'FALSE(termination)'

0 commit comments

Comments
 (0)