Skip to content

Commit d774afe

Browse files
tautschnigtautschnig
committed
label_properties: do not rely on source_locationt's get_function()
A source location is a place in a text file, and the function information stored in there need not coincide with the name we use in the goto model. In this vein, label_properties should use the actual function name so that properties in different instantiations of a function (as may happen when linking static functions) get unique names.
1 parent d932d6f commit d774afe

File tree

102 files changed

+386
-354
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

102 files changed

+386
-354
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE symex-driven-lazy-loading-expected-failure
22
Test
3-
--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'
3+
--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
44
^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
55
^EXIT=10$
66
^SIGNAL=0$

‎jbmc/regression/jbmc/exceptions28/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
test
33
--unwind 10
4-
^\[java::test.main:\(\[Ljava/lang/String;\)V\.1\] line 7 no uncaught exception: FAILURE$
4+
^\[__CPROVER__start\.1\] line 7 no uncaught exception: FAILURE$
55
^VERIFICATION FAILED$
66
^EXIT=10$
77
^SIGNAL=0$

‎regression/cbmc/link_json_symtabs/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ one.json_symtab
33
two.json_symtab
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[1\] file two.adb line [0-9]+ assertion: SUCCESS
6+
\[two\.1\] file two.adb line [0-9]+ assertion: SUCCESS
77
^VERIFICATION SUCCESSFUL$
88
--
99
^warning: ignoring

‎regression/cbmc/unique_labels1/bar.c

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
static int foo()
4+
{
5+
assert(1 < 0);
6+
}
7+
8+
void bar()
9+
{
10+
foo();
11+
}

‎regression/cbmc/unique_labels1/main.c

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
static int foo()
4+
{
5+
assert(0);
6+
}
7+
8+
void bar();
9+
10+
int main()
11+
{
12+
foo();
13+
bar();
14+
}

‎regression/cbmc/unique_labels1/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
bar.c
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^warning: ignoring
9+
assertion\.2
10+
--
11+
Each of the assertions in the two functions named "foo" should have a unique
12+
prefix, and thus be numbered "<prefix>.assertion.1."

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--enforce-contract foo _ --malloc-may-fail --malloc-fail-null
4-
^\[foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$
5-
^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
66
^EXIT=0$
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
4-
^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
5-
^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
4+
^\[__CPROVER_contracts_original_foo.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
66
^EXIT=0$
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$

‎regression/contracts/assigns-replace-malloc-zero/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
4-
^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
4+
^\[main.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$
55
^EXIT=0$
66
^SIGNAL=0$
77
\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$

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

+28-28
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,34 @@
11
CORE
22
main-enforce.c
33
--enforce-contract foo
4-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
5-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
7-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
8-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
9-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
10-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
11-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
12-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
13-
^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
14-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
15-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
16-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
17-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
18-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
19-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
20-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
21-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
22-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
23-
^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
24-
^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
25-
^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
26-
^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
27-
^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
28-
^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
29-
^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
30-
^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
31-
^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
6+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
7+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
8+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
9+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
10+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
11+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
12+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
13+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
14+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
15+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
16+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
17+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
18+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
19+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
20+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
21+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
22+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
23+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
24+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
25+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
26+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
27+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
28+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
29+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
30+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
31+
^\[__CPROVER_contracts_original_foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
3232
^VERIFICATION FAILED$
3333
^EXIT=10$
3434
^SIGNAL=0$

‎regression/contracts/assigns_enforce_02/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
^\[foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$
5-
^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
66
^EXIT=10$
77
^SIGNAL=0$
88
^VERIFICATION FAILED$

‎regression/contracts/assigns_enforce_03/test.desc

+12-12
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
11
CORE
22
main.c
33
--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
4-
^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
5-
^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
6-
^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
7-
^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$
8-
^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$
9-
^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$
10-
^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$
11-
^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$
12-
^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$
13-
^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$
14-
^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$
15-
^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$
4+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
6+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
7+
^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$
8+
^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$
9+
^\[__CPROVER_contracts_original_f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$
10+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$
11+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$
12+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$
13+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$
14+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$
15+
^\[__CPROVER_contracts_original_f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$
1616
^VERIFICATION SUCCESSFUL$
1717
^EXIT=0$
1818
^SIGNAL=0$

‎regression/contracts/assigns_enforce_04/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
CORE
22
main.c
33
--enforce-contract f1
4-
^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
5-
^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
6-
^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
7-
^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$
8-
^\[f3.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$
9-
^\[f3.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$
4+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
6+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
7+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$
8+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$
9+
^\[__CPROVER_contracts_original_f1.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$
1010
^VERIFICATION SUCCESSFUL$
1111
^EXIT=0$
1212
^SIGNAL=0$

‎regression/contracts/assigns_enforce_15/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract foo --enforce-contract baz --enforce-contract qux
4-
^\[foo.assigns.\d+\] line \d+ Check that \*x is valid: SUCCESS$
5-
^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
6-
^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*x is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
6+
^\[__CPROVER_contracts_original_qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

‎regression/contracts/assigns_enforce_18/test.desc

+11-11
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,17 @@
11
CORE
22
main.c
33
--enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
4-
^\[foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$
5-
^\[foo.assigns.\d+\] line 11 Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
7-
^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
8-
^\[bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$
9-
^\[bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$
10-
^\[bar.assigns.\d+\] line 19 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
11-
^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
12-
^\[baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$
13-
^\[baz.assigns.\d+\] line 25 Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
14-
^\[baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 7 Check that \*xp is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 11 Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
6+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
7+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
8+
^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 17 Check that \*a is valid: SUCCESS$
9+
^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 17 Check that \*b is valid: SUCCESS$
10+
^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 19 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
11+
^\[__CPROVER_contracts_original_bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
12+
^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 23 Check that \*a is valid: SUCCESS$
13+
^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 25 Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
14+
^\[__CPROVER_contracts_original_baz.assigns.\d+\] line 26 Check that \*a is assignable: SUCCESS$
1515
^VERIFICATION FAILED$
1616
^EXIT=10$
1717
^SIGNAL=0$

‎regression/contracts/assigns_enforce_19/test.desc

+7-7
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
11
CORE
22
main.c
33
--enforce-contract f --enforce-contract g
4-
^\[f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$
5-
^\[f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$
6-
^\[g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$
7-
^\[g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
8-
^\[g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
9-
^\[g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
10-
^\[g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
4+
^\[__CPROVER_contracts_original_f.assigns.\d+\] line \d+ Check that a is assignable: SUCCESS$
5+
^\[__CPROVER_contracts_original_f.assigns.\d+\] line \d+ Check that aa is assignable: SUCCESS$
6+
^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that b is valid: SUCCESS$
7+
^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
8+
^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
9+
^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
10+
^\[__CPROVER_contracts_original_g.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$

‎regression/contracts/assigns_enforce_20/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--enforce-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
7-
^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
6+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
7+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
88
^VERIFICATION FAILED$
99
--
1010
--

‎regression/contracts/assigns_enforce_21/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract foo --replace-call-with-contract quz
4-
^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
5-
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
6-
^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$
4+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
5+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
6+
^\[__CPROVER_contracts_original_foo.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

0 commit comments

Comments
 (0)