Use std::size_t when referring to object size

Author: tautschnig

jbmc/src/java_bytecode/java_bmc_util.cpp

@@ -29,9 +29,9 @@ void java_setup_symex(
     symex.add_loop_unwind_handler(
       [&goto_model](
         const call_stackt &context,
-        unsigned loop_num,
-        unsigned unwind,
-        unsigned &max_unwind)
+        std::size_t loop_num,
+        std::size_t unwind,
+        std::size_t &max_unwind)
       { // NOLINT (*)
         return java_enum_static_init_unwind_handler(
           context, loop_num, unwind, max_unwind, goto_model.get_symbol_table());

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -69,9 +69,9 @@ static irep_idt find_enum_function_on_stack(const call_stackt &context)
 ///   otherwise.
 tvt java_enum_static_init_unwind_handler(
   const call_stackt &context,
-  unsigned loop_number,
-  unsigned unwind_count,
-  unsigned &unwind_max,
+  std::size_t loop_number,
+  std::size_t unwind_count,
+  std::size_t &unwind_max,
   const symbol_tablet &symbol_table)
 {
   (void)loop_number; // unused parameter

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.h

@@ -19,9 +19,9 @@ class symbol_tablet;
 
 tvt java_enum_static_init_unwind_handler(
   const call_stackt &context,
-  unsigned loop_number,
-  unsigned unwind_count,
-  unsigned &unwind_max,
+  std::size_t loop_number,
+  std::size_t unwind_count,
+  std::size_t &unwind_max,
   const symbol_tablet &symbol_table);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -203,19 +203,19 @@ static void gather_transitive_predecessors(
 ///   slot `slotidx`
 static bool is_store_to_slot(
   const java_bytecode_convert_methodt::instructiont &inst,
-  unsigned slotidx)
+  std::size_t slotidx)
 {
   const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic;
 
   if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
     return false;
 
-  unsigned storeslotidx;
+  std::size_t storeslotidx;
   if(inst.args.size()==1)
   {
     // Store with an argument:
     const auto &arg=inst.args[0];
-    storeslotidx = numeric_cast_v<unsigned>(to_constant_expr(arg));
+    storeslotidx = numeric_cast_v<std::size_t>(to_constant_expr(arg));
   }
   else
   {

src/analyses/custom_bitvector_analysis.cpp

@@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 void custom_bitvector_domaint::set_bit(
   const irep_idt &identifier,
-  unsigned bit_nr,
+  std::size_t bit_nr,
   modet mode)
 {
   switch(mode)
@@ -48,7 +48,7 @@ void custom_bitvector_domaint::set_bit(
 
 void custom_bitvector_domaint::set_bit(
   const exprt &lhs,
-  unsigned bit_nr,
+  std::size_t bit_nr,
   modet mode)
 {
   irep_idt id=object2id(lhs);
@@ -174,8 +174,7 @@ custom_bitvector_domaint::vectorst
   return vectorst();
 }
 
-unsigned custom_bitvector_analysist::get_bit_nr(
-  const exprt &string_expr)
+std::size_t custom_bitvector_analysist::get_bit_nr(const exprt &string_expr)
 {
   if(string_expr.id()==ID_typecast)
     return get_bit_nr(to_typecast_expr(string_expr).op());
@@ -327,7 +326,8 @@ void custom_bitvector_domaint::transform(
         {
           if(instruction.call_arguments().size() == 2)
           {
-            unsigned bit_nr = cba.get_bit_nr(instruction.call_arguments()[1]);
+            const std::size_t bit_nr =
+              cba.get_bit_nr(instruction.call_arguments()[1]);
 
             // initialize to make Visual Studio happy
             modet mode = modet::SET_MUST;
@@ -456,7 +456,7 @@ void custom_bitvector_domaint::transform(
         DATA_INVARIANT(
           code.operands().size() == 2, "set/clear_may/must has two operands");
 
-        unsigned bit_nr = cba.get_bit_nr(code.op1());
+        const std::size_t bit_nr = cba.get_bit_nr(code.op1());
 
         // initialize to make Visual Studio happy
         modet mode = modet::SET_MUST;
@@ -578,7 +578,7 @@ void custom_bitvector_domaint::output(
     out << bit.first << " MAY:";
     bit_vectort b=bit.second;
 
-    for(unsigned i=0; b!=0; i++, b>>=1)
+    for(std::size_t i = 0; b != 0; i++, b >>= 1)
       if(b&1)
       {
         INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
@@ -594,7 +594,7 @@ void custom_bitvector_domaint::output(
     out << bit.first << " MUST:";
     bit_vectort b=bit.second;
 
-    for(unsigned i=0; b!=0; i++, b>>=1)
+    for(std::size_t i = 0; b != 0; i++, b >>= 1)
       if(b&1)
       {
         INVARIANT(i < cba.bits.size(), "inconsistent bit widths");
@@ -706,7 +706,7 @@ exprt custom_bitvector_domaint::eval(
   {
     if(src.operands().size()==2)
     {
-      unsigned bit_nr =
+      const std::size_t bit_nr =
         custom_bitvector_analysis.get_bit_nr(to_binary_expr(src).op1());
 
       exprt pointer = to_binary_expr(src).op0();
@@ -773,7 +773,7 @@ void custom_bitvector_analysist::check(
   bool use_xml,
   std::ostream &out)
 {
-  unsigned pass=0, fail=0, unknown=0;
+  std::size_t pass = 0, fail = 0, unknown = 0;
 
   for(const auto &gf_entry : goto_model.goto_functions.function_map)
   {

src/analyses/custom_bitvector_analysis.h

@@ -116,21 +116,21 @@ class custom_bitvector_domaint:public ai_domain_baset
 private:
   enum class modet { SET_MUST, CLEAR_MUST, SET_MAY, CLEAR_MAY };
 
-  void set_bit(const exprt &, unsigned bit_nr, modet);
-  void set_bit(const irep_idt &, unsigned bit_nr, modet);
+  void set_bit(const exprt &, std::size_t bit_nr, modet);
+  void set_bit(const irep_idt &, std::size_t bit_nr, modet);
 
-  static inline void set_bit(bit_vectort &dest, unsigned bit_nr)
+  static inline void set_bit(bit_vectort &dest, std::size_t bit_nr)
   {
     dest|=(1ll<<bit_nr);
   }
 
-  static inline void clear_bit(bit_vectort &dest, unsigned bit_nr)
+  static inline void clear_bit(bit_vectort &dest, std::size_t bit_nr)
   {
     dest|=(1ll<<bit_nr);
     dest^=(1ll<<bit_nr);
   }
 
-  static inline bool get_bit(const bit_vectort src, unsigned bit_nr)
+  static inline bool get_bit(const bit_vectort src, std::size_t bit_nr)
   {
     return (src&(1ll<<bit_nr))!=0;
   }
@@ -153,7 +153,7 @@ class custom_bitvector_analysist:public ait<custom_bitvector_domaint>
     return operator[](loc).eval(src, *this);
   }
 
-  unsigned get_bit_nr(const exprt &);
+  std::size_t get_bit_nr(const exprt &);
 
   typedef numberingt<irep_idt> bitst;
   bitst bits;

src/analyses/invariant_propagation.h

@@ -54,7 +54,7 @@ class invariant_propagationt:public
 
   inv_object_storet object_store;
 
-  typedef std::list<unsigned> object_listt;
+  typedef std::list<std::size_t> object_listt;
 
   void add_objects(const goto_programt &goto_program);
   void add_objects(const goto_functionst &goto_functions);