Merge pull request #7127 from remi-delmas-3000/assigns-slice-loop-contracts

CONTRACTS: Support slice targets in loop assigns clauses

Author: tautschnig

regression/contracts-dfcc/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts-dfcc/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_side_effects_2/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_enforce_side_effects_3/test.desc

@@ -3,7 +3,7 @@ main.c
 --dfcc main --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts-dfcc/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 --
 Checks whether type checking rejects literal constants in assigns clause.

regression/contracts-dfcc/reject_history_expr_in_assigns_clause/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^main.c.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
+^.*error: assigns clause target must be a non-void lvalue or a call to a function returning void$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$