malloc MAY fail cbmc

Author: Enrico Steffinlongo

regression/cbmc/Bitfields3/paths.desc

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

regression/cbmc/Bitfields3/test.desc

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

regression/cbmc/Function_Pointer6/test.desc

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

regression/cbmc/Linked_List1/test.desc

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

regression/cbmc/Linking8/test.desc

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

regression/cbmc/Malloc1/test.desc

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

regression/cbmc/Malloc11/slice-formula.desc

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

regression/cbmc/Malloc11/test.desc

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

regression/cbmc/Malloc13/test.desc

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

regression/cbmc/Malloc21/test.desc

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

regression/cbmc/Malloc23/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=10$
 ^SIGNAL=0$
 pointer outside object bounds in \*p: FAILURE

regression/cbmc/Malloc24/test.desc

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

regression/cbmc/Malloc6/test.desc

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

regression/cbmc/Malloc7/test.desc

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

regression/cbmc/Malloc9/test.desc

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

regression/cbmc/Pointer_array5/test.desc

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

regression/cbmc/Pointer_array6/test.desc

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

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,6 +1,6 @@
 CORE broken-cprover-smt-backend no-new-smt
 main.i
---no-malloc-fail --32 --no-simplify
+--no-malloc-may-fail --32 --no-simplify
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.i
---no-malloc-fail --32
+--no-malloc-may-fail --32
 ^EXIT=10$
 ^SIGNAL=0$
 array\.List dynamic object upper bound in p->List\[2\]: FAILURE

regression/cbmc/Pointer_byte_extract8/test.desc

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

regression/cbmc/Pointer_comparison3/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^\[main.assertion.3\] line 21 always false for different objects: FAILURE$
 ^\[main.assertion.4\] line 23 always false for different objects: FAILURE$
 ^\*\* 11 of 59 failed

regression/cbmc/String_Abstraction14/test.desc

@@ -1,6 +1,6 @@
 CORE
 pass-in-implicit.c
---no-malloc-fail --string-abstraction
+--no-malloc-may-fail --string-abstraction
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/String_Abstraction16/test.desc

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

regression/cbmc/String_Abstraction18/test.desc

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

regression/cbmc/String_Abstraction20/test.desc

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

regression/cbmc/String_Abstraction21/test.desc

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

regression/cbmc/Struct_Pointer2/test.desc

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

regression/cbmc/array-cell-sensitivity5/test_execution.desc

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

regression/cbmc/array-cell-sensitivity6/test_execution.desc

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

regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

@@ -1,6 +1,6 @@
 CORE broken-smt-backend no-new-smt
 main.c
---no-malloc-fail --smt2 --outfile -
+--no-malloc-may-fail --smt2 --outfile -
 \(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
 \(= \(select array\.1 \(\(_ zero_extend \d+\) \|main::1::idx!0@1#1\|\)\) #b1\)
 \(= \(select array\.1 \(_ bv\d+ \d+\)\) \(ite false #b1 #b0\)\)

regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc

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

regression/cbmc/big-endian-array1/test.desc

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

regression/cbmc/bounds_check1/test.desc

@@ -1,6 +1,6 @@
 CORE thorough-smt-backend no-new-smt
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=10$
 ^SIGNAL=0$
 \[\(.*\)i2\]: FAILURE

regression/cbmc/double_deref/double_deref.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} \(main::1::pptr!0@1#2 = address_of\(main::1::ptr[12]!0@1\) \? main::argc!0@1#1 = [12] : main::argc!0@1#1 = [12]\)
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_single_alias.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_single_alias.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_with_cast.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_cast.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} \(cast\(main::1::pptr!0@1#2, signedbv\[32\]\*\*\) = address_of\(main::1::ptr2!0@1\) \? main::argc!0@1#1 = 2 \: main::argc!0@1#1 = 1\)
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_with_cast_single_alias.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_cast_single_alias.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_with_member.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_member.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 ^\{1\} \(main::1::cptr!0@1#2 = address_of\(main::1::container2!0@1\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_with_member_single_alias.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_member_single_alias.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} main::argc!0@1#1 = 1
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_pointer_arithmetic.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 ^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[(mod\(main::argc!0@1#1, 2\)|cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\))\]
 ^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
 ^EXIT=0$

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,6 +1,6 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
---no-malloc-fail --show-vcc
+--no-malloc-may-fail --show-vcc
 \{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$0\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_short.desc

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

regression/cbmc/little-endian-array1/test.desc

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

regression/cbmc/malloc-may-fail/test_without_option.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion p: SUCCESS$

regression/cbmc/malloc-too-large/largest_representable.desc

@@ -1,6 +1,6 @@
 CORE
 largest_representable.c
---no-malloc-fail --malloc-fail-assert
+--no-malloc-may-fail --malloc-fail-assert
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[malloc.assertion.\d+\] line \d+ max allocation size exceeded: SUCCESS$

regression/cbmc/memset1/test.desc

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

regression/cbmc/pointer-offset-01/test.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---no-malloc-fail --trace
+--no-malloc-may-fail --trace
 ^\s*ub.*=(\(char \*\)&)?dynamic_object \+ \d+
 ^\s*offset_ubp1=\d+ul* \(00000000 1[0 ]+1\)$
 ^VERIFICATION FAILED$

regression/cbmc/pointer-overflow3/no-simplify.desc

@@ -1,6 +1,6 @@
 CORE no-new-smt
 main.c
---no-malloc-fail --pointer-overflow-check --no-simplify
+--no-malloc-may-fail --pointer-overflow-check --no-simplify
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ (\(signed (long (long )?)?int\))?10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - (\(signed (long (long )?)?int\))?10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ (\(signed (long (long )?)?int\))?10: FAILURE

regression/cbmc/pointer-overflow3/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail --pointer-overflow-check
+--no-malloc-may-fail --pointer-overflow-check
 ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ (\(signed (long (long )?)?int\))?10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - (\(signed (long (long )?)?int\))?10: FAILURE
 ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ (\(signed (long (long )?)?int\))?10: FAILURE

regression/cbmc/r_w_ok1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---no-malloc-fail
+--no-malloc-may-fail
 __CPROVER_[rw]_ok\(arbitrary_size, n \+ 1\): FAILURE$
 ^\*\* 2 of \d+ failed
 ^VERIFICATION FAILED$