Make use of bv_spect::max_value()

The method can be used in two places that previously duplicated its
logic.

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_object_factory.h"
 
+#include <util/bv_arithmetic.h>
 #include <util/expr_initializer.h>
 #include <util/nondet.h>
 #include <util/nondet_bool.h>
@@ -351,19 +352,6 @@ class recursion_set_entryt
   }
 };
 
-/// Get max value for an integer type
-/// \param type:
-///   Type to find maximum value for
-/// \return Maximum integer value
-static mp_integer max_value(const typet &type)
-{
-  if(type.id() == ID_signedbv)
-    return to_signedbv_type(type).largest();
-  else if(type.id() == ID_unsignedbv)
-    return to_unsignedbv_type(type).largest();
-  UNREACHABLE;
-}
-
 /// Initialise length and data fields for a nondeterministic String structure.
 ///
 /// If the structure is not a nondeterministic structure, the call results in
@@ -458,7 +446,7 @@ void initialize_nondet_string_fields(
   code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
 
   // assume (length_expr <= max_input_length)
-  if(max_nondet_string_length <= max_value(length_expr.type()))
+  if(max_nondet_string_length <= bv_spect(length_expr.type()).max_value())
   {
     exprt max_length =
       from_integer(max_nondet_string_length, length_expr.type());

src/ansi-c/ansi_c_entry_point.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "ansi_c_entry_point.h"
 
 #include <util/arith_tools.h>
+#include <util/bv_arithmetic.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/string_constant.h>
@@ -377,18 +378,7 @@ bool generate_ansi_c_start_function(
         }
 
         // assume envp_size is INTMAX-1
-        mp_integer max;
-
-        if(envp_size_symbol.type.id()==ID_signedbv)
-        {
-          max=to_signedbv_type(envp_size_symbol.type).largest();
-        }
-        else if(envp_size_symbol.type.id()==ID_unsignedbv)
-        {
-          max=to_unsignedbv_type(envp_size_symbol.type).largest();
-        }
-        else
-          UNREACHABLE;
+        mp_integer max = bv_spect(envp_size_symbol.type).max_value();
 
         exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);