Remove infinity_exprt

This removes `infinity_exprt` together with all its uses, where were all
about array size. Any such arrays were replaced by arrays of the maximum
viable size.

Author: tautschnig

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -450,7 +450,7 @@ refined_string_exprt java_string_library_preprocesst::replace_char_array(
     get_length(array, symbol_table), char_array, refined_string_type);
 
   const dereference_exprt inf_array(
-    char_array, array_typet(java_char_type(), infinity_exprt(java_int_type())));
+    char_array, array_typet(java_char_type(), java_int_type().largest_expr()));
 
   add_pointer_to_array_association(
     string_expr.content(), inf_array, symbol_table, loc, function_id, code);
@@ -619,7 +619,7 @@ exprt make_nondet_infinite_char_array(
   code_blockt &code)
 {
   const array_typet array_type(
-    java_char_type(), infinity_exprt(java_int_type()));
+    java_char_type(), java_int_type().largest_expr());
   const symbolt data_sym = fresh_java_symbol(
     pointer_type(array_type),
     "nondet_infinite_array_pointer",

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -40,21 +40,21 @@ class tt
   {
     return java_char_type();
   }
-  typet length_type() const
+  signedbv_typet length_type() const
   {
     return java_int_type();
   }
   array_typet array_type() const
   {
-    return array_typet(char_type(), infinity_exprt(length_type()));
+    return array_typet(char_type(), length_type().largest_expr());
   }
   refined_string_typet string_type() const
   {
     return refined_string_typet(length_type(), pointer_type(char_type()));
   }
   array_typet witness_type() const
   {
-    return array_typet(length_type(), infinity_exprt(length_type()));
+    return array_typet(length_type(), length_type().largest_expr());
   }
 };
 

jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp

@@ -21,15 +21,15 @@ Author: Diffblue Ltd.
 #include <java_bytecode/java_bytecode_language.h>
 #endif
 
-typet length_type()
+signedbv_typet length_type()
 {
   return signedbv_typet(32);
 }
 
 /// Make a struct with a pointer content and an integer length
 struct_exprt make_string_argument(std::string name)
 {
-  const array_typet char_array(char_type(), infinity_exprt(length_type()));
+  const array_typet char_array(char_type(), length_type().largest_expr());
   struct_typet type(
     {{"length", length_type()}, {"content", pointer_type(char_array)}});
 

regression/cbmc-concurrency/thread_chain_cbmc1/main.c

@@ -18,7 +18,8 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-concurrency/thread_chain_cbmc2/main.c

@@ -18,7 +18,8 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_bool __CPROVER_threads_exited
+  [(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.

regression/cbmc-cpp/Vector1/lib/list

@@ -372,10 +372,10 @@ namespace std {
   #ifdef VERS1
   unsigned _version;
   #elif defined VERS2
-  unsigned _version[__CPROVER::constant_infinity_uint];
+  unsigned _version[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   #endif
 
-  T _data[__CPROVER::constant_infinity_uint];
+  T _data[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   };
 
 }

regression/cbmc-cpp/Vector1/lib/vector

@@ -416,10 +416,10 @@ namespace std {
   #ifdef VERS1
   unsigned _version;
   #elif defined VERS2
-  unsigned _version[__CPROVER::constant_infinity_uint];
+  unsigned _version[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   #endif
 
-  T _data[__CPROVER::constant_infinity_uint];
+  T _data[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
   };
 
 }

regression/cbmc-cpp/initialization5/main.cpp

@@ -1,9 +1,9 @@
 #include <cassert>
-int a[__CPROVER::constant_infinity_uint];
+int a[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 struct A
 {
-  int i[__CPROVER::constant_infinity_uint];
+  int i[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 };
 
 A o;

regression/cbmc/Unbounded_Array5/main.c

@@ -1,4 +1,4 @@
-int mem[__CPROVER_constant_infinity_uint];
+int mem[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 int main()
 {

regression/cbmc/array_of_bool_as_bitvec/main.c

@@ -3,7 +3,7 @@
 #include <stdlib.h>
 
 __CPROVER_bool w[8];
-__CPROVER_bool v[__CPROVER_constant_infinity_uint];
+__CPROVER_bool v[(__CPROVER_size_t)1 << (sizeof(__CPROVER_size_t) * 8 - 2)];
 
 void main()
 {