Skip to content

Commit 6a3d552

Browse files
committed
Fixed contracts regressions
1 parent 7656098 commit 6a3d552

File tree

46 files changed

+46
-46
lines changed

Some content is hidden

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

46 files changed

+46
-46
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
3+
--replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo _ --no-standard-checks
44
^\[bar.precondition.\d+\] line \d+ Check requires clause of bar in foo: SUCCESS$
55
^\[baz.precondition.\d+\] line \d+ Check requires clause of baz in foo: SUCCESS$
66
^EXIT=0$

regression/contracts/assigns_enforce_21/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract foo --replace-call-with-contract quz
3+
--enforce-contract foo --replace-call-with-contract quz _ --no-standard-checks
44
^\[foo.assigns.\d+\] line \d+ Check that \*y is valid: SUCCESS$
55
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
66
^\[bar.assigns.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE$

regression/contracts/assigns_enforce_arrays_02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract f1 --enforce-contract f2
3+
--enforce-contract f1 --enforce-contract f2 _ --no-standard-checks
44
^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$
55
^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$
66
^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$

regression/contracts/assigns_enforce_havoc_object/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract foo
3+
--enforce-contract foo _ --no-standard-checks
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$

regression/contracts/assigns_enforce_multi_file_02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract f1
3+
--enforce-contract f1 _ --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[f1.assigns.\d+\] line \d+ Check that \*a is valid: SUCCESS$

regression/contracts/assigns_enforce_scoping_02/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract f1
3+
--enforce-contract f1 _ --no-standard-checks
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[f1.assigns.\d+\] line \d+ Check that \*f1\$\$1\$\$1\$\$b is assignable: SUCCESS$

regression/contracts/assigns_enforce_statics/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract foo _ --pointer-primitive-check
3+
--enforce-contract foo _ --pointer-primitive-check --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo.assigns.\d+\] line \d+ Check that x is valid: SUCCESS$

regression/contracts/assigns_enforce_structs_06/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--enforce-contract f1 --enforce-contract f2 --enforce-contract f3
3+
--enforce-contract f1 --enforce-contract f2 --enforce-contract f3 _ --no-standard-checks
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$

regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main_enforce.c
3-
--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
3+
--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check --no-standard-checks
44
^VERIFICATION SUCCESSFUL$
55
^EXIT=0$
66
^SIGNAL=0$

regression/contracts/assigns_type_checking_valid_cases/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--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
3+
--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 --no-standard-checks
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[foo10.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$

0 commit comments

Comments
 (0)