From 429d9054b0af7b7da6fb4d78a0de0917b0b2a6e6 Mon Sep 17 00:00:00 2001
From: Enrico Steffinlongo <enrico.steffinlongo@diffblue.com>
Date: Mon, 18 Dec 2023 23:07:07 +0000
Subject: [PATCH] malloc MAY fail cbmc/primitives

---
 .../exists_memory_checks/smt_missing_range_check.desc           | 2 +-
 .../cbmc-primitives/exists_memory_checks/valid_index_range.desc | 2 +-
 regression/cbmc-primitives/forall_6231_1/test.desc              | 2 +-
 regression/cbmc-primitives/forall_6231_2/test.desc              | 2 +-
 regression/cbmc-primitives/forall_6231_3/test.desc              | 2 +-
 .../forall_6231_3/test_malloc_less_than_bound.desc              | 2 +-
 6 files changed, 6 insertions(+), 6 deletions(-)

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
index 56f0ee658661..a2ee20ffd2dd 100644
--- a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc
+++ b/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$
diff --git a/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc b/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc
index 90ae42be1c34..830e7af009d7 100644
--- a/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc
+++ b/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$
diff --git a/regression/cbmc-primitives/forall_6231_1/test.desc b/regression/cbmc-primitives/forall_6231_1/test.desc
index 1d6fa8f57260..aab5fbf2f8e0 100644
--- a/regression/cbmc-primitives/forall_6231_1/test.desc
+++ b/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
diff --git a/regression/cbmc-primitives/forall_6231_2/test.desc b/regression/cbmc-primitives/forall_6231_2/test.desc
index 786c05df17de..2a3997916565 100644
--- a/regression/cbmc-primitives/forall_6231_2/test.desc
+++ b/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
diff --git a/regression/cbmc-primitives/forall_6231_3/test.desc b/regression/cbmc-primitives/forall_6231_3/test.desc
index 748f2e287e3d..c668271b3f5b 100644
--- a/regression/cbmc-primitives/forall_6231_3/test.desc
+++ b/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
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
index be22cba158a6..bbc8bd2271b1 100644
--- 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
@@ -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