Updates contracts regression-test descriptions

Signed-off-by: Felipe R. Monteiro <[email protected]>

Author: feliperodri

regression/contracts/assigns_enforce_scoping_01/test.desc

@@ -3,8 +3,9 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-assertion: SUCCESS$
-assertion: FAILURE$
+^\[f1.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_scoping_02/test.desc

@@ -3,8 +3,8 @@ main.c
 --enforce-all-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-assertion: SUCCESS$
-assertion: FAILURE$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that \*b is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/quantifiers-exists-both-enforce/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-exists-both-replace/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-exists-requires-enforce/test.desc

@@ -3,7 +3,11 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that found\_four is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-exists-requires-replace/test.desc

@@ -3,8 +3,8 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
-^\[2\] assertion: FAILURE$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/contracts/quantifiers-forall-both-enforce/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-forall-both-replace/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-all-calls-with-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[precondition.\d+\] file main.c line \d+ Check requires clause: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-forall-ensures-enforce/test.desc

@@ -3,7 +3,10 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/contracts/quantifiers-forall-requires-enforce/test.desc

@@ -3,7 +3,11 @@ main.c
 --enforce-all-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[1\] assertion: SUCCESS$
+^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
+^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that i is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that is\_identity is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring