malloc MAY fail cbmc/primitives

Author: Enrico Steffinlongo

regression/cbmc-primitives/alternating_quantifiers_6231/exists_in_forall.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 exists_in_forall.c
---no-malloc-fail --pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line \d* for all z, there exists a y so that y = z \+ 10 and y > 1: SUCCESS

regression/cbmc-primitives/alternating_quantifiers_6231/forall_in_exists.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 forall_in_exists.c
---no-malloc-fail --pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line \d* there exists a z between 0 and 2 so that for all o between 10 and 20, o > z and z = 1: SUCCESS

regression/cbmc-primitives/exists_assume_6231/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 test.c
---no-malloc-fail --pointer-check
+--no-malloc-may-fail --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line \d+ this assertion should be satified: SUCCESS

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

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

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

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

regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail --pointer-check --no-simplify --no-propagation
+--no-malloc-may-fail --pointer-check --no-simplify --no-propagation
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/r_w_ok_valid/test.desc

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

regression/cbmc-primitives/same-object-01/test-no-cp.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail --no-simplify --no-propagation
+--no-malloc-may-fail --no-simplify --no-propagation
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/same-object-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/same-object-02/test-no-cp.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail --no-simplify --no-propagation
+--no-malloc-may-fail --no-simplify --no-propagation
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/same-object-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/same-object-03/test-no-cp.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail --no-simplify --no-propagation
+--no-malloc-may-fail --no-simplify --no-propagation
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-primitives/same-object-03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$