use std::size_t

Author: kroening

src/solvers/flattening/bv_pointers.cpp

@@ -688,7 +688,7 @@ void bv_pointerst::encode(std::size_t addr, bvt &bv)
 
   // set variable part
   for(std::size_t i=0; i<object_bits; i++)
-    bv[offset_bits+i]=const_literal((addr&(1<<i))!=0);
+    bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
 }
 
 /*******************************************************************\

src/solvers/prop/minimize.cpp

@@ -136,7 +136,8 @@ void prop_minimizet::operator()()
   // we need to use assumptions
   assert(prop_conv.has_set_assumptions());
 
-  _iterations=_number_satisfied=0;
+  _iterations=0;
+  _number_satisfied=0;
   _value=0;
   bool last_was_SAT=false;
 

src/solvers/refinement/bv_refinement.h

@@ -45,12 +45,12 @@ class bv_refinementt:public bv_pointerst
   struct approximationt
   {
   public:
-    explicit approximationt(unsigned _id_nr):id_nr(_id_nr)
+    explicit approximationt(std::size_t _id_nr):id_nr(_id_nr)
     {
     }
 
     exprt expr;
-    unsigned no_operands;
+    std::size_t no_operands;
 
     bvt op0_bv, op1_bv, op2_bv, result_bv;
     mp_integer op0_value, op1_value, op2_value, result_value;
@@ -70,7 +70,7 @@ class bv_refinementt:public bv_pointerst
     void add_over_assumption(literalt l);
     void add_under_assumption(literalt l);
 
-    unsigned id_nr;
+    std::size_t id_nr;
   };
 
   typedef std::list<approximationt> approximationst;

src/util/ieee_float.cpp

@@ -106,7 +106,7 @@ Function: ieee_float_spect::from_type
 
 void ieee_float_spect::from_type(const floatbv_typet &type)
 {
-  unsigned width=type.get_width();
+  std::size_t width=type.get_width();
   f=type.get_f();
   assert(f!=0);
   assert(f<width);
@@ -223,7 +223,7 @@ Function: ieee_floatt::to_string_decimal
 
 \*******************************************************************/
 
-std::string ieee_floatt::to_string_decimal(unsigned precision) const
+std::string ieee_floatt::to_string_decimal(std::size_t precision) const
 {
   std::string result;
 
@@ -244,7 +244,7 @@ std::string ieee_floatt::to_string_decimal(unsigned precision) const
     if(precision>0)
     {
       result+='.';
-      for(unsigned i=0; i<precision; i++)
+      for(std::size_t i=0; i<precision; i++)
         result+='0';
     }
   }
@@ -262,7 +262,7 @@ std::string ieee_floatt::to_string_decimal(unsigned precision) const
       if(precision>0)
       {
         result+='.';
-        for(unsigned i=0; i<precision; i++)
+        for(std::size_t i=0; i<precision; i++)
           result+='0';
       }
     }
@@ -325,7 +325,7 @@ Function: ieee_floatt::to_string_scientific
 
 \*******************************************************************/
 
-std::string ieee_floatt::to_string_scientific(unsigned precision) const
+std::string ieee_floatt::to_string_scientific(std::size_t precision) const
 {
   std::string result;
 
@@ -346,7 +346,7 @@ std::string ieee_floatt::to_string_scientific(unsigned precision) const
     if(precision>0)
     {
       result+='.';
-      for(unsigned i=0; i<precision; i++)
+      for(std::size_t i=0; i<precision; i++)
         result+='0';
     }
 
@@ -747,7 +747,7 @@ void ieee_floatt::align()
   mp_integer f_power=power(2, spec.f);
   mp_integer f_power_next=power(2, spec.f+1);
 
-  unsigned lowPower2 = fraction.floorPow2();
+  std::size_t lowPower2 = fraction.floorPow2();
   mp_integer exponent_offset=0;
 
   if (lowPower2 < spec.f) // too small

src/util/ieee_float.h

@@ -20,9 +20,9 @@ class floatbv_typet;
 class ieee_float_spect
 {
 public:
-  // Bits for fraction (excluding hidden bit) and exponent,
-  // respectively
-  unsigned f, e;
+  // Number of bits for fraction (excluding hidden bit)
+  // and exponent, respectively
+  std::size_t f, e;
 
   // x86 has an extended precision format with an explicit
   // integer bit.
@@ -41,11 +41,11 @@ class ieee_float_spect
   {
   }
 
-  ieee_float_spect(unsigned _f, unsigned _e):f(_f), e(_e), x86_extended(false)
+  ieee_float_spect(std::size_t _f, std::size_t _e):f(_f), e(_e), x86_extended(false)
   {
   }
 
-  inline unsigned width() const
+  inline std::size_t width() const
   {
     // Add one for the sign bit.
     // Add one if x86 explicit integer bit is used.
@@ -241,8 +241,8 @@ class ieee_floatt
     return format(format_spect());
   }
 
-  std::string to_string_decimal(unsigned precision) const;
-  std::string to_string_scientific(unsigned precision) const;  
+  std::string to_string_decimal(std::size_t precision) const;
+  std::string to_string_scientific(std::size_t precision) const;  
   std::string format(const format_spect &format_spec) const;
 
   friend inline std::ostream& operator << (std::ostream &out, const ieee_floatt &f)

src/util/std_expr.cpp

@@ -218,7 +218,7 @@ Function: shift_exprt::shift_exprt
 shift_exprt::shift_exprt(
   const exprt &_src,
   const irep_idt &_id,
-  const unsigned _distance):
+  const std::size_t _distance):
   binary_exprt(_src, _id, constant_exprt::integer_constant(_distance))
 {
 }
@@ -237,7 +237,7 @@ Function: extractbit_exprt::extractbit_exprt
 
 extractbit_exprt::extractbit_exprt(
   const exprt &_src,
-  const unsigned _index):
+  const std::size_t _index):
   binary_predicate_exprt(
     _src, ID_extractbit, constant_exprt::integer_constant(_index))
 {
@@ -257,8 +257,8 @@ Function: extractbit_exprt::extractbits_exprt
 
 extractbits_exprt::extractbits_exprt(
   const exprt &_src,
-  const unsigned _upper,
-  const unsigned _lower,
+  const std::size_t _upper,
+  const std::size_t _lower,
   const typet &_type):
   exprt(ID_extractbits, _type)
 {

src/util/std_expr.h

@@ -2005,7 +2005,7 @@ class shift_exprt:public binary_exprt
   {
   }
 
-  shift_exprt(const exprt &_src, const irep_idt &_id, const unsigned _distance);
+  shift_exprt(const exprt &_src, const irep_idt &_id, const std::size_t _distance);
 
   inline exprt &op()
   {
@@ -2066,7 +2066,7 @@ class shl_exprt:public shift_exprt
   {
   }
 
-  shl_exprt(const exprt &_src, const unsigned _distance):shift_exprt(_src, ID_shl, _distance)
+  shl_exprt(const exprt &_src, const std::size_t _distance):shift_exprt(_src, ID_shl, _distance)
   {
   }
 };
@@ -2084,7 +2084,7 @@ class ashr_exprt:public shift_exprt
   {
   }
 
-  inline ashr_exprt(const exprt &_src, const unsigned _distance):shift_exprt(_src, ID_ashr, _distance)
+  inline ashr_exprt(const exprt &_src, const std::size_t _distance):shift_exprt(_src, ID_ashr, _distance)
   {
   }
 };
@@ -2102,7 +2102,7 @@ class lshr_exprt:public shift_exprt
   {
   }
 
-  inline lshr_exprt(const exprt &_src, const unsigned _distance):shift_exprt(_src, ID_lshr, _distance)
+  inline lshr_exprt(const exprt &_src, const std::size_t _distance):shift_exprt(_src, ID_lshr, _distance)
   {
   }
 };
@@ -2190,7 +2190,7 @@ class extractbit_exprt:public binary_predicate_exprt
 
   extractbit_exprt(
     const exprt &_src,
-    const unsigned _index);
+    const std::size_t _index);
 
   exprt &src()
   {
@@ -2260,8 +2260,8 @@ class extractbits_exprt:public exprt
 
   extractbits_exprt(
     const exprt &_src,
-    const unsigned _upper,
-    const unsigned _lower,
+    const std::size_t _upper,
+    const std::size_t _lower,
     const typet &_type);
 
   exprt &src()
@@ -2936,7 +2936,7 @@ class member_exprt:public exprt
     return get_size_t(ID_component_number);
   }
 
-  inline void set_component_number(unsigned component_number)
+  inline void set_component_number(std::size_t component_number)
   {
     set(ID_component_number, component_number);
   }

src/xmllang/graphml.cpp

@@ -31,12 +31,12 @@ Function: add_node
 
 \*******************************************************************/
 
-static unsigned add_node(
+static std::size_t add_node(
   const std::string &name,
-  std::map<std::string, unsigned> &name_to_node,
+  std::map<std::string, std::size_t> &name_to_node,
   graphmlt &graph)
 {
-  std::pair<std::map<std::string, unsigned>::iterator, bool> entry=
+  std::pair<std::map<std::string, std::size_t>::iterator, bool> entry=
     name_to_node.insert(std::make_pair(name, 0));
   if(entry.second)
     entry.first->second=graph.add_node();
@@ -58,7 +58,7 @@ Function: build_graph_rec
 
 static bool build_graph_rec(
   const xmlt &xml,
-  std::map<std::string, unsigned> &name_to_node,
+  std::map<std::string, std::size_t> &name_to_node,
   std::map<std::string, std::map<std::string, std::string> > &defaults,
   graphmlt &dest,
   std::string &entrynode)
@@ -67,7 +67,7 @@ static bool build_graph_rec(
   {
     const std::string node_name=xml.get_attribute("id");
 
-    const unsigned n=add_node(node_name, name_to_node, dest);
+    const std::size_t n=add_node(node_name, name_to_node, dest);
 
     graphmlt::nodet &node=dest[n];
     node.node_name=node_name;
@@ -184,7 +184,7 @@ static bool build_graph(
 {
   assert(dest.size()==0);
 
-  std::map<std::string, unsigned> name_to_node;
+  std::map<std::string, std::size_t> name_to_node;
   std::map<std::string, std::map<std::string, std::string> > defaults;
   std::string entrynode;
 
@@ -196,15 +196,15 @@ static bool build_graph(
       dest,
       entrynode);
 
-  for(unsigned i=0; !err && i<dest.size(); ++i)
+  for(std::size_t i=0; !err && i<dest.size(); ++i)
   {
     const graphmlt::nodet &n=dest[i];
 
     assert(!n.node_name.empty());
   }
 
   assert(!entrynode.empty());
-  std::map<std::string, unsigned>::const_iterator it=
+  std::map<std::string, std::size_t>::const_iterator it=
     name_to_node.find(entrynode);
   assert(it!=name_to_node.end());
   entry=it->second;