use std::size_t where needed

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6495 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/goto-instrument/accelerate/overflow_instrumenter.cpp

@@ -83,8 +83,8 @@ void overflow_instrumentert::overflow_expr(const exprt &expr,
     }
 
     const typet &old_type = ns.follow(expr.op0().type());
-    unsigned new_width = expr.type().get_int(ID_width);
-    unsigned old_width = old_type.get_int(ID_width);
+    std::size_t new_width = expr.type().get_int(ID_width);
+    std::size_t old_width = old_type.get_int(ID_width);
 
     if (type.id() == ID_signedbv) {
       if (old_type.id() == ID_signedbv) {
@@ -160,7 +160,7 @@ void overflow_instrumentert::overflow_expr(const exprt &expr,
 
     if (expr.operands().size() >= 3) {
       // The overflow checks are binary.
-      for (unsigned i = 1; i < expr.operands().size(); i++) {
+      for (std::size_t i = 1; i < expr.operands().size(); i++) {
         exprt tmp;
 
         if (i == 1) {

src/goto-instrument/accelerate/trace_automaton.cpp

@@ -299,10 +299,12 @@ void automatont::move(state_sett &s, goto_programt::targett a, state_sett &t) {
   }
 }
 
-void trace_automatont::get_transitions(sym_mapt &transitions) {
+void trace_automatont::get_transitions(sym_mapt &transitions)
+{
   automatont::transition_tablet &dtrans = dta.transitions;
 
-  for (unsigned int i = 0; i < dtrans.size(); ++i) {
+  for(std::size_t i = 0; i < dtrans.size(); ++i)
+  {
     automatont::transitionst &dta_transitions = dtrans[i];
 
     for (automatont::transitionst::iterator it = dta_transitions.begin();
@@ -318,13 +320,14 @@ void trace_automatont::get_transitions(sym_mapt &transitions) {
   }
 }
 
-void automatont::reverse(goto_programt::targett epsilon) {
+void automatont::reverse(goto_programt::targett epsilon)
+{
   transition_tablet old_table;
   statet new_init;
 
   old_table.swap(transitions);
 
-  for (unsigned int i = 0; i < old_table.size(); i++) {
+  for(std::size_t i = 0; i < old_table.size(); i++) {
     transitions.push_back(transitionst());
   }
 
@@ -354,7 +357,8 @@ void automatont::reverse(goto_programt::targett epsilon) {
 
   init_state = new_init;
 
-  for (unsigned int i = 0; i < old_table.size(); i++) {
+  for(std::size_t i = 0; i < old_table.size(); i++)
+  {
     transitionst &trans = old_table[i];
 
     for (transitionst::iterator it = trans.begin();
@@ -400,8 +404,10 @@ void automatont::trim() {
     tmp.swap(new_states);
   } while (!new_states.empty());
 
-  for (unsigned int i = 0; i < num_states; i++) {
-    if (reachable.find(i) == reachable.end()) {
+  for(std::size_t i = 0; i < num_states; i++)
+  {
+    if (reachable.find(i) == reachable.end())
+    {
       transitions[i] = transitionst();
       accept_states.erase(i);
     }
@@ -443,8 +449,9 @@ void automatont::output(std::ostream &str) {
   }
 }
 
-unsigned int automatont::count_transitions() {
-  unsigned int ret = 0;
+std::size_t automatont::count_transitions()
+{
+  std::size_t ret = 0;
 
   for (transition_tablet::iterator it = transitions.begin();
        it != transitions.end();

src/goto-instrument/accelerate/trace_automaton.h

@@ -37,7 +37,7 @@ class automatont {
   void reverse(goto_programt::targett epsilon);
   void trim();
 
-  unsigned int count_transitions();
+  std::size_t count_transitions();
 
   void output(std::ostream &str);
 

src/goto-instrument/accelerate/util.cpp

@@ -58,32 +58,38 @@ typet join_types(const typet &t1, const typet &t2) {
     bitvector_typet b1 = to_bitvector_type(t1);
     bitvector_typet b2 = to_bitvector_type(t2);
 
-    if (is_unsigned(b1) && is_unsigned(b2)) {
+    if (is_unsigned(b1) && is_unsigned(b2))
+    {
       // We just need to take the max of their widths.
-      unsigned int width = std::max(b1.get_width(), b2.get_width());
+      std::size_t width = std::max(b1.get_width(), b2.get_width());
       return unsignedbv_typet(width);
-    } else if(is_signed(b1) && is_signed(b2)) {
+    }
+    else if(is_signed(b1) && is_signed(b2))
+    {
       // Again, just need to take the max of the widths.
-      unsigned int width = std::max(b1.get_width(), b2.get_width());
+      std::size_t width = std::max(b1.get_width(), b2.get_width());
       return signedbv_typet(width);
-    } else {
+    }
+    else
+    {
       // This is the (slightly) tricky case.  If we have a signed and an
       // unsigned type, we're going to return a signed type.  And to cast
       // an unsigned type to a signed type, we need the signed type to be
       // at least one bit wider than the unsigned type we're casting from.
-      unsigned int signed_width = is_signed(t1) ? b1.get_width() :
-                                                  b2.get_width();
-      unsigned int unsigned_width = is_signed(t1) ? b2.get_width() :
-                                                    b1.get_width();
+      std::size_t signed_width = is_signed(t1) ? b1.get_width() :
+                                                 b2.get_width();
+      std::size_t unsigned_width = is_signed(t1) ? b2.get_width() :
+                                                   b1.get_width();
       //unsigned_width++;
 
-      unsigned int width = std::max(signed_width, unsigned_width);
+      std::size_t width = std::max(signed_width, unsigned_width);
 
       return signedbv_typet(width);
     }
   }
 
-  std::cerr << "Tried to join types: " << t1.to_string() << " and " <<
-    t2.to_string() << std::endl;
+  std::cerr << "Tried to join types: "
+            << t1.to_string() << " and " << t2.to_string()
+            << std::endl;
   assert(!"Couldn't join types");
 }