label_properties: do not rely on source_locationt's get_function()

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception1.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException1:()V.1'
+--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception2.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException2:()V.1'
+--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetLength/test_exception.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException:()V.1'
+--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException1:()V.1'
+--function Test.testException1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException2:()V.1'
+--function Test.testException2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property 'java::Test.testException:()V.1'
+--function Test.testException --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --property __CPROVER__start.1
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$

jbmc/regression/jbmc/exceptions28/test.desc

@@ -1,7 +1,7 @@
 CORE
 test
 --unwind 10
-^\[java::test.main:\(\[Ljava/lang/String;\)V\.1\] line 7 no uncaught exception: FAILURE$
+^\[__CPROVER__start\.1\] line 7 no uncaught exception: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/link_json_symtabs/test.desc

@@ -3,7 +3,7 @@ one.json_symtab
 two.json_symtab
 ^EXIT=0$
 ^SIGNAL=0$
-\[1\] file two.adb line [0-9]+ assertion: SUCCESS
+\[two\.1\] file two.adb line [0-9]+ assertion: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc/unique_labels1/bar.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(1 < 0);
+}
+
+void bar()
+{
+  foo();
+}

regression/cbmc/unique_labels1/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(0);
+}
+
+void bar();
+
+int main()
+{
+  foo();
+  bar();
+}

regression/cbmc/unique_labels1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+bar.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+assertion\.2
+--
+Each of the assertions in the two functions named "foo" should have a unique
+prefix, and thus be numbered "<prefix>.assertion.1."

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

@@ -1,8 +1,8 @@
 CORE dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
-^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc

@@ -1,34 +1,34 @@
 CORE
 main-enforce.c
 --dfcc main --enforce-contract foo
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
-^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_02/test.desc

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

regression/contracts-dfcc/assigns_enforce_15/test-baz.desc

@@ -1,7 +1,7 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract baz
-^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
+^\[baz_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_15/test-qux.desc

@@ -1,7 +1,7 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract qux
-^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
+^\[qux_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_18/test-bar.desc

@@ -1,7 +1,7 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract bar _ --pointer-primitive-check
-^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
+^\[bar_wrapped_for_contract_checking.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_18/test-baz.desc

@@ -2,7 +2,7 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract baz _ --pointer-primitive-check
 ^\[free.frees.\d+\].*Check that ptr is freeable: FAILURE
-^\[baz.assigns.\d+\].*Check that \*a is assignable: SUCCESS$
+^\[baz_wrapped_for_contract_checking.assigns.\d+\].*Check that \*a is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_18/test-foo.desc

@@ -1,8 +1,8 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo _ --pointer-primitive-check
-^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_19_a/test.desc

@@ -1,7 +1,7 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
-^\[f.assigns.\d+\] .* Check that a is assignable: SUCCESS$
+^\[f_wrapped_for_contract_checking.assigns.\d+\] .* Check that a is assignable: SUCCESS$
 ^\[f.postcondition.\d+\] .* Check ensures clause of contract contract::f for function f: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/contracts-dfcc/assigns_enforce_19_b/test.desc

@@ -1,10 +1,10 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f
-^\[f.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
-^\[f.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
-^\[f.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
-^\[f.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
+^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
+^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
+^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
+^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_20/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc

@@ -1,8 +1,8 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f1
-^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
-^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
+^\[f1_wrapped_for_contract_checking.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
+^\[f1_wrapped_for_contract_checking.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc

@@ -1,8 +1,8 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract f2
-^\[f2.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
-^\[f2.assigns.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
+^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
+^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc

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

regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc

@@ -2,12 +2,12 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo
-^\[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$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc

@@ -2,12 +2,12 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo
-^\[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$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc

@@ -2,12 +2,12 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 main.c function foo
-^\[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$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
+^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$