Cleans up test descs from contracts regression

feliperodri · feliperodri · commit d9d21f1dc5ec · 2021-09-02T17:16:33.000Z
Avoid escaping unnecessary characters.

Signed-off-by: Felipe R. Monteiro &lt;felisous@amazon.com&gt;
diff --git a/regression/contracts/assigns_enforce_17/test.desc b/regression/contracts/assigns_enforce_17/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.assertion.\d+\] line \d+ assertion x \=\= 0\: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc
@@ -3,10 +3,10 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
-^\[f2.\d+\] line \d+ Check that p\-\>x is assignable\: FAILURE$
-^\[f3.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable\: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
+^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
+^\[f4.\d+\] line \d+ Check that p is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_structs_05/test.desc b/regression/contracts/assigns_enforce_structs_05/test.desc
@@ -3,10 +3,10 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
-^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)0\] is assignable\: SUCCESS$
-^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)1\] is assignable\: SUCCESS$
-^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)2\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_structs_06/test.desc b/regression/contracts/assigns_enforce_structs_06/test.desc
@@ -3,14 +3,14 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: SUCCESS$
-^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)1\] is assignable\: SUCCESS$
-^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)2\] is assignable\: SUCCESS$
-^\[f1.\d+\] line \d+ Check that p\-\>size is assignable\: FAILURE$
-^\[f2.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
-^\[f2.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
-^\[f3.\d+\] line \d+ Check that p\-\>buf is assignable\: SUCCESS$
-^\[f3.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p->size is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc
@@ -3,10 +3,10 @@ main.c
 --enforce-all-contracts _ --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
-^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure\: pointer NULL in p\-\>buf\: FAILURE$
-^\[f2.\d+\] line \d+ Check that pp\-\>p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
-^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure\: pointer NULL in pp\-\>p\-\>buf\: FAILURE$
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
+^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc
@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts _ --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure\: pointer NULL in p\-\>buf\: FAILURE$
-^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=\> p\-\>buf\[0\] \=\= 0\: FAILURE$
+^\[pointer\_dereference.\d+\] file main.c line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion p \!\= NULL \=\=> p->buf\[0\] \=\= 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[foo10.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
-^\[foo10.\d+\] line \d+ Check that buffer\-\>aux\.allocated is assignable: SUCCESS$
+^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
+^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$
 ^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
@@ -14,10 +14,10 @@ main.c
 ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
 ^\[foo5.\d+\] line \d+ Check that buffer.len is assignable: SUCCESS$
-^\[foo6.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
-^\[foo6.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
-^\[foo7.\d+\] line \d+ Check that \*buffer\-\>data is assignable: SUCCESS$
-^\[foo7.\d+\] line \d+ Check that buffer\-\>len is assignable: SUCCESS$
+^\[foo6.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$
+^\[foo6.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
+^\[foo7.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$
+^\[foo7.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_validity_pointer_03/test.desc b/regression/contracts/assigns_validity_pointer_03/test.desc
@@ -7,7 +7,7 @@ main.c
 // bar
 ASSERT \*x > 0
 IF !\(\*x == 3\) THEN GOTO \d
-tmp_if_expr = \*y == 5 \? true \: false;
+tmp_if_expr = \*y == 5 \? true : false;
 ASSUME tmp_if_expr
 // baz
 ASSUME \*z == 7
diff --git a/regression/contracts/history-pointer-enforce-09/test.desc b/regression/contracts/history-pointer-enforce-09/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^\[foo.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc
@@ -3,16 +3,16 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
-^\[postcondition.\d+\] file main.c line \d+ Check ensures clause\: SUCCESS$
-^\[bar.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable\: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*p\-\>y is assignable\: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable\: SUCCESS$
-^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == 7\: SUCCESS$
-^\[main.assertion.\d+\] line \d+ assertion \*\(p\-\>y\) == -1\: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
+^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == -1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/history-pointer-enforce-11/test.desc b/regression/contracts/history-pointer-enforce-11/test.desc
@@ -3,8 +3,8 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[postcondition.\d+\] Check ensures clause\: SUCCESS$
-^\[foo.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^\[postcondition.\d+\] Check ensures clause: SUCCESS$
+^\[foo.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/history-pointer-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc
@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[precondition.\d+\] file main.c line \d+ Check requires clause\: SUCCESS$
-^\[main.assertion.\d+\] line \d+ assertion p\-\>y \!\= 7\: FAILURE$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
-\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion n\[9\] == 113: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/test_array_memory_too_small_replace/test.desc b/regression/contracts/test_array_memory_too_small_replace/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 \[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE
-\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/test_scalar_memory_replace/test.desc b/regression/contracts/test_scalar_memory_replace/test.desc
@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \_\_CPROVER\_r\_ok\(n, sizeof\(int\)\): SUCCESS
-\[main.assertion.\d+\] line \d+ assertion o \>\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion o >\= 10 \&\& o \=\= \*n \+ 5: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/test_struct_enforce/test.desc b/regression/contracts/test_struct_enforce/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[foo.\d+\] line \d+ Check that x-\>baz is assignable: SUCCESS
-\[foo.\d+\] line \d+ Check that x-\>qux is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that x->baz is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that x->qux is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= 10: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[foo.\d+\] line \d+ Check that x-\>str\[\(.*\)\(x-\>len - 1\)\] is assignable: SUCCESS
+\[foo.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/test_struct_replace/test.desc b/regression/contracts/test_struct_replace/test.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS
-\[main.assertion.\d+\] line \d+ assertion rval \=\= x-\>baz \+ x-\>qux: SUCCESS
+\[main.assertion.\d+\] line \d+ assertion rval \=\= x->baz \+ x->qux: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \*x \=\= \*y: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/trivial_contract_enforce/test.desc b/regression/contracts/trivial_contract_enforce/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/trivial_contract_replace/test.desc b/regression/contracts/trivial_contract_replace/test.desc
@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$
+^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
