The size of arrays is unsigned

regression/goto-harness/havoc-global-int-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:7 --havoc-variables y
+--harness-type initialise-with-memory-snapshot --memory-snapshot ../load-snapshot-json-snapshots/global-int-x-y-snapshot.json --initial-goto-location main:5 --havoc-variables y
 ^\[main.assertion.1\] line \d+ assertion y \+ 2 > y: FAILURE$
 ^\[main.assertion.2\] line \d+ assertion 0: FAILURE$
 ^EXIT=10$

src/ansi-c/c_typecheck_initializer.cpp

@@ -951,7 +951,7 @@ exprt c_typecheck_baset::do_initializer_list(
     // make complete by setting array size
     size_t size=result.operands().size();
     result.type().id(ID_array);
-    result.type().set(ID_size, from_integer(size, index_type()));
+    result.type().set(ID_size, from_integer(size, size_type()));
   }
 
   return result;

src/ansi-c/c_typecheck_type.cpp

@@ -559,7 +559,6 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
   if(size.is_not_nil())
   {
     typecheck_expr(size);
-    make_index_type(size);
 
     // The size need not be a constant!
     // We simplify it, for the benefit of array initialisation.
@@ -587,10 +586,13 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
         throw 0;
       }
 
+      implicit_typecast(tmp_size, size_type());
+      simplify(tmp_size, *this);
       size=tmp_size;
     }
     else if(tmp_size.id()==ID_infinity)
     {
+      tmp_size.type() = size_type();
       size=tmp_size;
     }
     else if(tmp_size.id()==ID_symbol &&
@@ -602,6 +604,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
       // Of course we can modify a 'const' symbol, e.g.,
       // using a pointer type cast. Interestingly,
       // at least gcc 4.2.1 makes the very same mistake!
+      implicit_typecast(tmp_size, size_type());
       size=tmp_size;
     }
     else
@@ -985,7 +988,7 @@ void c_typecheck_baset::typecheck_compound_body(
 
         // make it zero-length
         c_type.id(ID_array);
-        c_type.set(ID_size, from_integer(0, index_type()));
+        c_type.set(ID_size, from_integer(0, size_type()));
       }
     }
   }

src/ansi-c/literals/convert_string_literal.cpp

@@ -132,7 +132,7 @@ exprt convert_string_literal(const std::string &src)
     result.set(ID_C_string_constant, true);
     result.type()=typet(ID_array);
     result.type().subtype()=subtype;
-    result.type().set(ID_size, from_integer(value.size(), index_type()));
+    result.type().set(ID_size, from_integer(value.size(), size_type()));
 
     result.operands().resize(value.size());
     for(std::size_t i=0; i<value.size(); i++)

src/cpp/cpp_typecheck_compound_type.cpp

@@ -774,7 +774,8 @@ void cpp_typecheckt::check_fixed_size_array(typet &type)
           array_type.size() = symbol.value;
       }
 
-      make_constant_index(array_type.size());
+      implicit_typecast(array_type.size(), size_type());
+      make_constant(array_type.size());
     }
 
     // recursive call for multi-dimensional arrays

src/cpp/cpp_typecheck_expr.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_initializer.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -758,10 +759,8 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr)
     exprt &size=to_array_type(expr.type()).size();
     typecheck_expr(size);
 
-    bool size_is_unsigned=(size.type().id()==ID_unsignedbv);
-    bitvector_typet integer_type(
-      size_is_unsigned ? ID_unsignedbv : ID_signedbv, config.ansi_c.int_width);
-    implicit_typecast(size, integer_type);
+    implicit_typecast(size, size_type());
+    simplify(size, *this);
 
     expr.set(ID_statement, ID_cpp_new_array);
 

src/util/string_constant.cpp

@@ -20,7 +20,7 @@ string_constantt::string_constantt(const irep_idt &_value)
 
 void string_constantt::set_value(const irep_idt &value)
 {
-  exprt size_expr=from_integer(value.size()+1, index_type());
+  exprt size_expr = from_integer(value.size() + 1, size_type());
   type()=array_typet(char_type(), size_expr);
   set(ID_value, value);
 }
@@ -33,7 +33,7 @@ array_exprt string_constantt::to_array_expr() const
   const typet &char_type = to_array_type(type()).subtype();
   bool char_is_unsigned=char_type.id()==ID_unsignedbv;
 
-  exprt size=from_integer(string_size, index_type());
+  exprt size = from_integer(string_size, size_type());
 
   array_exprt dest({}, array_typet(char_type, size));