Align tests with is_fresh behaviour

Author: Remi Delmas

Diff for: regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc

@@ -2,16 +2,14 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
-^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
-^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: UNKNOWN$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

Diff for: regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_fail/test.desc

@@ -2,11 +2,11 @@ CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract foo
 ^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer NULL in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer invalid in \*x: UNKNOWN$
 ^\[bar.pointer_dereference.\d+\] line 10 dereference failure: deallocated dynamic object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 10 dereference failure: dead object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 10 dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 10 dereference failure: invalid integer address in \*x: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

Diff for: regression/contracts-dfcc/test_pointer_in_range_enforce_requires_disjunction_fail/test.desc

@@ -2,16 +2,14 @@ CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
 ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
-^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
-^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer NULL in \*y: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer invalid in \*y: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer invalid in \*y: UNKNOWN$
 ^\[foo.pointer_dereference.\d+\] line 8 dereference failure: deallocated dynamic object in \*y: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line 8 dereference failure: dead object in \*y: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*y: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 8 dereference failure: invalid integer address in \*y: FAILURE$
+^\[foo.pointer_dereference.\d+\] line 8 dereference failure: invalid integer address in \*y: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

Diff for: regression/contracts-dfcc/test_pointer_in_range_replace_ensures_disjunction_fail/test.desc

@@ -2,11 +2,11 @@ CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract foo
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: UNKNOWN$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: FAILURE$
 ^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: FAILURE$
+^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$