malloc MAY fail cbmc/primitives

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -1,6 +1,6 @@
 CORE smt-backend no-new-smt
 smt_missing_range_check.c
---pointer-check -z3
+--no-malloc-may-fail --pointer-check -z3
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 valid_index_range.c
---pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/forall_6231_1/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test.c
---pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS

regression/cbmc-primitives/forall_6231_2/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test.c
---pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS

regression/cbmc-primitives/forall_6231_3/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test.c
---pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test_malloc_less_than_bound.c
---pointer-check
+--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