Merge pull request #8316 from diffblue/pointer-dereference-is-now-fatal

tautschnig · web-flow · commit 780b687a3628 · 2024-06-14T09:14:13.000+02:00
pointer checks are now fatal
diff --git a/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc b/regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc
@@ -1,6 +1,6 @@
 CORE
 pointer_subtraction.c
---no-signed-overflow-check --trace
+--no-signed-overflow-check --trace --no-pointer-check
 \[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
 \[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
 \[main\.assertion\.3\] line \d+ expected failure after pointer manipulation: FAILURE
diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc
@@ -1,6 +1,6 @@
 CORE
 pointers_assume.c
---trace
+--trace --no-pointer-check
 \[main\.assertion\.1\] line \d+ x == y: expected failure: FAILURE
 \[main\.assertion\.2\] line \d+ z >= x: expected successful: SUCCESS
 \[main\.assertion\.3\] line \d+ z <= y: expected successful: SUCCESS
diff --git a/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc b/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc
@@ -4,7 +4,7 @@ invalid_index_range.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS
+^\[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: UNKNOWN$
 line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
 --
 --
diff --git a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
@@ -4,8 +4,8 @@ smt_missing_range_check.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
-\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
+^\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: UNKNOWN$
+^\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$
 --
 --
 Check that memory checks fail for pointer dereferences inside an existential
diff --git a/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc b/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc
@@ -3,13 +3,13 @@ test_malloc_less_than_bound.c
 --no-malloc-may-fail --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
-\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+^\[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: UNKNOWN$
+^\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS$
+^\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE$
+^\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: UNKNOWN$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/cbmc/Function_Pointer18/test.desc b/regression/cbmc/Function_Pointer18/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
-
+--no-pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
 \[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
diff --git a/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---function foo
+--function foo --no-pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 4: SUCCESS$
 ^EXIT=10$
diff --git a/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc b/regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---function foo
+--function foo --no-pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) == 5: FAILURE$
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) >= 4: SUCCESS$
 ^EXIT=10$
diff --git a/regression/cbmc/array-cell-sensitivity10/test_execution.desc b/regression/cbmc/array-cell-sensitivity10/test_execution.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 16.*SUCCESS$
 ^\[main.assertion\.2\] line 17.*FAILURE$
diff --git a/regression/cbmc/array-cell-sensitivity3/test_execution.desc b/regression/cbmc/array-cell-sensitivity3/test_execution.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 9.*SUCCESS$
 ^\[main.assertion\.2\] line 10.*FAILURE$
diff --git a/regression/cbmc/array-cell-sensitivity7/test_execution.desc b/regression/cbmc/array-cell-sensitivity7/test_execution.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 10.*SUCCESS$
 ^\[main.assertion\.2\] line 11.*FAILURE$
diff --git a/regression/cbmc/array-cell-sensitivity8/test_execution.desc b/regression/cbmc/array-cell-sensitivity8/test_execution.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 11.*SUCCESS$
 ^\[main.assertion\.2\] line 12.*FAILURE$
diff --git a/regression/cbmc/byte_update14/test.desc b/regression/cbmc/byte_update14/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
-
+--no-pointer-check
 ^VERIFICATION FAILED$
 ^\[main.assertion\.1\] line 10.*SUCCESS$
 ^\[main.assertion\.2\] line 11.*FAILURE$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
@@ -6,7 +6,7 @@ main.c
 ^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$
 ^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$
 ^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$
-^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$
+^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: UNKNOWN$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-extra-checks/test.desc b/regression/cbmc/pointer-extra-checks/test.desc
@@ -4,10 +4,10 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.pointer_dereference.1\] .* dereference failure: pointer NULL in \*p: FAILURE$
-^\[main.pointer_dereference.2\] .* dereference failure: dead object in \*q: SUCCESS$
-^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: SUCCESS$
-^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: SUCCESS$
-^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
+^\[main.pointer_dereference.2\] .* dereference failure: dead object in \*q: UNKNOWN$
+^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: UNKNOWN$
+^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: UNKNOWN$
+^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: UNKNOWN$
 ^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$
 ^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
 ^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
diff --git a/regression/cbmc/ptr_arithmetic_on_null/test.desc b/regression/cbmc/ptr_arithmetic_on_null/test.desc
@@ -4,9 +4,9 @@ main.c
 ^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?1: SUCCESS$
 ^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - (\(.*\))?1: SUCCESS$
 ^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$
-^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: SUCCESS$
+^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: UNKNOWN$
 ^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == (\(.*\))?0: FAILURE$
-^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): SUCCESS$
+^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): UNKNOWN$
 ^\[main.assertion.7\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc/switch8/test.desc b/regression/cbmc/switch8/test.desc
@@ -8,7 +8,7 @@ main.c
 ^\[main\.pointer_dereference\.1\] line 36 dereference failure: dead object in \*p: SUCCESS$
 ^\[main\.pointer_dereference\.2\] line 36 dereference failure: pointer outside object bounds in \*p: SUCCESS$
 ^\[main\.assertion\.3\] line 42 assertion \*p == 42: FAILURE$
-^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: SUCCESS$
+^\[main\.pointer_dereference\.5\] line 42 dereference failure: pointer outside object bounds in \*p: UNKNOWN$
 ^\[main\.pointer_dereference\.3\] line 42 dereference failure: pointer NULL in \*p: SUCCESS$
 ^\[main\.pointer_dereference\.4\] line 42 dereference failure: dead object in \*p: FAILURE$
 ^\[main\.assertion\.4\] line 49 assertion e == 42: FAILURE$
diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc
@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[f2.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$
-^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$
+^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: UNKNOWN$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c b/regression/contracts-dfcc/assigns_replace_conditional_targets/main.c
@@ -1,4 +1,5 @@
 #include <stdbool.h>
+#include <stdlib.h>
 
 bool nz(int x)
 {
@@ -46,6 +47,9 @@ int main()
   old_y = y;
 
   char *z = malloc(1);
+  if(z == NULL)
+    return;
+
   *z = '0';
 
   foo(a, &x, &y, z);
diff --git a/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc b/regression/contracts-dfcc/assigns_replace_conditional_targets/test.desc
@@ -2,13 +2,13 @@ CORE
 main.c
 --dfcc main --replace-call-with-contract foo
 ^main.c function main$
-^\[main\.assertion\.\d+\] line 55 a unchanged, expecting SUCCESS: SUCCESS$
-^\[main\.assertion\.\d+\] line 57 x changed, expecting FAILURE: FAILURE$
-^\[main\.assertion\.\d+\] line 59 x unchanged, expecting SUCCESS: SUCCESS$
-^\[main\.assertion\.\d+\] line 62 y changed, expecting FAILURE: FAILURE$
-^\[main\.assertion\.\d+\] line 64 y unchanged, expecting SUCCESS: SUCCESS$
-^\[main\.assertion\.\d+\] line 67 z changed, expecting FAILURE: FAILURE$
-^\[main\.assertion\.\d+\] line 69 z unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 59 a unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 61 x changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 63 x unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 66 y changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 68 y unchanged, expecting SUCCESS: SUCCESS$
+^\[main\.assertion\.\d+\] line 71 z changed, expecting FAILURE: FAILURE$
+^\[main\.assertion\.\d+\] line 73 z unchanged, expecting SUCCESS: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/main.c b/regression/contracts-dfcc/invar_dynamic_struct_member/main.c
@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 typedef struct test
 {
   int x;
@@ -6,6 +8,8 @@ typedef struct test
 void main()
 {
   struct test *t = malloc(sizeof(test));
+  if(t == NULL)
+    return;
   t->x = 0;
 
   unsigned n;
diff --git a/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc b/regression/contracts-dfcc/invar_dynamic_struct_member/test.desc
@@ -3,14 +3,14 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 12 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 12 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 16 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 16 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 16 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 16 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$
-^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$
-^\[main.assertion.\d+\] line 29 assertion .*: FAILURE$
+^\[main.assigns.\d+\] line 26 Check that t->x is assignable: SUCCESS$
+^\[main.assigns.\d+\] line 29 Check that t->x is assignable: SUCCESS$
+^\[main.assertion.\d+\] line 33 assertion .*: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts-dfcc/loop_assigns-02/main.c b/regression/contracts-dfcc/loop_assigns-02/main.c
@@ -11,7 +11,11 @@ struct blob
 void main()
 {
   struct blob *b = malloc(sizeof(struct blob));
+  if(b == NULL)
+    return;
   b->data = malloc(SIZE);
+  if(b->data == NULL)
+    return;
 
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
diff --git a/regression/contracts-dfcc/loop_assigns-02/test.desc b/regression/contracts-dfcc/loop_assigns-02/test.desc
@@ -3,10 +3,10 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 17 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 17 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 17 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 17 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 21 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 21 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts-dfcc/loop_assigns-04/main.c b/regression/contracts-dfcc/loop_assigns-04/main.c
@@ -12,7 +12,11 @@ void main()
 {
   int y;
   struct blob *b = malloc(sizeof(struct blob));
+  if(b == NULL)
+    return;
   b->data = malloc(SIZE);
+  if(b->data == NULL)
+    return;
 
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
diff --git a/regression/contracts-dfcc/loop_assigns-04/test.desc b/regression/contracts-dfcc/loop_assigns-04/test.desc
@@ -3,14 +3,14 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 18 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 18 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 18 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 18 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+\] line 27 Check assigns clause inclusion for loop .*: FAILURE$
-^\[main.loop_invariant_base.\d+\] line 27 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 27 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 27 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 22 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 22 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 22 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 22 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 31 Check assigns clause inclusion for loop .*: FAILURE$
+^\[main.loop_invariant_base.\d+\] line 31 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 31 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 31 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc
@@ -7,10 +7,10 @@ main.c
 ^\[foo.assigns.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$
 ^\[foo.assigns.\d+\] line \d+ Check that \*p is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*q is assignable: UNKNOWN$
+^\[foo.assigns.\d+\] line \d+ Check that \*w is assignable: UNKNOWN$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: UNKNOWN$
+^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_POINTER_OBJECT\(\(void \*\)z\) is assignable: UNKNOWN$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc
@@ -3,11 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] line 22 Check that t->x is assignable: SUCCESS$
-^\[main.assigns.\d+\] line 25 Check that t->x is assignable: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: UNKNOWN$
+^\[main\.\d+\] .* Check that loop invariant is preserved: UNKNOWN$
+^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
+^\[main.assigns.\d+\] line 22 Check that t->x is assignable: UNKNOWN$
+^\[main.assigns.\d+\] line 25 Check that t->x is assignable: UNKNOWN$
 ^\[main.assertion.1\] .* assertion .*: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc
@@ -3,10 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: UNKNOWN$
+^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
 ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
-^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: UNKNOWN$
 ^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc
@@ -3,9 +3,9 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that j is assignable: SUCCESS$
-^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
+^\[main.assigns.\d+\] .* Check that j is assignable: UNKNOWN$
+^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: UNKNOWN$
 ^\[main.assigns.\d+\] .* Check that y is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc
@@ -3,7 +3,7 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.assigns.\d+\] .* Check that i is assignable: UNKNOWN$
 ^\[main.assigns.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/goto-instrument/generate-function-body-complex-struct/test.desc b/regression/goto-instrument/generate-function-body-complex-struct/test.desc
@@ -9,9 +9,9 @@ main.c
 \[main.assertion.4\] .* assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: SUCCESS
 \[main.assertion.5\] .* assertion main_struct.pointer_contents->struct_contents.some_variable == 11: FAILURE
 \[main.assertion.6\] .* assertion main_struct.struct_contents.some_variable == 10: FAILURE
-\[main.assertion.7\] .* assertion main_struct.struct_contents.some_constant == 20: SUCCESS
+\[main.assertion.7\] .* assertion main_struct.struct_contents.some_constant == 20: UNKNOWN
 \[main.assertion.8\] .* assertion main_struct.union_contents.some_double < 14.0 && main_struct.union_contents.some_double > 12.0: FAILURE
-\[main.assertion.9\] .* assertion child_struct.struct_contents.some_variable == 11: SUCCESS
-\[main.assertion.10\] .* assertion child_struct.union_contents.some_integer == 31: SUCCESS
-\[main.assertion.11\] .* assertion !child_struct.pointer_contents: SUCCESS
+\[main.assertion.9\] .* assertion child_struct.struct_contents.some_variable == 11: UNKNOWN
+\[main.assertion.10\] .* assertion child_struct.union_contents.some_integer == 31: UNKNOWN
+\[main.assertion.11\] .* assertion !child_struct.pointer_contents: UNKNOWN
 ^VERIFICATION FAILED$
diff --git a/regression/goto-instrument/nondet_static_exclude/test.desc b/regression/goto-instrument/nondet_static_exclude/test.desc
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
