Make use of bitvector_typet::largest

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

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -351,19 +351,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 +445,8 @@ 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 <= to_bitvector_type(length_expr.type()).largest())
   {
     exprt max_length =
       from_integer(max_nondet_string_length, length_expr.type());

src/ansi-c/ansi_c_entry_point.cpp

@@ -377,18 +377,8 @@ 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;
+        const mp_integer max =
+          to_bitvector_type(envp_size_symbol.type).largest();
 
         exprt max_minus_one=from_integer(max-1, envp_size_symbol.type);
 

src/util/simplify_expr_int.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include "arith_tools.h"
-#include "bv_arithmetic.h"
 #include "byte_operators.h"
 #include "config.h"
 #include "expr_util.h"
@@ -1879,8 +1878,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
   if(expr.op0().type().id()==ID_unsignedbv ||
      expr.op0().type().id()==ID_signedbv)
   {
-    bv_spect spec(expr.op0().type());
-    mp_integer max(spec.max_value());
+    mp_integer max(to_bitvector_type(expr.op0().type()).largest());
 
     if(expr.id()==ID_notequal)
     {