Skip to content

Commit fc24af0

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 d6c318e commit fc24af0

File tree

180 files changed

+615
-579
lines changed

Some content is hidden

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

180 files changed

+615
-579
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-dfcc/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
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
4-
^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
5-
^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
4+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
66
^EXIT=0$
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/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
--dfcc main --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+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
7+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$
8+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$
9+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$
10+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$
11+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$
12+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$
13+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$
14+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$
15+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$
16+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$
17+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$
18+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$
19+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$
20+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$
21+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
22+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
23+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
24+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
25+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
26+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
27+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
28+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
29+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
30+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
31+
^\[foo_wrapped_for_contract_checking.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
3232
^VERIFICATION FAILED$
3333
^EXIT=10$
3434
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_02/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract foo
4-
^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
4+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract baz
4-
^\[baz.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
4+
^\[baz_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
55
^VERIFICATION FAILED$
66
^EXIT=10$
77
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract qux
4-
^\[qux.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
4+
^\[qux_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that global is assignable: FAILURE$
55
^VERIFICATION FAILED$
66
^EXIT=10$
77
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract bar _ --pointer-primitive-check
4-
^\[bar.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
4+
^\[bar_wrapped_for_contract_checking.assigns.\d+\] line 20 Check that \*b is assignable: SUCCESS$
55
^VERIFICATION SUCCESSFUL$
66
^EXIT=0$
77
^SIGNAL=0$

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ CORE
22
main.c
33
--dfcc main --enforce-contract baz _ --pointer-primitive-check
44
^\[free.frees.\d+\].*Check that ptr is freeable: FAILURE
5-
^\[baz.assigns.\d+\].*Check that \*a is assignable: SUCCESS$
5+
^\[baz_wrapped_for_contract_checking.assigns.\d+\].*Check that \*a is assignable: SUCCESS$
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract foo _ --pointer-primitive-check
4-
^\[foo.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
5-
^\[foo.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
4+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*xp is assignable: SUCCESS$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 14 Check that y is assignable: FAILURE$
66
^VERIFICATION FAILED$
77
^EXIT=10$
88
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_19_a/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract f
4-
^\[f.assigns.\d+\] .* Check that a is assignable: SUCCESS$
4+
^\[f_wrapped_for_contract_checking.assigns.\d+\] .* Check that a is assignable: SUCCESS$
55
^\[f.postcondition.\d+\] .* Check ensures clause of contract contract::f for function f: SUCCESS$
66
^VERIFICATION SUCCESSFUL$
77
^EXIT=0$

‎regression/contracts-dfcc/assigns_enforce_19_b/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract f
4-
^\[f.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
5-
^\[f.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
6-
^\[f.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
7-
^\[f.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
4+
^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that b is assignable: SUCCESS$
5+
^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*points_to_b is assignable: SUCCESS$
6+
^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that c is assignable: FAILURE$
7+
^\[f_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that \*points_to_c is assignable: FAILURE$
88
^VERIFICATION FAILED$
99
^EXIT=10$
1010
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_20/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--dfcc main --enforce-contract foo
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[foo.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that x is assignable: FAILURE$
77
^VERIFICATION FAILED$
88
--
99
--

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

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

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
22
main.c
33
--dfcc main --enforce-contract f2
4-
^\[f2.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
5-
^\[f2.assigns.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
4+
^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
5+
^\[f2_wrapped_for_contract_checking.assigns.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
66
^EXIT=0$
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$

‎regression/contracts-dfcc/assigns_enforce_conditional_function_call_condition/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
^main.c function foo$
5-
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_conditional_lvalue/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
main.c function foo
5-
^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
7-
^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
8-
^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$
9-
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
10-
^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
7+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
8+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$
9+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
10+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_conditional_lvalue_list/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
main.c function foo
5-
^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$
7-
^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
8-
^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$
9-
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
10-
^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$
7+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
8+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$
9+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
10+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$

‎regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc

+6-6
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo
44
main.c function foo
5-
^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
6-
^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
7-
^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
8-
^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
9-
^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10-
^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
5+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
6+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
7+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
8+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
9+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10+
^\[foo_wrapped_for_contract_checking.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$

0 commit comments

Comments
 (0)