malloc MAY fail cbmc/library

Author: Enrico Steffinlongo

regression/cbmc-library/Malloc20/test.desc

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

regression/cbmc-library/String6/test.desc

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

regression/cbmc-library/calloc-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-library/equality_through_struct_containing_arrays3/test.desc

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

regression/cbmc-library/fileno-01/test.desc

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

regression/cbmc-library/memcpy-04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^\[publish.assertion.1\] line 18 should pass: SUCCESS$
 ^\[publish.assertion.2\] line 19 should fail: FAILURE$
 ^\*\* 1 of \d+ failed

regression/cbmc-library/memcpy-05/test.desc

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

regression/cbmc-library/memcpy-08/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^\[main.assertion.1\] line 20 should pass: SUCCESS$
 ^\[main.assertion.2\] line 21 should fail: FAILURE$
 ^\*\* 1 of \d+ failed

regression/cbmc-library/realloc-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-library/realloc-02/test.desc

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