use std::size_t

Author: kroening

src/analyses/goto_check.cpp

@@ -342,11 +342,11 @@ void goto_checkt::integer_overflow_check(
 
     if(type.id()==ID_signedbv)
     {
-      unsigned new_width=to_signedbv_type(type).get_width();
+      std::size_t new_width=to_signedbv_type(type).get_width();
 
       if(old_type.id()==ID_signedbv) // signed -> signed
       {
-        unsigned old_width=to_signedbv_type(old_type).get_width();
+        std::size_t old_width=to_signedbv_type(old_type).get_width();
         if(new_width>=old_width) return; // always ok
 
         binary_relation_exprt no_overflow_upper(ID_le);
@@ -367,7 +367,7 @@ void goto_checkt::integer_overflow_check(
       }
       else if(old_type.id()==ID_unsignedbv) // unsigned -> signed
       {
-        unsigned old_width=to_unsignedbv_type(old_type).get_width();
+        std::size_t old_width=to_unsignedbv_type(old_type).get_width();
         if(new_width>=old_width+1) return; // always ok
 
         binary_relation_exprt no_overflow_upper(ID_le);
@@ -408,11 +408,11 @@ void goto_checkt::integer_overflow_check(
     }
     else if(type.id()==ID_unsignedbv)
     {
-      unsigned new_width=to_unsignedbv_type(type).get_width();
+      std::size_t new_width=to_unsignedbv_type(type).get_width();
 
       if(old_type.id()==ID_signedbv) // signed -> unsigned
       {
-        unsigned old_width=to_signedbv_type(old_type).get_width();
+        std::size_t old_width=to_signedbv_type(old_type).get_width();
 
         if(new_width>=old_width-1)
         {
@@ -451,7 +451,7 @@ void goto_checkt::integer_overflow_check(
       }
       else if(old_type.id()==ID_unsignedbv) // unsigned -> unsigned
       {
-        unsigned old_width=to_unsignedbv_type(old_type).get_width();
+        std::size_t old_width=to_unsignedbv_type(old_type).get_width();
         if(new_width>=old_width) return; // always ok
 
         binary_relation_exprt no_overflow_upper(ID_le);

src/goto-instrument/goto_program2code.cpp

@@ -969,7 +969,7 @@ bool goto_program2codet::set_block_end_points(
   cases_listt &cases,
   std::set<unsigned> &processed_locations)
 {
-  std::map<goto_programt::const_targett, unsigned> targets_done;
+  std::map<goto_programt::const_targett, std::size_t> targets_done;
 
   for(cases_listt::iterator it=cases.begin();
       it!=cases.end();

src/goto-programs/graphml_goto_trace.cpp

@@ -155,7 +155,7 @@ void convert(
   graphml[sink].is_violation=false;
 
   // step numbers start at 1
-  std::vector<unsigned> step_to_node(goto_trace.steps.size()+1, 0);
+  std::vector<std::size_t> step_to_node(goto_trace.steps.size()+1, 0);
 
   for(goto_tracet::stepst::const_iterator
       it=goto_trace.steps.begin();

src/pointer-analysis/value_set.cpp

@@ -181,7 +181,7 @@ void value_sett::output(
 
     const object_map_dt &object_map=e.object_map.read();
 
-    unsigned width=0;
+    std::size_t width=0;
 
     for(object_map_dt::const_iterator
         o_it=object_map.begin();
@@ -1878,7 +1878,7 @@ exprt value_sett::make_member(
   if(src.id()==ID_struct ||
      src.id()==ID_constant)
   {
-    unsigned no=struct_union_type.component_number(component_name);
+    std::size_t no=struct_union_type.component_number(component_name);
     assert(no<src.operands().size());
     return src.operands()[no];
   }

src/pointer-analysis/value_set_fi.cpp

@@ -89,7 +89,7 @@ void value_set_fit::output(
     object_mapt object_map;
     flatten(e, object_map);
 
-    unsigned width=0;    
+    std::size_t width=0;    
 
     forall_objects(o_it, object_map.read())
     {

src/pointer-analysis/value_set_fivr.cpp

@@ -117,7 +117,7 @@ void value_set_fivrt::output(
     out << display_name << " = { ";
     if(object_map.read().size()!=0) out << "\n      ";
 
-    unsigned width=0;
+    std::size_t width=0;
 
     forall_objects(o_it, object_map.read())
     {

src/pointer-analysis/value_set_fivrns.cpp

@@ -120,7 +120,7 @@ void value_set_fivrnst::output_entry(
   out << display_name << " = { ";
   if(object_map.read().size()!=0) out << "\n      ";
 
-  unsigned width=0;
+  std::size_t width=0;
 
   forall_valid_objects(o_it, object_map.read())
   {

src/solvers/flattening/boolbv_typecast.cpp

@@ -545,7 +545,7 @@ bool boolbvt::type_conversion(
         build_offset_map(dest_struct, dest_offsets);
 
         // build name map
-        typedef std::map<irep_idt, unsigned> op_mapt;
+        typedef std::map<irep_idt, std::size_t> op_mapt;
         op_mapt op_map;
 
         for(std::size_t i=0; i<op_comp.size(); i++)

src/solvers/flattening/bv_pointers.cpp

@@ -678,7 +678,7 @@ Function: bv_pointerst::encode
 
 \*******************************************************************/
 
-void bv_pointerst::encode(unsigned addr, bvt &bv)
+void bv_pointerst::encode(std::size_t addr, bvt &bv)
 {
   bv.resize(bits);
 
@@ -795,9 +795,9 @@ Function: bv_pointerst::add_addr
 
 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 {
-  unsigned a=pointer_logic.add_object(expr);
+  std::size_t a=pointer_logic.add_object(expr);
 
-  if(a==(unsigned(1)>>object_bits))
+  if(a==(std::size_t(1)>>object_bits))
     throw "too many variables";
 
   encode(a, bv);

src/solvers/flattening/bv_pointers.h

@@ -28,7 +28,7 @@ class bv_pointerst:public boolbvt
 
   unsigned object_bits, offset_bits, bits;
 
-  void encode(unsigned object, bvt &bv);
+  void encode(std::size_t object, bvt &bv);
 
   virtual bvt convert_pointer_type(const exprt &expr);