Skip to content

Commit 0a184c6

Browse files
author
Remi Delmas
committed
Update broken tests.
1 parent d78fe86 commit 0a184c6

File tree

9 files changed

+9
-13
lines changed

9 files changed

+9
-13
lines changed

regression/contracts/assigns_enforce_address_of/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
6+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
4+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
55
^CONVERSION ERROR
66
^EXIT=(1|64)$
77
^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
4+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
55
^CONVERSION ERROR
66
^EXIT=(1|64)$
77
^SIGNAL=0$

regression/contracts/assigns_enforce_function_calls/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
7-
^.*error: side-effects not allowed in assigns clause targets$
6+
^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$
87
^CONVERSION ERROR$
98
--
109
--

regression/contracts/assigns_enforce_literal/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
6+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_side_effects_1/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
activate-multi-line-match
5-
.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets\n.*\n.*error: side-effects not allowed in assigns clause targets\n.*\n.*error: ternary expressions not allowed in assigns clause targets\n)
4+
^.*error: void-typed expressions not allowed as assigns clause targets$
65
^CONVERSION ERROR$
76
^EXIT=(1|64)$
87
^SIGNAL=0$

regression/contracts/assigns_enforce_side_effects_2/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
7-
^.*error: side-effects not allowed in assigns clause targets$
6+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
87
^CONVERSION ERROR$
98
--
109
--

regression/contracts/assigns_enforce_side_effects_3/test.desc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
7-
^.*error: side-effects not allowed in assigns clause targets$
6+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
87
^CONVERSION ERROR$
98
--
109
--

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=(1|64)$
55
^SIGNAL=0$
66
^CONVERSION ERROR$
7-
^.*error: assigns clause target must be an lvalue or __CPROVER_POINTER_OBJECT expression$
7+
^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
88
--
99
Checks whether type checking rejects literal constants in assigns clause.

0 commit comments

Comments
 (0)