diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception1.desc index 2164f8ee958..2d028162973 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception1.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception2.desc index 989931248aa..053d6f33c4b 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetCharAt/test_exception2.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetLength/test_exception.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetLength/test_exception.desc index 47c59753a8e..bfe48187dfa 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBufferSetLength/test_exception.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc index 2164f8ee958..2d028162973 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception1.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc index 989931248aa..053d6f33c4b 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetCharAt/test_exception2.desc +++ b/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$ diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc index 47c59753a8e..bfe48187dfa 100644 --- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderSetLength/test_exception.desc +++ b/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$ diff --git a/jbmc/regression/jbmc/exceptions28/test.desc b/jbmc/regression/jbmc/exceptions28/test.desc index 6909a80c595..f8bb999e0d6 100644 --- a/jbmc/regression/jbmc/exceptions28/test.desc +++ b/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$ diff --git a/regression/cbmc/link_json_symtabs/test.desc b/regression/cbmc/link_json_symtabs/test.desc index c5a0c306551..b9dddde5a8f 100644 --- a/regression/cbmc/link_json_symtabs/test.desc +++ b/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 diff --git a/regression/cbmc/unique_labels1/bar.c b/regression/cbmc/unique_labels1/bar.c new file mode 100644 index 00000000000..6f8d74c6062 --- /dev/null +++ b/regression/cbmc/unique_labels1/bar.c @@ -0,0 +1,11 @@ +#include + +static int foo() +{ + assert(1 < 0); +} + +void bar() +{ + foo(); +} diff --git a/regression/cbmc/unique_labels1/main.c b/regression/cbmc/unique_labels1/main.c new file mode 100644 index 00000000000..85c33c635b8 --- /dev/null +++ b/regression/cbmc/unique_labels1/main.c @@ -0,0 +1,14 @@ +#include + +static int foo() +{ + assert(0); +} + +void bar(); + +int main() +{ + foo(); + bar(); +} diff --git a/regression/cbmc/unique_labels1/test.desc b/regression/cbmc/unique_labels1/test.desc new file mode 100644 index 00000000000..cd854477093 --- /dev/null +++ b/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 ".assertion.1." diff --git a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc index db64e5e4568..528c2ef074a 100644 --- a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc b/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc index e1df873e83e..aa895d9be6b 100644 --- a/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_02/test.desc b/regression/contracts-dfcc/assigns_enforce_02/test.desc index 0df9cf4e3b1..1c76851024b 100644 --- a/regression/contracts-dfcc/assigns_enforce_02/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_15/test-baz.desc b/regression/contracts-dfcc/assigns_enforce_15/test-baz.desc index 5bc46c7fc8a..bdf1c00d750 100644 --- a/regression/contracts-dfcc/assigns_enforce_15/test-baz.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_15/test-qux.desc b/regression/contracts-dfcc/assigns_enforce_15/test-qux.desc index a53bd23a8fb..7e6eeb3ad3f 100644 --- a/regression/contracts-dfcc/assigns_enforce_15/test-qux.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_18/test-bar.desc b/regression/contracts-dfcc/assigns_enforce_18/test-bar.desc index f2a4c4de791..27aaa40f3a9 100644 --- a/regression/contracts-dfcc/assigns_enforce_18/test-bar.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_18/test-baz.desc b/regression/contracts-dfcc/assigns_enforce_18/test-baz.desc index 3585127b044..45ad702ddb0 100644 --- a/regression/contracts-dfcc/assigns_enforce_18/test-baz.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_18/test-foo.desc b/regression/contracts-dfcc/assigns_enforce_18/test-foo.desc index 111aff96e99..fa762096362 100644 --- a/regression/contracts-dfcc/assigns_enforce_18/test-foo.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_19_a/test.desc b/regression/contracts-dfcc/assigns_enforce_19_a/test.desc index a251f482d68..e01394cd327 100644 --- a/regression/contracts-dfcc/assigns_enforce_19_a/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_19_b/test.desc b/regression/contracts-dfcc/assigns_enforce_19_b/test.desc index efea0427e21..747665985de 100644 --- a/regression/contracts-dfcc/assigns_enforce_19_b/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_20/test.desc b/regression/contracts-dfcc/assigns_enforce_20/test.desc index e5527888b89..553a6df9125 100644 --- a/regression/contracts-dfcc/assigns_enforce_20/test.desc +++ b/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$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc index da5a5325a7b..53a150b8cef 100644 --- a/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f1.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc index 078391a2a99..f6b0e85712a 100644 --- a/regression/contracts-dfcc/assigns_enforce_arrays_02/test-f2.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc index edc907296f1..29859372964 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc index ab7bdfa3204..a86c3e12f39 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc index 4de6284e3c5..1d26c56771c 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc index d45cb3bddbf..f79693e653d 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc index 73812da891d..98c6c23d933 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_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 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$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_unions/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_unions/test.desc index e5417594b2a..6e5111d1ed5 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_unions/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_conditional_unions/test.desc @@ -3,11 +3,11 @@ main.c --dfcc main --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check ^\[is_high_level.assigns.\d+\] line 52 Check that latch is assignable: SUCCESS$ ^\[is_high_level.assigns.\d+\] line 53 Check that once is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 87 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 93 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ -^\[update.assigns.\d+\] line 98 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ -^\[update.assigns.\d+\] line 103 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ -^\[update.assigns.\d+\] line 107 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ +^\[update_wrapped_for_contract_checking.assigns.\d+\] line 87 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ +^\[update_wrapped_for_contract_checking.assigns.\d+\] line 93 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ +^\[update_wrapped_for_contract_checking.assigns.\d+\] line 98 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ +^\[update_wrapped_for_contract_checking.assigns.\d+\] line 103 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ +^\[update_wrapped_for_contract_checking.assigns.\d+\] line 107 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_free_dead/test.desc b/regression/contracts-dfcc/assigns_enforce_free_dead/test.desc index 314d1e38e1b..1e7053d8285 100644 --- a/regression/contracts-dfcc/assigns_enforce_free_dead/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_free_dead/test.desc @@ -1,10 +1,10 @@ CORE dfcc-only main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-primitive-check -^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 9 Check that \*\(\*y\) is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 21 Check that \*\(\*y\) is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 33 Check that \*x is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 9 Check that \*\(\*y\) is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 21 Check that \*\(\*y\) is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 33 Check that \*x is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc b/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc index d4cad6d9d72..ffa15b8a5f5 100644 --- a/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_malloc_01/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f\.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS +^\[f_wrapped_for_contract_checking\.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc b/regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc index 5bd4ad89152..89aac262eea 100644 --- a/regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_malloc_02/test.desc @@ -2,9 +2,9 @@ CORE dfcc-only main.c --dfcc main --enforce-contract f main.c function f -^\[f.assigns.\d+\] line 7 Check that ptr is assignable: SUCCESS$ -^\[f.assigns.\d+\] line 12 Check that \*ptr is assignable: SUCCESS$ -^\[f.assigns.\d+\] line 13 Check that n is assignable: SUCCESS$ +^\[f_wrapped_for_contract_checking.assigns.\d+\] line 7 Check that ptr is assignable: SUCCESS$ +^\[f_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that \*ptr is assignable: SUCCESS$ +^\[f_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that n is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc b/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc index 7914bd088d1..2a4d716f3bc 100644 --- a/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_malloc_03/test.desc @@ -1,8 +1,8 @@ CORE main.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].* Check that \*loc1 is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that \*loc2 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that \*loc1 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that \*loc2 is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc b/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc index ce6b1e21ea3..f00ea706f3f 100644 --- a/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo _ --pointer-check -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ +^\[foo_wrapped_for_contract_checking.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/assigns_enforce_scoping_01/test.desc b/regression/contracts-dfcc/assigns_enforce_scoping_01/test.desc index ebb6bf0bd8b..d9f3718d5bf 100644 --- a/regression/contracts-dfcc/assigns_enforce_scoping_01/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_scoping_01/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_scoping_02/test.desc b/regression/contracts-dfcc/assigns_enforce_scoping_02/test.desc index 3e1b0214cd7..6b3364341fc 100644 --- a/regression/contracts-dfcc/assigns_enforce_scoping_02/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_scoping_02/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_statics/test.desc b/regression/contracts-dfcc/assigns_enforce_statics/test.desc index 8f0e543b508..56399ec5b17 100644 --- a/regression/contracts-dfcc/assigns_enforce_statics/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_statics/test.desc @@ -1,9 +1,9 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo _ --pointer-primitive-check -^\[foo.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: FAILURE$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*y is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc index 171bb04eb34..7ca04b9081c 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_01/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^\[.*assigns.*\].*: FAILURE$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc index 6d1aceb2d75..6dbad87e464 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_02/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f ^EXIT=0$ ^SIGNAL=0$ -^\[f.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ +^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*a is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^\[.*assigns.*\].*: FAILURE$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f1.desc index d1e16803068..0f1527baa5d 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f1.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f2.desc index e17e81712f6..0d5dd01561a 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f2.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f2 ^EXIT=10$ ^SIGNAL=0$ -^\[f2.assigns.\d+\] line \d+ Check that p->x is assignable: FAILURE$ +^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f3.desc b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f3.desc index dda2ff022b0..b18a383fe19 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_04/test-f3.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_04/test-f3.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f3 ^EXIT=0$ ^SIGNAL=0$ -^\[f3.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[f3_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc index fbb81d3f3c3..4d0f832ff7c 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc @@ -3,10 +3,10 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc index a0ca61df0c3..094dd4e698c 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc @@ -3,10 +3,10 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc index 6a58247dbd4..dedcc501f73 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract f2 ^EXIT=10$ ^SIGNAL=0$ -^\[f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc index 65ec69add21..fda891bbd04 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f3.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract f3 ^EXIT=0$ ^SIGNAL=0$ -^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ -^\[f3.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[f3_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ +^\[f3_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc index 48ee2f48940..84643b14dfc 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc @@ -3,7 +3,7 @@ main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f1 _ --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc index a0ebcd86895..a8a842464e8 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc @@ -3,7 +3,7 @@ main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f2 _ --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2_wrapped_for_contract_checking.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc index ae4d709b2fe..66e746b3d5f 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract f1 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc index 81632e6070c..d939b0a3b4d 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_function_pointer/test.desc b/regression/contracts-dfcc/assigns_function_pointer/test.desc index 29064487bef..f0d5f9e395a 100644 --- a/regression/contracts-dfcc/assigns_function_pointer/test.desc +++ b/regression/contracts-dfcc/assigns_function_pointer/test.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract bar ^EXIT=0$ ^SIGNAL=0$ -^\[bar.assigns.\d+\] line \d+ Check that s->f is assignable: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that \*f is assignable: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that s->f is assignable: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*f is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion x \=\= 2: SUCCESS$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo10.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo10.desc index 8ce9577b01a..7713b41b323 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo10.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo10.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract foo10 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo10.assigns.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ +^\[foo10_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo10_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo3.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo3.desc index 7b0a33af003..5e14b70021c 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo3.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo3.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract foo3 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo3.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[foo3_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo4.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo4.desc index 3600c6a2592..62bd00d9b65 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo4.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo4.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract foo4 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo4.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ -^\[foo4.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo4_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ +^\[foo4_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo6.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo6.desc index 69d6770068c..40a5faaed1d 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo6.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo6.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract foo6 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo6.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo6.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo6_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo6_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo7.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo7.desc index 42df1f71ac6..3887e7b040e 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo7.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo7.desc @@ -3,8 +3,8 @@ main.c --dfcc main --enforce-contract foo7 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo7.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[foo7_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[foo7_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc index 21d30e188ac..23e1df5bf2f 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc @@ -3,16 +3,16 @@ main.c --dfcc main --enforce-contract foo8 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ +^\[foo8_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/assigns_validity_pointer_02/test.desc b/regression/contracts-dfcc/assigns_validity_pointer_02/test.desc index 7729123b8a8..a0aaa7ba3cf 100644 --- a/regression/contracts-dfcc/assigns_validity_pointer_02/test.desc +++ b/regression/contracts-dfcc/assigns_validity_pointer_02/test.desc @@ -7,7 +7,7 @@ main.c ^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^\[baz.assigns.\d+\] line \d+ Check that \*z is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/contracts_with_function_pointers/test.desc b/regression/contracts-dfcc/contracts_with_function_pointers/test.desc index a62fcad01a9..7ecb491a8ae 100644 --- a/regression/contracts-dfcc/contracts_with_function_pointers/test.desc +++ b/regression/contracts-dfcc/contracts_with_function_pointers/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[bar.postcondition.\d+\].*Check ensures clause of contract contract::bar for function bar: SUCCESS$ -^\[bar.assigns.\d+\].*Check that \*return\_value\_baz is assignable: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assigns.\d+\].*Check that \*return\_value\_baz is assignable: SUCCESS$ ^\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts-dfcc/havoc-static/test-exclude.desc b/regression/contracts-dfcc/havoc-static/test-exclude.desc index f4136a5f8b9..ae7a384982d 100644 --- a/regression/contracts-dfcc/havoc-static/test-exclude.desc +++ b/regression/contracts-dfcc/havoc-static/test-exclude.desc @@ -1,9 +1,9 @@ CORE main.c --dfcc main --enforce-contract foo --nondet-static-exclude main.c:a --nondet-static-exclude main.c:c -^\[foo.assertion.\d+\].* guarded by a: SUCCESS$ -^\[foo.assertion.\d+\].* guarded by b: SUCCESS$ -^\[foo.assertion.\d+\].* guarded by c: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by a: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by b: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by c: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/havoc-static/test.desc b/regression/contracts-dfcc/havoc-static/test.desc index af0f8a3cb16..0bce3dbd414 100644 --- a/regression/contracts-dfcc/havoc-static/test.desc +++ b/regression/contracts-dfcc/havoc-static/test.desc @@ -1,9 +1,9 @@ CORE main.c --dfcc main --enforce-contract foo -^\[foo.assertion.\d+\].* guarded by a: FAILURE$ -^\[foo.assertion.\d+\].* guarded by b: SUCCESS$ -^\[foo.assertion.\d+\].* guarded by c: FAILURE$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by a: FAILURE$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by b: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].* guarded by c: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/history-pointer-enforce-09/test.desc b/regression/contracts-dfcc/history-pointer-enforce-09/test.desc index f3756a86a59..45949ba3a98 100644 --- a/regression/contracts-dfcc/history-pointer-enforce-09/test.desc +++ b/regression/contracts-dfcc/history-pointer-enforce-09/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/history-pointer-enforce-10/test-bar.desc b/regression/contracts-dfcc/history-pointer-enforce-10/test-bar.desc index ceb94cfdf62..3d7ba3ac3bf 100644 --- a/regression/contracts-dfcc/history-pointer-enforce-10/test-bar.desc +++ b/regression/contracts-dfcc/history-pointer-enforce-10/test-bar.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[bar.postcondition.\d+\] line \d+ Check ensures clause of contract contract::bar for function bar: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that p->y 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-dfcc/history-pointer-enforce-10/test-foo.desc b/regression/contracts-dfcc/history-pointer-enforce-10/test-foo.desc index 3b8c84b0557..1b6b624fb25 100644 --- a/regression/contracts-dfcc/history-pointer-enforce-10/test-foo.desc +++ b/regression/contracts-dfcc/history-pointer-enforce-10/test-foo.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\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-dfcc/loop-freeness-check/test.desc b/regression/contracts-dfcc/loop-freeness-check/test.desc index ef93e2830c9..5c91e1908ec 100644 --- a/regression/contracts-dfcc/loop-freeness-check/test.desc +++ b/regression/contracts-dfcc/loop-freeness-check/test.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$ -^\[foo.assigns.\d+\].*Check that arr\[\(.*\)i\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that i is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that arr\[\(.*\)i\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc index 173445e6b92..aabb8962cb5 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc @@ -5,12 +5,12 @@ main_bounded.c ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ -^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc index 7c20dc70831..858710848db 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc @@ -5,12 +5,12 @@ main.c ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ -^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc index 9788d6bae1a..50657d4aa99 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc @@ -4,12 +4,12 @@ main_bounded.c ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ -^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc index 59e873628b6..d46523823ee 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check -^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$ -^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$ +^\[__CPROVER_contracts_write_set_insert_object_from.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: FAILURE$ ^\*\* 2 of \d+ failed ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc index 1f0bb2c9e7e..88e184d9526 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc @@ -4,12 +4,12 @@ main_bounded.c ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ -^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc index 2325a4ab7ff..391b8582082 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc @@ -4,12 +4,12 @@ main.c ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ -^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\] line \d+ size is capped: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ +^\[foo_wrapped_for_contract_checking.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc b/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc index d26b261e946..174a2d28cd2 100644 --- a/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc +++ b/regression/contracts-dfcc/quantifiers-exists-both-replace/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --replace-call-with-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ +^\[main.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/contracts-dfcc/quantifiers-exists-requires-replace/test.desc b/regression/contracts-dfcc/quantifiers-exists-requires-replace/test.desc index 96d1ffc6191..4c20d794075 100644 --- a/regression/contracts-dfcc/quantifiers-exists-requires-replace/test.desc +++ b/regression/contracts-dfcc/quantifiers-exists-requires-replace/test.desc @@ -3,8 +3,8 @@ main.c --dfcc main --replace-call-with-contract f1 --replace-call-with-contract f2 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ -^\[f2.precondition.\d+\] line \d+ Check requires clause of (contract contract::f2 for function f2|f2 in main): FAILURE$ +^\[main.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ +^\[main.precondition.\d+\] line \d+ Check requires clause of (contract contract::f2 for function f2|f2 in main): FAILURE$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc b/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc index 21981c6325e..b08159a42e6 100644 --- a/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc +++ b/regression/contracts-dfcc/quantifiers-forall-both-replace/test.desc @@ -3,7 +3,7 @@ main.c --dfcc main --replace-call-with-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ +^\[main.precondition.\d+\] line \d+ Check requires clause of (contract contract::f1 for function f1|f1 in main): SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc index 8458deb6fd9..ade49225ac3 100644 --- a/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ +^\[f1_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/contracts-dfcc/test_aliasing_enforce/test.desc b/regression/contracts-dfcc/test_aliasing_enforce/test.desc index e8fc5123fe6..d640dd22cf7 100644 --- a/regression/contracts-dfcc/test_aliasing_enforce/test.desc +++ b/regression/contracts-dfcc/test_aliasing_enforce/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause of contract contract::foo for function foo: SUCCESS$ -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts-dfcc/test_aliasing_ensure/test.desc b/regression/contracts-dfcc/test_aliasing_ensure/test.desc index 27a7b7d5a2c..eb1a9b424b2 100644 --- a/regression/contracts-dfcc/test_aliasing_ensure/test.desc +++ b/regression/contracts-dfcc/test_aliasing_ensure/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ -\[foo.assigns.\d+\].*Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\].*Check that \*y is assignable: SUCCESS -\[foo.assigns.\d+\].*Check that z is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*x is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*y is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that z is assignable: SUCCESS \[main.assertion.\d+\].*assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-bar.desc b/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-bar.desc index e5306b7a57a..944264070cf 100644 --- a/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-bar.desc +++ b/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-bar.desc @@ -2,9 +2,9 @@ CORE dfcc-only main_bar.c --dfcc main --enforce-contract bar ^\[bar.postcondition.\d+\].*Check ensures clause of contract contract::bar for function bar: SUCCESS$ -^\[bar.assertion.\d+\].*x is r_ok: SUCCESS$ -^\[bar.assigns.\d+\].*Check that \*x is assignable: SUCCESS$ -^\[bar.assertion.\d+\].*deref x is r_ok: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assertion.\d+\].*x is r_ok: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assigns.\d+\].*Check that \*x is assignable: SUCCESS$ +^\[bar_wrapped_for_contract_checking.assertion.\d+\].*deref x is r_ok: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-foo.desc b/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-foo.desc index d6126990dcd..ecedd26d0f9 100644 --- a/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-foo.desc +++ b/regression/contracts-dfcc/test_aliasing_ensure_indirect/test-foo.desc @@ -2,11 +2,11 @@ CORE dfcc-only main_foo.c --dfcc main --enforce-contract foo --replace-call-with-contract bar ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ -^\[foo.assertion.\d+\].*x1 r_ok: SUCCESS$ -^\[foo.assertion.\d+\].*x2 r_ok: SUCCESS$ -^\[foo.assertion.\d+\].*deref x2 r_ok: SUCCESS$ -^\[foo.assertion.\d+\].*deref x2 r_ok: SUCCESS$ -^\[foo.assertion.\d+\].*x2 updated: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*x1 r_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*x2 r_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*deref x2 r_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*deref x2 r_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*x2 updated: SUCCESS$ ^\[bar.precondition.\d+\].*Check requires clause of contract contract::bar for function bar: SUCCESS$ ^\[bar.assigns.\d+\].*Check that the assigns clause of contract::bar is included in the caller's assigns clause: SUCCESS$ ^\[bar.frees.\d+\].*Check that the frees clause of contract::bar is included in the caller's frees clause: SUCCESS$ diff --git a/regression/contracts-dfcc/test_array_memory_enforce/test.desc b/regression/contracts-dfcc/test_array_memory_enforce/test.desc index 3ed2e82468f..bd8de796df5 100644 --- a/regression/contracts-dfcc/test_array_memory_enforce/test.desc +++ b/regression/contracts-dfcc/test_array_memory_enforce/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_ensures/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_ensures/test.desc index 7cc4c7a4a21..3f9322fb262 100644 --- a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_ensures/test.desc +++ b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_ensures/test.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].*Check that \*out1 is assignable: SUCCESS$ -^\[foo.assigns.\d+\].*Check that \*out2 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out1 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out2 is assignable: SUCCESS$ ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_requires/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_requires/test.desc index d4b08e244fd..80a133492c6 100644 --- a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_requires/test.desc +++ b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_separation_against_requires/test.desc @@ -1,9 +1,9 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assertion.\d+\].*in1 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in2 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in2 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_size/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_size/test.desc index 427486e620a..7716bb1e5a7 100644 --- a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_size/test.desc +++ b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_fail_size/test.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].*Check that \*out is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out is assignable: SUCCESS$ ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_pass/test.desc index b886f1f2a20..d97fea3e5ab 100644 --- a/regression/contracts-dfcc/test_is_fresh_enforce_ensures_pass/test.desc +++ b/regression/contracts-dfcc/test_is_fresh_enforce_ensures_pass/test.desc @@ -2,11 +2,11 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ -^\[foo.assertion.\d+\].*in1 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in2 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ -^\[foo.assigns.\d+\].*Check that \*out1 is assignable: SUCCESS$ -^\[foo.assigns.\d+\].*Check that \*out2 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in2 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out1 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out2 is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_pass/test.desc index 892c333cd03..71db2aba57f 100644 --- a/regression/contracts-dfcc/test_is_fresh_enforce_requires_pass/test.desc +++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_pass/test.desc @@ -1,11 +1,11 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assertion.\d+\].*in1 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in2 is rw_ok: SUCCESS$ -^\[foo.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ -^\[foo.assertion.\d+\].*in1 is zero: SUCCESS$ -^\[foo.assertion.\d+\].*in2 is zero: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in2 is rw_ok: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 and in2 do not alias: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in1 is zero: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assertion.\d+\].*in2 is zero: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_pass/test-enforce.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_pass/test-enforce.desc index 19936ff0231..263207b4e29 100644 --- a/regression/contracts-dfcc/test_is_fresh_replace_ensures_pass/test-enforce.desc +++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_pass/test-enforce.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].*Check that \*out_ptr1 is assignable: SUCCESS$ -^\[foo.assigns.\d+\].*Check that \*out_ptr2 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out_ptr1 is assignable: SUCCESS$ +^\[foo_wrapped_for_contract_checking.assigns.\d+\].*Check that \*out_ptr2 is assignable: SUCCESS$ ^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ ^\[main.assertion.\d+\].*out1 is rw_ok: SUCCESS$ ^\[main.assertion.\d+\].*out2 is rw_ok: SUCCESS$ diff --git a/regression/contracts-dfcc/test_scalar_memory_enforce/test.desc b/regression/contracts-dfcc/test_scalar_memory_enforce/test.desc index ad6e7372ed5..c82df337bf2 100644 --- a/regression/contracts-dfcc/test_scalar_memory_enforce/test.desc +++ b/regression/contracts-dfcc/test_scalar_memory_enforce/test.desc @@ -2,7 +2,7 @@ CORE main.c --dfcc main --enforce-contract foo \[foo.postcondition.\d+\].*Check ensures clause( of contract contract::foo for function foo)?: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/test_struct_enforce/test.desc b/regression/contracts-dfcc/test_struct_enforce/test.desc index 5551d67dbbf..cebf3fb3ee7 100644 --- a/regression/contracts-dfcc/test_struct_enforce/test.desc +++ b/regression/contracts-dfcc/test_struct_enforce/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$ -\[foo.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that x->qux is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that x->baz is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\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-dfcc/test_struct_member_enforce/test.desc b/regression/contracts-dfcc/test_struct_member_enforce/test.desc index 5c1636b03be..ec9277d5a29 100644 --- a/regression/contracts-dfcc/test_struct_member_enforce/test.desc +++ b/regression/contracts-dfcc/test_struct_member_enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$ -\[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS +\[foo_wrapped_for_contract_checking.assigns.\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-dfcc/typed_target_pointer/test.desc b/regression/contracts-dfcc/typed_target_pointer/test.desc index 10f4d922ccb..631eb4be02b 100644 --- a/regression/contracts-dfcc/typed_target_pointer/test.desc +++ b/regression/contracts-dfcc/typed_target_pointer/test.desc @@ -1,8 +1,8 @@ CORE main.c --enforce-contract foo -^\[foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&x, .*, TRUE\) is valid: SUCCESS$ -^\[foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&\(\*y\), .*, FALSE\) is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&x, .*, TRUE\) is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&\(\*y\), .*, FALSE\) is valid: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc index 43dcf8ef277..25e4bd6c390 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc @@ -1,8 +1,8 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null -^\[foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$ -^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc index be3c595b24e..35547c4f3c5 100644 --- a/regression/contracts/assigns-replace-ignored-return-value/test.desc +++ b/regression/contracts/assigns-replace-ignored-return-value/test.desc @@ -1,8 +1,8 @@ CORE main.c --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo -^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$ -^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$ +^\[__CPROVER_contracts_original_foo.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$ +^\[__CPROVER_contracts_original_foo.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns-replace-malloc-zero/test.desc b/regression/contracts/assigns-replace-malloc-zero/test.desc index 3aed45563ee..991f8b3a9a0 100644 --- a/regression/contracts/assigns-replace-malloc-zero/test.desc +++ b/regression/contracts/assigns-replace-malloc-zero/test.desc @@ -1,7 +1,7 @@ CORE main.c --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null -^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$ +^\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc index 2abca0b8bd1..5ca77523d22 100644 --- a/regression/contracts/assigns_enforce_02/test.desc +++ b/regression/contracts/assigns_enforce_02/test.desc @@ -1,8 +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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc index 4b342024cc9..ee19f225223 100644 --- a/regression/contracts/assigns_enforce_03/test.desc +++ b/regression/contracts/assigns_enforce_03/test.desc @@ -1,18 +1,18 @@ 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$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc index 35a898dd382..9fbaae37777 100644 --- a/regression/contracts/assigns_enforce_04/test.desc +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -1,12 +1,12 @@ 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$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_15/test.desc b/regression/contracts/assigns_enforce_15/test.desc index 82ce16cb582..bddc3baec9d 100644 --- a/regression/contracts/assigns_enforce_15/test.desc +++ b/regression/contracts/assigns_enforce_15/test.desc @@ -1,9 +1,9 @@ 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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is valid: SUCCESS$ +^\[__CPROVER_contracts_original_baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$ +^\[__CPROVER_contracts_original_qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc index 09560eaedd6..0b131c347cd 100644 --- a/regression/contracts/assigns_enforce_18/test.desc +++ b/regression/contracts/assigns_enforce_18/test.desc @@ -1,17 +1,17 @@ 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 __CPROVER_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 __CPROVER_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 __CPROVER_POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ -^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 11 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 19 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$ +^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 25 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_19/test.desc b/regression/contracts/assigns_enforce_19/test.desc index c003078d31c..5b400c119d5 100644 --- a/regression/contracts/assigns_enforce_19/test.desc +++ b/regression/contracts/assigns_enforce_19/test.desc @@ -1,13 +1,13 @@ CORE main.c --enforce-contract f --enforce-contract g -^\[f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$ -^\[f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$ -^\[g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$ -^\[g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$ -^\[g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$ -^\[g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$ -^\[g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$ +^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$ +^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_20/test.desc b/regression/contracts/assigns_enforce_20/test.desc index 440e688a534..c88945233b8 100644 --- a/regression/contracts/assigns_enforce_20/test.desc +++ b/regression/contracts/assigns_enforce_20/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc index f27b7f42c59..6a485824698 100644 --- a/regression/contracts/assigns_enforce_21/test.desc +++ b/regression/contracts/assigns_enforce_21/test.desc @@ -1,9 +1,9 @@ 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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc index e8150f13152..680570d1ef7 100644 --- a/regression/contracts/assigns_enforce_arrays_02/test.desc +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -1,13 +1,13 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 -^\[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 __CPROVER_object_whole\(\(.* \*\)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 __CPROVER_POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 12 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 16 Check that __CPROVER_POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 54d643ef138..88b64106267 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,8 +1,8 @@ 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$ +^\[__CPROVER_contracts_original_uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[\(.*int\)i\]\) is valid: SUCCESS$ +^\[__CPROVER_contracts_original_uses_assigns.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc index 2106dd933e3..49289d33524 100644 --- a/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc +++ b/regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc @@ -2,9 +2,9 @@ CORE main.c --enforce-contract foo ^main.c function foo$ -^\[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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 10 Check that \*x is valid when .*: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_lvalue/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc index 999be3227c8..023c19a5baf 100644 --- a/regression/contracts/assigns_enforce_conditional_lvalue/test.desc +++ b/regression/contracts/assigns_enforce_conditional_lvalue/test.desc @@ -2,14 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that \*y is valid when !\(a != FALSE\): SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc index 9e01d79ca12..3591b173e0f 100644 --- a/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc @@ -2,14 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that \*y is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc index 59513d2907f..73e265217d8 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc @@ -2,14 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.* \*\)x\) is valid when a != FALSE: SUCCESS$ -^\[foo.assigns.\d+\] line 7 Check that __CPROVER_object_whole\(\(.* \*\)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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.* \*\)x\) is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that __CPROVER_object_whole\(\(.* \*\)y\) is valid when !\(a != FALSE\): SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc index 954c6a0cc92..481af0c264b 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc @@ -2,14 +2,14 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)x\) is valid when a != FALSE: SUCCESS$ -^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)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$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)x\) is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)y\) is valid when a != FALSE: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_unions/test.desc b/regression/contracts/assigns_enforce_conditional_unions/test.desc index 04637c10efe..6e4aaa127fb 100644 --- a/regression/contracts/assigns_enforce_conditional_unions/test.desc +++ b/regression/contracts/assigns_enforce_conditional_unions/test.desc @@ -1,22 +1,22 @@ CORE main.c --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check -^\[update.assigns.\d+] line 73 Check that __CPROVER_object_whole\(\(.*\)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 __CPROVER_object_whole\(\(.*\)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 __CPROVER_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 __CPROVER_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 __CPROVER_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 __CPROVER_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 __CPROVER_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$ +^\[__CPROVER_contracts_original_update.assigns.\d+] line 73 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS +^\[__CPROVER_contracts_original_update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS +^\[__CPROVER_contracts_original_update.assigns.\d+] line 76 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS +^\[__CPROVER_contracts_original_update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 84 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 90 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 95 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 100 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 104 Check that __CPROVER_POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_detect_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_local_statics/test.desc index 363b231dc52..428a47e6584 100644 --- a/regression/contracts/assigns_enforce_detect_local_statics/test.desc +++ b/regression/contracts/assigns_enforce_detect_local_statics/test.desc @@ -1,9 +1,9 @@ CORE main.c --enforce-contract bar -^\[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$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 17 Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 20 Check that \*yy is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc index df0a24af87e..d43eece41ce 100644 --- a/regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc +++ b/regression/contracts/assigns_enforce_detect_replaced_local_statics/test.desc @@ -1,8 +1,8 @@ CORE main.c --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --pointer-check -^\[foo.assigns.\d+\] line \d+ Check that __local_static \(assigned by the contract of bar\) is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that __local_static_arr \(assigned by the contract of bar\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __local_static \(assigned by the contract of bar\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __local_static_arr \(assigned by the contract of bar\) is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$ ^\[main.assertion.\d+\] line \d+ expecting FAILURE: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc index 3bc041ab15c..2aa23d41767 100644 --- a/regression/contracts/assigns_enforce_free_dead/test.desc +++ b/regression/contracts/assigns_enforce_free_dead/test.desc @@ -1,25 +1,25 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check -\[foo.assigns.\d+\] line 4 Check that \*x is valid: SUCCESS$ -\[foo.assigns.\d+\] line 4 Check that \*p is valid when .*: SUCCESS$ -\[foo.assigns.\d+\] line 4 Check that \*\(\*p\) is valid when .*: SUCCESS$ -^\[foo.assigns.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 4 Check that \*x is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 4 Check that \*p is valid when .*: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 4 Check that \*\(\*p\) is valid when .*: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*p is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*p is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*q is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*w is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$ -- Checks that invalidated CARs are correctly tracked on `free` and `DEAD`. diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc index 2563aafae1a..c3ec9939912 100644 --- a/regression/contracts/assigns_enforce_havoc_object/test.desc +++ b/regression/contracts/assigns_enforce_havoc_object/test.desc @@ -3,9 +3,9 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc index c9f45d47c58..308852d8a0a 100644 --- a/regression/contracts/assigns_enforce_multi_file_02/test.desc +++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract f1 ^EXIT=0$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that b->y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that b->y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/assigns_enforce_offsets_2/test.desc b/regression/contracts/assigns_enforce_offsets_2/test.desc index dbf3b1e0810..254cc87625f 100644 --- a/regression/contracts/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts/assigns_enforce_offsets_2/test.desc @@ -1,9 +1,9 @@ CORE main.c --enforce-contract foo _ --pointer-check -^\[foo.assigns.*\d+\].* line 5 Check that \*x is valid: SUCCESS$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.*\d+\].* line 5 Check that \*x is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ +^\[__CPROVER_contracts_original_foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_offsets_4/test.desc b/regression/contracts/assigns_enforce_offsets_4/test.desc index a9144122d51..c2437bf9fe4 100644 --- a/regression/contracts/assigns_enforce_offsets_4/test.desc +++ b/regression/contracts/assigns_enforce_offsets_4/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo _ --pointer-check -^\[foo.assigns.*\d+\].* line 5 Check that x\[\(.*\)10\] is valid: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.*\d+\].* line 5 Check that x\[\(.*\)10\] is valid: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc index d95afefade3..61b04706fce 100644 --- a/regression/contracts/assigns_enforce_scoping_01/test.desc +++ b/regression/contracts/assigns_enforce_scoping_01/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc index a5d07aa04d5..de6f6d98b25 100644 --- a/regression/contracts/assigns_enforce_scoping_02/test.desc +++ b/regression/contracts/assigns_enforce_scoping_02/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that \*b is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc index 87f417d025f..1180b249202 100644 --- a/regression/contracts/assigns_enforce_statics/test.desc +++ b/regression/contracts/assigns_enforce_statics/test.desc @@ -3,9 +3,9 @@ main.c --enforce-contract foo _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^\[.*assigns.*\].*: FAILURE$ diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc index 003a6fd2f4a..7b520edfc9e 100644 --- a/regression/contracts/assigns_enforce_structs_04/test.desc +++ b/regression/contracts/assigns_enforce_structs_04/test.desc @@ -3,9 +3,9 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 --enforce-contract f4 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->x is assignable: FAILURE$ -^\[f3.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line \d+ Check that p->x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line \d+ Check that p->y 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 index 2a56bf89725..adbcd2101ce 100644 --- 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-contract f1 --enforce-contract f2 --enforce-contract f3 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ -^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ -^\[f3.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f3.assigns.\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 index c7337935f6b..cb0dd7842d6 100644 --- 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-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\].*line 16 Check that \*p->buf is valid: FAILURE$ -^\[f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ -^\[f2.assigns.\d+\].*line 21 Check that \*pp->p->buf is valid: FAILURE$ -^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\].*line 16 Check that \*p->buf is valid: FAILURE$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\].*line 21 Check that \*pp->p->buf is valid: FAILURE$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_08/test.desc b/regression/contracts/assigns_enforce_structs_08/test.desc index 054a165460b..4054b110ae5 100644 --- a/regression/contracts/assigns_enforce_structs_08/test.desc +++ b/regression/contracts/assigns_enforce_structs_08/test.desc @@ -1,8 +1,8 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc index ed4c35002f3..68957c2c1fa 100644 --- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc +++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc @@ -4,13 +4,13 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^main.c function baz$ -^\[baz.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$ -^\[baz.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$ ^main.c function foo$ -^\[foo.assertion.\d+\] line 20 foo.x.set: SUCCESS$ -^\[foo.assertion.\d+\] line 25 foo.local.set: SUCCESS$ -^\[foo.assertion.\d+\] line 29 foo.y.set: SUCCESS$ -^\[foo.assertion.\d+\] line 33 foo.z.set: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assertion.\d+\] line 20 foo.x.set: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assertion.\d+\] line 25 foo.local.set: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assertion.\d+\] line 29 foo.y.set: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assertion.\d+\] line 33 foo.z.set: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_replace_08/test.desc b/regression/contracts/assigns_replace_08/test.desc index 1e029090ff0..d9deaec4916 100644 --- a/regression/contracts/assigns_replace_08/test.desc +++ b/regression/contracts/assigns_replace_08/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check ^EXIT=10$ ^SIGNAL=0$ -\[foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$ +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$ ^.* 1 of \d+ failed \(\d+ iteration.*\)$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/assigns_replace_09/test.desc b/regression/contracts/assigns_replace_09/test.desc index 535ca9a1f05..4d5b13e53f7 100644 --- a/regression/contracts/assigns_replace_09/test.desc +++ b/regression/contracts/assigns_replace_09/test.desc @@ -3,8 +3,8 @@ main.c --replace-call-with-contract bar --enforce-contract foo ^EXIT=0$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that \*z is valid: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*z is valid: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^Condition: \!not\_found$ diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index 588301c9ead..2d5f4f5d920 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -3,25 +3,25 @@ main.c --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo10.assigns.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ -^\[foo3.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ -^\[foo4.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ -^\[foo4.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ -^\[foo6.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo6.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ -^\[foo7.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo10.assigns.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo3.assigns.\d+\] line \d+ Check that y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo4.assigns.\d+\] line \d+ Check that \*c is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo4.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo6.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo6.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo7.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts/contracts_with_function_pointers/test.desc b/regression/contracts/contracts_with_function_pointers/test.desc index 1520b8dba51..6e612fd261a 100644 --- a/regression/contracts/contracts_with_function_pointers/test.desc +++ b/regression/contracts/contracts_with_function_pointers/test.desc @@ -4,8 +4,8 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line \d+ Check that \*return\_value\_baz is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC properly instrument functions with function pointers diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc index 6ab7a0823ef..f2374945034 100644 --- a/regression/contracts/history-pointer-enforce-10/test.desc +++ b/regression/contracts/history-pointer-enforce-10/test.desc @@ -6,9 +6,9 @@ main.c ^\[bar.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ ^\[baz.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ ^\[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ -^\[bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_bar.assigns.\d+\] line \d+ Check that p->y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_foo.assigns.\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-replace-04/test.desc b/regression/contracts/history-pointer-replace-04/test.desc index c4458b4a9bf..8e19772b146 100644 --- a/regression/contracts/history-pointer-replace-04/test.desc +++ b/regression/contracts/history-pointer-replace-04/test.desc @@ -3,7 +3,7 @@ main.c --replace-call-with-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$ +^\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion p->y \!\= 7: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts/loop_assigns-05/test.desc b/regression/contracts/loop_assigns-05/test.desc index 0dc2ffedc89..890bf99c99b 100644 --- a/regression/contracts/loop_assigns-05/test.desc +++ b/regression/contracts/loop_assigns-05/test.desc @@ -3,10 +3,10 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ -^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ diff --git a/regression/contracts/loop_assigns_inference-01/test.desc b/regression/contracts/loop_assigns_inference-01/test.desc index 11da15c0fcf..27ae86a92fe 100644 --- a/regression/contracts/loop_assigns_inference-01/test.desc +++ b/regression/contracts/loop_assigns_inference-01/test.desc @@ -3,10 +3,10 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ -^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ diff --git a/regression/contracts/loop_assigns_scoped_local_statics/test.desc b/regression/contracts/loop_assigns_scoped_local_statics/test.desc index 761d2f6fe27..92555f86b8d 100644 --- a/regression/contracts/loop_assigns_scoped_local_statics/test.desc +++ b/regression/contracts/loop_assigns_scoped_local_statics/test.desc @@ -3,20 +3,20 @@ main.c --apply-loop-contracts ^EXIT=0$ ^SIGNAL=0$ -^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$ -^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ -^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$ -^\[body_1.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ -^\[body_2.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ -^\[body_3.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ -^\[incr.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion before_loop\(\) == 0: SUCCESS$ ^\[main.assertion.\d+\] line \d+ assertion after_loop\(\) == 0: SUCCESS$ -^\[upperbound.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ +^\[main.assigns.\d+\] line \d+ Check that __static_local is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts/loop_guard_with_side_effects/test.desc b/regression/contracts/loop_guard_with_side_effects/test.desc index e1c9d00edb1..aef0af12065 100644 --- a/regression/contracts/loop_guard_with_side_effects/test.desc +++ b/regression/contracts/loop_guard_with_side_effects/test.desc @@ -1,7 +1,7 @@ CORE main.c --apply-loop-contracts _ --unsigned-overflow-check -\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$ +\[main.assigns\.\d+\] line \d+ Check that \*j is assignable: SUCCESS$ \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS \[check.overflow\.\d+\] line \d+ arithmetic overflow on unsigned \+ in \*j \+ 1u: SUCCESS \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ diff --git a/regression/contracts/loop_guard_with_side_effects_fail/test.desc b/regression/contracts/loop_guard_with_side_effects_fail/test.desc index 0d753f4ad57..85efe6ed9c2 100644 --- a/regression/contracts/loop_guard_with_side_effects_fail/test.desc +++ b/regression/contracts/loop_guard_with_side_effects_fail/test.desc @@ -1,7 +1,7 @@ CORE main.c --apply-loop-contracts _ --unsigned-overflow-check -\[check.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$ +\[main.assigns\.\d+\] line \d+ Check that \*j is assignable: FAILURE$ \[main\.\d+\] line \d+ Check loop invariant before entry: SUCCESS$ \[main\.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$ \[main.assigns\.\d+\] line \d+ Check that i is assignable: SUCCESS$ diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index ebd37152ecf..446a6576ca8 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ +^\[__CPROVER_contracts_original_f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/contracts/test_aliasing_enforce/test.desc b/regression/contracts/test_aliasing_enforce/test.desc index f26bda8c1f1..7d956fa1ab7 100644 --- a/regression/contracts/test_aliasing_enforce/test.desc +++ b/regression/contracts/test_aliasing_enforce/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_aliasing_ensure/test.desc b/regression/contracts/test_aliasing_ensure/test.desc index 70ae1bdd9ff..0bcfd564083 100644 --- a/regression/contracts/test_aliasing_ensure/test.desc +++ b/regression/contracts/test_aliasing_ensure/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that z is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc index 226a5d2aebb..16711bfb23c 100644 --- a/regression/contracts/test_aliasing_ensure_indirect/test.desc +++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS +\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/test_array_memory_replace/test.desc b/regression/contracts/test_array_memory_replace/test.desc index b6c5d13435b..228a0042137 100644 --- a/regression/contracts/test_array_memory_replace/test.desc +++ b/regression/contracts/test_array_memory_replace/test.desc @@ -3,7 +3,7 @@ main.c --replace-call-with-contract foo ^EXIT=0$ ^SIGNAL=0$ -\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS +\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: 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 index fb30f3ebf7c..bc0249779ef 100644 --- a/regression/contracts/test_array_memory_too_small_replace/test.desc +++ b/regression/contracts/test_array_memory_too_small_replace/test.desc @@ -3,7 +3,7 @@ main.c --replace-call-with-contract foo ^EXIT=10$ ^SIGNAL=0$ -\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE +\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: FAILURE \[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 index 941d4f8c249..6d367157f68 100644 --- a/regression/contracts/test_scalar_memory_replace/test.desc +++ b/regression/contracts/test_scalar_memory_replace/test.desc @@ -3,7 +3,7 @@ main.c --replace-call-with-contract foo ^EXIT=0$ ^SIGNAL=0$ -\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS +\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: 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 ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc index 213f347ed88..629e1efb37a 100644 --- a/regression/contracts/variant_multidimensional_ackermann/test.desc +++ b/regression/contracts/variant_multidimensional_ackermann/test.desc @@ -1,7 +1,7 @@ CORE main.c --apply-loop-contracts --replace-call-with-contract ackermann -^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in main: SUCCESS$ +^\[main.precondition\.\d+\] line \d+ Check requires clause of ackermann in main: SUCCESS$ ^\[ackermann.precondition\.\d+\] line \d+ Check requires clause of ackermann in ackermann: SUCCESS$ ^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$ ^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$ diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc index dcd33598351..cbde80b9529 100644 --- a/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*p\[.*0\] == 10: SUCCESS -\[main.assertion.2\] .*p\[.*1\] == 20: SUCCESS -\[main.assertion.3\] .*q\[.*0\] == 100: SUCCESS -\[main.assertion.4\] .*q\[.*99\] == 101: SUCCESS +\[main.assertion.\d+\] .*p\[.*0\] == 10: SUCCESS +\[main.assertion.\d+\] .*p\[.*1\] == 20: SUCCESS +\[main.assertion.\d+\] .*q\[.*0\] == 100: SUCCESS +\[main.assertion.\d+\] .*q\[.*99\] == 101: SUCCESS -- diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc index 474b957707e..d9bffb3f1b0 100644 --- a/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*p\[.*0\] == 10: UNKNOWN -\[main.assertion.2\] .*p\[.*1\] == 20: UNKNOWN -\[main.assertion.3\] .*q\[.*0\] == 100: UNKNOWN -\[main.assertion.4\] .*q\[.*99\] == 101: UNKNOWN +\[main.assertion.\d+\] .*p\[.*0\] == 10: UNKNOWN +\[main.assertion.\d+\] .*p\[.*1\] == 20: UNKNOWN +\[main.assertion.\d+\] .*q\[.*0\] == 100: UNKNOWN +\[main.assertion.\d+\] .*q\[.*99\] == 101: UNKNOWN -- diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc index 91687849c60..012bd459930 100644 --- a/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers value-set --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*p\[.*0\] == 10: SUCCESS -\[main.assertion.2\] .*p\[.*1\] == 20: SUCCESS -\[main.assertion.3\] .*q\[.*0\] == 100: SUCCESS -\[main.assertion.4\] .*q\[.*99\] == 101: SUCCESS +\[main.assertion.\d+\] .*p\[.*0\] == 10: SUCCESS +\[main.assertion.\d+\] .*p\[.*1\] == 20: SUCCESS +\[main.assertion.\d+\] .*q\[.*0\] == 100: SUCCESS +\[main.assertion.\d+\] .*q\[.*99\] == 101: SUCCESS -- diff --git a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc index 0aaca9a8b72..8bdadd70304 100644 --- a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*alias == 99: SUCCESS -\[main.assertion.2\] .*alias == 100: SUCCESS -\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: SUCCESS -\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS +\[main.assertion.\d+\] .*alias == 99: SUCCESS +\[main.assertion.\d+\] .*alias == 100: SUCCESS +\[main.assertion.\d+\] .*i_was_malloced\[.*0\] == 101: SUCCESS +\[main.assertion.\d+\] .*alias\[.*1\] == 102: SUCCESS -- diff --git a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc index 8aa9ea66315..af099e2e276 100644 --- a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*alias == 99: UNKNOWN -\[main.assertion.2\] .*alias == 100: UNKNOWN -\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: UNKNOWN -\[main.assertion.4\] .*alias\[.*1\] == 102: UNKNOWN +\[main.assertion.\d+\] .*alias == 99: UNKNOWN +\[main.assertion.\d+\] .*alias == 100: UNKNOWN +\[main.assertion.\d+\] .*i_was_malloced\[.*0\] == 101: UNKNOWN +\[main.assertion.\d+\] .*alias\[.*1\] == 102: UNKNOWN -- diff --git a/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc index 9d7320b2dc0..59fc539a44b 100644 --- a/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc +++ b/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-pointers value-set --vsd-arrays every-element --verify ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] .*alias == 99: SUCCESS -\[main.assertion.2\] .*alias == 100: SUCCESS -\[main.assertion.3\] .*i_was_malloced\[.*0\] == 101: SUCCESS -\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS +\[main.assertion.\d+\] .*alias == 99: SUCCESS +\[main.assertion.\d+\] .*alias == 100: SUCCESS +\[main.assertion.\d+\] .*i_was_malloced\[.*0\] == 101: SUCCESS +\[main.assertion.\d+\] .*alias\[.*1\] == 102: SUCCESS -- diff --git a/regression/symtab2gb/multiple_symtabs/test.desc b/regression/symtab2gb/multiple_symtabs/test.desc index 8e91b64c60d..9ec1b3ecbb2 100644 --- a/regression/symtab2gb/multiple_symtabs/test.desc +++ b/regression/symtab2gb/multiple_symtabs/test.desc @@ -3,8 +3,8 @@ entry_point.json_symtab user.json_symtab library.json_symtab ^EXIT=10$ ^SIGNAL=0$ -^\[1\] file library.adb line \d+ assertion: FAILURE$ -^\[2\] file library.adb line \d+ assertion: FAILURE$ +^\[library\.1\] file library.adb line \d+ assertion: FAILURE$ +^\[library\.2\] file library.adb line \d+ assertion: FAILURE$ ^VERIFICATION FAILED$ -- error diff --git a/regression/symtab2gb/single_symtab/test.desc b/regression/symtab2gb/single_symtab/test.desc index 317003031f5..cb25d7ec064 100644 --- a/regression/symtab2gb/single_symtab/test.desc +++ b/regression/symtab2gb/single_symtab/test.desc @@ -3,8 +3,8 @@ entry_point.json_symtab ^EXIT=10$ ^SIGNAL=0$ -^\[1\] file entry_point.adb line \d+ assertion: FAILURE$ -^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$ +^\[entry_point\.1\] file entry_point.adb line \d+ assertion: FAILURE$ +^\[entry_point\.2\] file entry_point.adb line \d+ assertion: SUCCESS$ ^VERIFICATION FAILED$ -- error diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp index 46f092774b4..9b270b097c5 100644 --- a/src/goto-instrument/aggressive_slicer.cpp +++ b/src/goto-instrument/aggressive_slicer.cpp @@ -100,7 +100,7 @@ void aggressive_slicert::doit() auto property_loc = find_property(p, goto_model.goto_functions); if(!property_loc.has_value()) throw "unable to find property in call graph"; - note_functions_to_keep(property_loc.value().get_function()); + note_functions_to_keep(property_loc->first); } // Add functions within distance of shortest path functions diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index 49a5d18dfbe..7136165d5ec 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -67,13 +67,12 @@ void label_properties( it->source_location_nonconst().set_function(function_identifier); } - irep_idt function = it->source_location().get_function(); + PRECONDITION(!function_identifier.empty()); + std::string prefix = id2string(function_identifier); - std::string prefix=id2string(function); if(!it->source_location().get_property_class().empty()) { - if(!prefix.empty()) - prefix+="."; + prefix += "."; std::string class_infix = id2string(it->source_location().get_property_class()); @@ -84,8 +83,7 @@ void label_properties( prefix+=class_infix; } - if(!prefix.empty()) - prefix+="."; + prefix += "."; std::size_t &count=property_counters[prefix]; diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 90be11961c2..91c21e9698c 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -19,9 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" -optionalt find_property( - const irep_idt &property, - const goto_functionst & goto_functions) +optionalt> +find_property(const irep_idt &property, const goto_functionst &goto_functions) { for(const auto &fct : goto_functions.function_map) { @@ -33,7 +32,7 @@ optionalt find_property( { if(ins.source_location().get_property_id() == property) { - return ins.source_location(); + return std::make_pair(fct.first, ins.source_location()); } } } diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index afb99a4ba06..9b4ef077008 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -45,11 +45,14 @@ void show_properties( /// \param property: irep_idt that identifies property /// \param goto_functions: program in which to search for /// the property -/// \return optional the location of the -/// property, if found. -optionalt find_property( - const irep_idt &property, - const goto_functionst &goto_functions); +/// \return A pair of function identifier and source location, where the +/// function identifier is that of the GOTO function that contains the ASSERT +/// instruction labelled by \p property, if any such property label exists. +/// The source location is that of the ASSERT instruction matching the +/// property. The function identifier and source location's function attribute +/// are not necessarily equal. +optionalt> +find_property(const irep_idt &property, const goto_functionst &goto_functions); /// \brief Collects the properties in the goto program into a `json_arrayt` /// \param json_properties: JSON array to hold the properties diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index bcfa6c0f191..ba2e416771c 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -940,8 +940,7 @@ void goto_symext::loop_bound_exceeded( { // Generate VCC for unwinding assertion. const std::string property_id = - id2string(state.source.pc->source_location().get_function()) + - ".unwind." + loop_number; + id2string(state.source.function_id) + ".unwind." + loop_number; vcc( negated_cond, property_id,