CONTRACTS: New class instrument_spec_assignst encapsulating assigns clause checking logic.

regression/contracts/assigns-enforce-malloc-zero/test.desc

@@ -1,9 +1,10 @@
 CORE
 main.c
 --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
+^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
+^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo\.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that objects of size zero or __CPROVER_max_malloc_size

regression/contracts/assigns-replace-ignored-return-value/test.desc

@@ -5,7 +5,7 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-^[.*] Check that .*ignored_return_value.* is assignable: FAILURE
+^\[.*assigns.*\].*ignored_return_value.*FAILURE
 --
 This test checks that when replacing a call by a contract for a call that
 ignores the return value of the function, the temporary introduced to 

regression/contracts/assigns_enforce_02/test.desc

@@ -1,6 +1,8 @@
 CORE
 main.c
 --enforce-contract foo
+^\[foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$
+^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_03/test.desc

@@ -1,9 +1,21 @@
 CORE
 main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that verification succeeds when assigns clauses are respected through multiple function calls.

regression/contracts/assigns_enforce_04/test.desc

@@ -1,12 +1,15 @@
 CORE
 main.c
 --enforce-contract f1
+^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
+^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$
+^\[f3.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
-^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
-^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$
-^VERIFICATION SUCCESSFUL$
 --
 --
 This test checks that verification only considers assigns clause from enforced function.

regression/contracts/assigns_enforce_15/test.desc

@@ -1,11 +1,12 @@
 CORE
 main.c
 --enforce-contract foo --enforce-contract baz --enforce-contract qux
+^\[foo.assigns.\d+\] line \d+ Check that \*x is valid: SUCCESS$
+^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
+^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\[baz.\d+\] line \d+ Check that global is assignable: FAILURE$
-^\[qux.\d+\] line \d+ Check that global is assignable: FAILURE$
-^VERIFICATION FAILED$
 --
 --
 Checks whether verification fails when enforcing a contract

regression/contracts/assigns_enforce_18/test.desc

@@ -1,16 +1,20 @@
 CORE
 main.c
 --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
+^\[foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$
+^\[foo.assigns.\d+\] line 11 Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
+^\[bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$
+^\[bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$
+^\[bar.assigns.\d+\] line 19 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
+^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
+^\[baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$
+^\[baz.assigns.\d+\] line 25 Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
+^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
-^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
-^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
-^VERIFICATION FAILED$
 --
 --
 Checks whether contract enforcement works with functions that deallocate memory.

regression/contracts/assigns_enforce_19/test.desc

@@ -1,14 +1,15 @@
 CORE
 main.c
 --enforce-contract f --enforce-contract g
+^\[f.assigns.\d+\] line 9 Check that a is assignable: SUCCESS$
+^\[g.assigns.\d+\] line 14 Check that b is valid: SUCCESS$
+^\[g.assigns.\d+\] line 16 Check that b is assignable: SUCCESS$
+^\[g.assigns.\d+\] line 17 Check that c is assignable: FAILURE$
+^\[g.assigns.\d+\] line 18 Check that \*points_to_b is assignable: SUCCESS$
+^\[g.assigns.\d+\] line 19 Check that \*points_to_c is assignable: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$
-^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$
-^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$
-^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$
-^VERIFICATION FAILED$
 --
 --
 Checks whether contract enforcement works with (local and global) static variables.

regression/contracts/assigns_enforce_20/test.desc

@@ -3,8 +3,8 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_21/test.desc

@@ -1,12 +1,12 @@
 CORE
 main.c
 --enforce-contract foo --replace-call-with-contract quz
+^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
+^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-main.c function bar
-^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE
-^VERIFICATION FAILED$
 --
 --
 Checks whether checks write set for sub-function calls.

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,11 +1,13 @@
 CORE
 main.c
 --enforce-contract f1 --enforce-contract f2
-^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$
-^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
+^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
+^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
+^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
+^\[f2.assigns.\d+\] line 12 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid: SUCCESS$
+^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$
+^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$
+^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,10 +1,11 @@
 CORE
 main.c
 --enforce-contract uses_assigns
+^\[uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[\(.*int\)i\]\) is valid: SUCCESS$
+^\[assigns_ptr.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
-^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
-^VERIFICATION SUCCESSFUL$
 --
 --
 Checks whether verification succeeds for array elements at a symbolic index. 

regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc

@@ -2,8 +2,9 @@ CORE
 main.c
 --enforce-contract foo
 ^main.c function foo$
-^\[foo\.\d+\] line 16 Check that \*x is assignable: SUCCESS$
-^\[foo\.\d+\] line 20 Check that \*x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 10 Check that \*x is valid when .*: SUCCESS$
+^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_lvalue/test.desc

@@ -2,12 +2,14 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
-^\[foo\.\d+\] line 8 Check that \*y is assignable: FAILURE$
-^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
-^\[foo\.\d+\] line 13 Check that \*y is assignable: SUCCESS$
-^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
-^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 3 Check that \*y is valid when !\(a != FALSE\): SUCCESS$
+^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc

@@ -2,12 +2,14 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
-^\[foo\.\d+\] line 8 Check that \*y is assignable: SUCCESS$
-^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
-^\[foo\.\d+\] line 13 Check that \*y is assignable: FAILURE$
-^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
-^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 3 Check that \*y is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_pointer_object/test.desc

@@ -2,12 +2,14 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo\.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
-^\[foo\.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
-^\[foo\.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 7 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when !\(a != FALSE\): SUCCESS$
+^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc

@@ -2,16 +2,17 @@ CORE
 main.c
 --enforce-contract foo
 main.c function foo
-^\[foo\.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
-^\[foo\.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
-^\[foo\.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
-^\[foo\.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when a != FALSE: SUCCESS$
+^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 --
-Check that conditional assigns clause  `c ? {__CPROVER_POINTER_OBJECT((p), .. }`
-match with control flow path conditions.
+Check that conditional target groups match with control flow path conditions.

regression/contracts/assigns_enforce_conditional_unions/test.desc

@@ -1,18 +1,22 @@
 CORE
 main.c
 --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
-^\[is_high_level.\d+\] line 50 Check that latch is assignable: SUCCESS$
-^\[is_high_level.\d+\] line 51 Check that once is assignable: SUCCESS$
-^\[update.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
-^\[update.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
-^\[update.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
-^\[update.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
-^\[update.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
-^\[update.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
-^\[update.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
-^\[update.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
-^\[update.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
-^\[update.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
+^\[update.assigns.\d+] line 73 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS
+^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS
+^\[update.assigns.\d+] line 76 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS
+^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS
+^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$
+^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$
+^\[update.assigns.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
+^\[update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
+^\[update.assigns.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
+^\[update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
+^\[update.assigns.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
+^\[update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
+^\[update.assigns.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
+^\[update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
+^\[update.assigns.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
+^\[update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_detect_local_statics/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
 --enforce-contract bar
-^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS
-^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS
-^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE
+^\[foo.assigns.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line 20 Check that \*yy is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$