From f2f218e244e17d4ded0010c140c8da8a08cdef39 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 18 Mar 2022 21:12:31 +0000
Subject: [PATCH] goto_rw/range_spect: gracefully handle arbitrarily large
 ranges

When the value of an mp_integer doesn't fit into a
range_spect::value_type we can safely fall back to using "unknown"
instead, which is a safe over-approximation.
---
 .../cbmc/havoc_slice_checks/full-slice.desc      | 15 +++++++++++++++
 src/analyses/goto_rw.h                           | 16 +++++++++++++---
 2 files changed, 28 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc/havoc_slice_checks/full-slice.desc

diff --git a/regression/cbmc/havoc_slice_checks/full-slice.desc b/regression/cbmc/havoc_slice_checks/full-slice.desc
new file mode 100644
index 00000000000..01af361a4ba
--- /dev/null
+++ b/regression/cbmc/havoc_slice_checks/full-slice.desc
@@ -0,0 +1,15 @@
+CORE
+main.c
+--full-slice
+^\[main\.assertion\.\d+\] line 9 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 13 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 18 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 21 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 24 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 27 assertion havoc_slice W_OK.*: FAILURE$
+^\[main\.assertion\.\d+\] line 30 assertion havoc_slice W_OK.*: FAILURE$
+\*\* 7 of [0-9]+ failed \(.*\)
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h
index 4d7ad1d0370..fdb53deb314 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -78,10 +78,20 @@ class range_spect
 
   static range_spect to_range_spect(const mp_integer &size)
   {
-    PRECONDITION(size.is_long());
+    // The size need not fit into the analysis platform's width of a signed long
+    // (as an example, it could be an unsigned size_t max, or perhaps the source
+    // platform has much wider types than the analysis platform.
+    if(!size.is_long())
+      return range_spect::unknown();
+
     mp_integer::llong_t ll = size.to_long();
-    CHECK_RETURN(ll <= std::numeric_limits<range_spect::value_type>::max());
-    CHECK_RETURN(ll >= std::numeric_limits<range_spect::value_type>::min());
+    if(
+      ll > std::numeric_limits<range_spect::value_type>::max() ||
+      ll < std::numeric_limits<range_spect::value_type>::min())
+    {
+      return range_spect::unknown();
+    }
+
     return range_spect{(value_type)ll};
   }