Skip to content

Commit 3bbd3ab

Browse files
remi-delmas-3000remi-delmas-3000
authored
Merge pull request #6575 from remi-delmas-3000/assigns-clause-checking-cleanup
CONTRACTS: New class `instrument_spec_assignst` encapsulating assigns clause checking logic.
2 parents f2240be + 63d03bc commit 3bbd3ab

File tree

109 files changed

+1551
-1377
lines changed

Some content is hidden

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

109 files changed

+1551
-1377
lines changed

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
main.c
33
--enforce-contract foo _ --malloc-may-fail --malloc-fail-null
4+
^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
5+
^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
46
^EXIT=0$
57
^SIGNAL=0$
6-
^\[foo\.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS
78
^VERIFICATION SUCCESSFUL$
89
--
910
This test checks that objects of size zero or __CPROVER_max_malloc_size

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
8-
^[.*] Check that .*ignored_return_value.* is assignable: FAILURE
8+
^\[.*assigns.*\].*ignored_return_value.*FAILURE
99
--
1010
This test checks that when replacing a call by a contract for a call that
1111
ignores the return value of the function, the temporary introduced to

‎regression/contracts/assigns_enforce_02/test.desc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +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$
46
^EXIT=10$
57
^SIGNAL=0$
68
^VERIFICATION FAILED$

‎regression/contracts/assigns_enforce_03/test.desc

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,21 @@
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$
16+
^VERIFICATION SUCCESSFUL$
417
^EXIT=0$
518
^SIGNAL=0$
6-
^VERIFICATION SUCCESSFUL$
719
--
820
--
921
This test checks that verification succeeds when assigns clauses are respected through multiple function calls.

‎regression/contracts/assigns_enforce_04/test.desc

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,15 @@
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$
10+
^VERIFICATION SUCCESSFUL$
411
^EXIT=0$
512
^SIGNAL=0$
6-
^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
7-
^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
8-
^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$
9-
^VERIFICATION SUCCESSFUL$
1013
--
1114
--
1215
This test checks that verification only considers assigns clause from enforced function.

‎regression/contracts/assigns_enforce_15/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
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$
7+
^VERIFICATION FAILED$
48
^EXIT=10$
59
^SIGNAL=0$
6-
^\[baz.\d+\] line \d+ Check that global is assignable: FAILURE$
7-
^\[qux.\d+\] line \d+ Check that global is assignable: FAILURE$
8-
^VERIFICATION FAILED$
910
--
1011
--
1112
Checks whether verification fails when enforcing a contract

‎regression/contracts/assigns_enforce_18/test.desc

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,20 @@
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$
15+
^VERIFICATION FAILED$
416
^EXIT=10$
517
^SIGNAL=0$
6-
^\[bar.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
7-
^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
8-
^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
9-
^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
10-
^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
11-
^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
12-
^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
13-
^VERIFICATION FAILED$
1418
--
1519
--
1620
Checks whether contract enforcement works with functions that deallocate memory.

‎regression/contracts/assigns_enforce_19/test.desc

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,15 @@
11
CORE
22
main.c
33
--enforce-contract f --enforce-contract g
4+
^\[f.assigns.\d+\] line 9 Check that a is assignable: SUCCESS$
5+
^\[g.assigns.\d+\] line 14 Check that b is valid: SUCCESS$
6+
^\[g.assigns.\d+\] line 16 Check that b is assignable: SUCCESS$
7+
^\[g.assigns.\d+\] line 17 Check that c is assignable: FAILURE$
8+
^\[g.assigns.\d+\] line 18 Check that \*points_to_b is assignable: SUCCESS$
9+
^\[g.assigns.\d+\] line 19 Check that \*points_to_c is assignable: FAILURE$
10+
^VERIFICATION FAILED$
411
^EXIT=10$
512
^SIGNAL=0$
6-
^\[f.\d+\] line \d+ Check that a is assignable: SUCCESS$
7-
^\[g.\d+\] line \d+ Check that b is assignable: SUCCESS$
8-
^\[g.\d+\] line \d+ Check that c is assignable: FAILURE$
9-
^\[g.\d+\] line \d+ Check that \*points\_to\_b is assignable: SUCCESS$
10-
^\[g.\d+\] line \d+ Check that \*points\_to\_c is assignable: FAILURE$
11-
^VERIFICATION FAILED$
1213
--
1314
--
1415
Checks whether contract enforcement works with (local and global) static variables.

‎regression/contracts/assigns_enforce_20/test.desc

Lines changed: 2 additions & 2 deletions
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.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
7-
^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
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$
88
^VERIFICATION FAILED$
99
--
1010
--

‎regression/contracts/assigns_enforce_21/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
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$
7+
^VERIFICATION FAILED$
48
^EXIT=10$
59
^SIGNAL=0$
6-
main.c function bar
7-
^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
8-
^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE
9-
^VERIFICATION FAILED$
1010
--
1111
--
1212
Checks whether checks write set for sub-function calls.

‎regression/contracts/assigns_enforce_arrays_02/test.desc

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
CORE
22
main.c
33
--enforce-contract f1 --enforce-contract f2
4-
^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
5-
^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$
6-
^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
7-
^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
8-
^\[f2.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
4+
^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
5+
^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
6+
^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$
7+
^\[f2.assigns.\d+\] line 12 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid: SUCCESS$
8+
^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$
9+
^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$
10+
^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$
911
^EXIT=10$
1012
^SIGNAL=0$
1113
^VERIFICATION FAILED$

‎regression/contracts/assigns_enforce_arrays_05/test.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
CORE
22
main.c
33
--enforce-contract uses_assigns
4+
^\[uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[\(.*int\)i\]\) is valid: SUCCESS$
5+
^\[assigns_ptr.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
6+
^VERIFICATION SUCCESSFUL$
47
^EXIT=0$
58
^SIGNAL=0$
6-
^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
7-
^VERIFICATION SUCCESSFUL$
89
--
910
--
1011
Checks whether verification succeeds for array elements at a symbolic index.

‎regression/contracts/assigns_enforce_conditional_function_call_condition/test.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@ CORE
22
main.c
33
--enforce-contract foo
44
^main.c function foo$
5-
^\[foo\.\d+\] line 16 Check that \*x is assignable: SUCCESS$
6-
^\[foo\.\d+\] line 20 Check that \*x is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line 10 Check that \*x is valid when .*: SUCCESS$
6+
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: SUCCESS$
7+
^\[foo.assigns.\d+\] line 20 Check that \*x is assignable: FAILURE$
78
^VERIFICATION FAILED$
89
^EXIT=10$
910
^SIGNAL=0$

‎regression/contracts/assigns_enforce_conditional_lvalue/test.desc

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@ CORE
22
main.c
33
--enforce-contract foo
44
main.c function foo
5-
^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6-
^\[foo\.\d+\] line 8 Check that \*y is assignable: FAILURE$
7-
^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
8-
^\[foo\.\d+\] line 13 Check that \*y is assignable: SUCCESS$
9-
^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
10-
^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$
6+
^\[foo.assigns.\d+\] line 3 Check that \*y is valid when !\(a != FALSE\): SUCCESS$
7+
^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
8+
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
9+
^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
10+
^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: SUCCESS$
11+
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
12+
^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
1113
^VERIFICATION FAILED$
1214
^EXIT=10$
1315
^SIGNAL=0$

‎regression/contracts/assigns_enforce_conditional_lvalue_list/test.desc

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@ CORE
22
main.c
33
--enforce-contract foo
44
main.c function foo
5-
^\[foo\.\d+\] line 7 Check that \*x is assignable: SUCCESS$
6-
^\[foo\.\d+\] line 8 Check that \*y is assignable: SUCCESS$
7-
^\[foo\.\d+\] line 12 Check that \*x is assignable: FAILURE$
8-
^\[foo\.\d+\] line 13 Check that \*y is assignable: FAILURE$
9-
^\[foo\.\d+\] line 16 Check that \*x is assignable: FAILURE$
10-
^\[foo\.\d+\] line 17 Check that \*y is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line 3 Check that \*x is valid when a != FALSE: SUCCESS$
6+
^\[foo.assigns.\d+\] line 3 Check that \*y is valid when a != FALSE: SUCCESS$
7+
^\[foo.assigns.\d+\] line 7 Check that \*x is assignable: SUCCESS$
8+
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: SUCCESS$
9+
^\[foo.assigns.\d+\] line 12 Check that \*x is assignable: FAILURE$
10+
^\[foo.assigns.\d+\] line 13 Check that \*y is assignable: FAILURE$
11+
^\[foo.assigns.\d+\] line 16 Check that \*x is assignable: FAILURE$
12+
^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: FAILURE$
1113
^VERIFICATION FAILED$
1214
^EXIT=10$
1315
^SIGNAL=0$

‎regression/contracts/assigns_enforce_conditional_pointer_object/test.desc

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,14 @@ CORE
22
main.c
33
--enforce-contract foo
44
main.c function foo
5-
^\[foo\.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
6-
^\[foo\.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
7-
^\[foo\.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
8-
^\[foo\.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
9-
^\[foo\.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10-
^\[foo\.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
6+
^\[foo.assigns.\d+\] line 7 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when !\(a != FALSE\): SUCCESS$
7+
^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
8+
^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
9+
^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10+
^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
11+
^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
12+
^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
1113
^VERIFICATION FAILED$
1214
^EXIT=10$
1315
^SIGNAL=0$

‎regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,17 @@ CORE
22
main.c
33
--enforce-contract foo
44
main.c function foo
5-
^\[foo\.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
6-
^\[foo\.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
7-
^\[foo\.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
8-
^\[foo\.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
9-
^\[foo\.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10-
^\[foo\.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
5+
^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$
6+
^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when a != FALSE: SUCCESS$
7+
^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
8+
^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$
9+
^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
10+
^\[foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
11+
^\[foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$
12+
^\[foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$
1113
^VERIFICATION FAILED$
1214
^EXIT=10$
1315
^SIGNAL=0$
1416
--
1517
--
16-
Check that conditional assigns clause `c ? {__CPROVER_POINTER_OBJECT((p), .. }`
17-
match with control flow path conditions.
18+
Check that conditional target groups match with control flow path conditions.

‎regression/contracts/assigns_enforce_conditional_unions/test.desc

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,22 @@
11
CORE
22
main.c
33
--enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check
4-
^\[is_high_level.\d+\] line 50 Check that latch is assignable: SUCCESS$
5-
^\[is_high_level.\d+\] line 51 Check that once is assignable: SUCCESS$
6-
^\[update.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
7-
^\[update.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
8-
^\[update.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
9-
^\[update.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
10-
^\[update.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
11-
^\[update.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
12-
^\[update.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
13-
^\[update.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
14-
^\[update.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
15-
^\[update.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
4+
^\[update.assigns.\d+] line 73 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS
5+
^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS
6+
^\[update.assigns.\d+] line 76 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS
7+
^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS
8+
^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$
9+
^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$
10+
^\[update.assigns.\d+\] line 84 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: SUCCESS$
11+
^\[update.assigns.\d+\] line 85 Check that state->digest.high_level.first.ctx->flags is assignable: SUCCESS$
12+
^\[update.assigns.\d+\] line 90 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: SUCCESS$
13+
^\[update.assigns.\d+\] line 91 Check that state->digest.high_level.second.ctx->flags is assignable: SUCCESS$
14+
^\[update.assigns.\d+\] line 95 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
15+
^\[update.assigns.\d+\] line 96 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
16+
^\[update.assigns.\d+\] line 100 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.first.ctx->digest\) is assignable: FAILURE$
17+
^\[update.assigns.\d+\] line 101 Check that state->digest.high_level.first.ctx->flags is assignable: FAILURE$
18+
^\[update.assigns.\d+\] line 104 Check that POINTER_OBJECT\(\(void \*\)state->digest.high_level.second.ctx->digest\) is assignable: FAILURE$
19+
^\[update.assigns.\d+\] line 105 Check that state->digest.high_level.second.ctx->flags is assignable: FAILURE$
1620
^VERIFICATION FAILED$
1721
^EXIT=10$
1822
^SIGNAL=0$

‎regression/contracts/assigns_enforce_detect_local_statics/test.desc

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
CORE
22
main.c
33
--enforce-contract bar
4-
^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS
5-
^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS
6-
^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE
4+
^\[foo.assigns.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS$
5+
^\[foo.assigns.\d+\] line 17 Check that \*y is assignable: SUCCESS$
6+
^\[foo.assigns.\d+\] line 20 Check that \*yy is assignable: FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

0 commit comments

Comments
 (0)