From 162e6e98afd1023e99f93f0c1c035120fa924dfe Mon Sep 17 00:00:00 2001 From: kroening Date: Sun, 26 Oct 2014 14:11:38 +0000 Subject: [PATCH] property IDs have changed git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4664 6afb6bc1-c8e4-404c-8f48-9ae832c5b171 --- regression/cbmc/Multi_Dimensional_Array6/test.desc | 5 +++-- regression/cbmc/Pointer_byte_extract5/test.desc | 6 +++--- regression/cbmc/Pointer_byte_extract8/test.desc | 6 +++--- 3 files changed, 9 insertions(+), 8 deletions(-) diff --git a/regression/cbmc/Multi_Dimensional_Array6/test.desc b/regression/cbmc/Multi_Dimensional_Array6/test.desc index a4c00cbdbc..bb31956ca0 100644 --- a/regression/cbmc/Multi_Dimensional_Array6/test.desc +++ b/regression/cbmc/Multi_Dimensional_Array6/test.desc @@ -1,9 +1,10 @@ CORE main.c ---unwind 3 --no-unwinding-assertions --all-claims +--unwind 3 --no-unwinding-assertions --all-properties ^EXIT=0$ ^SIGNAL=0$ -^\[main\.2\] : FAILED$ +^\[main\.assertion\.1\] : OK$ +^\[main\.assertion\.2\] : FAILED$ ^\*\* 1 of 2 failed (2 iterations)$ -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index ba5a37372d..9cd8254a18 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -1,9 +1,9 @@ CORE main.c ---all-claims --bounds-check --32 +--all-properties --bounds-check --32 ^EXIT=0$ ^SIGNAL=0$ -^\[main\.11\] array.List upper bound in .*: FAILED$ -^\*\* 1 of 11 failed (2 iterations)$ +^\[main\.array_bounds\.11\] array.List upper bound in .*: FAILED$ +^\*\* 1 of 9 failed (2 iterations)$ -- ^warning: ignoring diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc index b2c346e6f1..0215dfc436 100644 --- a/regression/cbmc/Pointer_byte_extract8/test.desc +++ b/regression/cbmc/Pointer_byte_extract8/test.desc @@ -1,9 +1,9 @@ KNOWNBUG main.c ---all-claims --bounds-check --32 --no-simplify +--all-properties --bounds-check --32 --no-simplify ^EXIT=0$ ^SIGNAL=0$ -^\[main\.11\] array.List upper bound: FAILED$ -^\*\* 1 of 11 failed (2 iterations)$ +^\[main\.array_bounds\.5\] array.List upper bound: FAILED$ +^\*\* 1 of 9 failed (2 iterations)$ -- ^warning: ignoring