Merge pull request #6768 from tautschnig/bugfixes/goto_rw-large-object

goto_rw/range_spect: gracefully handle arbitrarily large ranges

Author: tautschnig

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$
+--

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};
   }