Various bits of cleanup, to be broken up into sensible commits

Author: tautschnig

src/ansi-c/expr2c.cpp

@@ -2218,9 +2218,8 @@ std::string expr2ct::convert_array(
         break;
 
       assert(it->is_constant());
-      mp_integer i;
-      to_integer(*it, i);
-      unsigned int ch=integer2unsigned(i);
+      const auto i = numeric_cast<mp_integer>(*it);
+      const unsigned int ch = numeric_cast_v<unsigned>(*i);
 
       if(last_was_hex)
       {

src/ansi-c/padding.cpp

@@ -35,12 +35,15 @@ mp_integer alignment(const typet &type, const namespacet &ns)
   const exprt &given_alignment=
     static_cast<const exprt &>(type.find(ID_C_alignment));
 
-  mp_integer a_int;
+  mp_integer a_int = 0;
 
   // we trust it blindly, no matter how nonsensical
-  if(given_alignment.is_nil() ||
-     to_integer(given_alignment, a_int))
-    a_int=0;
+  if(given_alignment.is_not_nil())
+  {
+    const auto a = numeric_cast<mp_integer>(given_alignment);
+    if(a.has_value())
+      a_int = *a;
+  }
 
   // alignment but no packing
   if(a_int>0 && !type.get_bool(ID_C_packed))
@@ -250,17 +253,16 @@ void add_padding(struct_typet &type, const namespacet &ns)
   }
 
   // any explicit alignment for the struct?
-  if(type.find(ID_C_alignment).is_not_nil())
+  const exprt &alignment =
+    static_cast<const exprt &>(type.find(ID_C_alignment));
+  if(alignment.is_not_nil())
   {
-    const exprt &alignment=
-      static_cast<const exprt &>(type.find(ID_C_alignment));
     if(alignment.id()!=ID_default)
     {
-      exprt tmp=alignment;
-      simplify(tmp, ns);
-      mp_integer tmp_i;
-      if(!to_integer(tmp, tmp_i) && tmp_i>max_alignment)
-        max_alignment=tmp_i;
+      const auto tmp_i = numeric_cast<mp_integer>(simplify_expr(alignment, ns));
+
+      if(tmp_i.has_value() && *tmp_i > max_alignment)
+        max_alignment = *tmp_i;
     }
   }
   // Is the struct packed, without any alignment specification?

src/ansi-c/type2name.cpp

@@ -178,14 +178,19 @@ static std::string type2name(
   }
   else if(type.id()==ID_array)
   {
-    const array_typet &t=to_array_type(type);
-    mp_integer size;
-    if(t.size().id()==ID_symbol)
-      result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
-    else if(to_integer(t.size(), size))
-      result+="ARR?";
+    const exprt &size = to_array_type(type).size();
+
+    if(size.id()==ID_symbol)
+      result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
     else
-      result+="ARR"+integer2string(size);
+    {
+      const auto size_int = numeric_cast<mp_integer>(size);
+
+      if(!size_int.has_value())
+        result += "ARR?";
+      else
+        result += "ARR" + integer2string(*size_int);
+    }
   }
   else if(type.id()==ID_symbol ||
           type.id()==ID_c_enum_tag ||

src/cpp/cpp_token_buffer.cpp

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <ansi-c/ansi_c_y.tab.h>
 #include <ansi-c/ansi_c_parser.h>
 
-int cpp_token_buffert::LookAhead(unsigned offset)
+int cpp_token_buffert::LookAhead(std::size_t offset)
 {
   assert(current_pos<=token_vector.size());
 
@@ -56,7 +56,7 @@ int cpp_token_buffert::get_token()
   return kind;
 }
 
-int cpp_token_buffert::LookAhead(unsigned offset, cpp_tokent &token)
+int cpp_token_buffert::LookAhead(std::size_t offset, cpp_tokent &token)
 {
   assert(current_pos<=token_vector.size());
 

src/cpp/cpp_token_buffer.h

@@ -25,12 +25,12 @@ class cpp_token_buffert
   {
   }
 
-  typedef unsigned int post;
+  typedef std::size_t post;
 
-  int LookAhead(unsigned offset);
+  int LookAhead(std::size_t offset);
   int get_token(cpp_tokent &token);
   int get_token();
-  int LookAhead(unsigned offset, cpp_tokent &token);
+  int LookAhead(std::size_t offset, cpp_tokent &token);
 
   post Save();
   void Restore(post pos);

src/cpp/cpp_typecheck_code.cpp

@@ -25,12 +25,12 @@ void cpp_typecheckt::typecheck_code(codet &code)
 
   if(statement==ID_try_catch)
   {
-    code.type()=code_typet();
+    code.type() = code_typet({}, empty_typet());
     typecheck_try_catch(code);
   }
   else if(statement==ID_member_initializer)
   {
-    code.type()=code_typet();
+    code.type() = code_typet({}, empty_typet());
     typecheck_member_initializer(code);
   }
   else if(statement==ID_msc_if_exists ||

src/cpp/cpp_typecheck_constructor.cpp

@@ -437,7 +437,7 @@ void cpp_typecheckt::default_assignop_value(
   declarator.value().add_source_location()=source_location;
   declarator.value().id(ID_code);
   declarator.value().set(ID_statement, ID_block);
-  declarator.value().type()=code_typet();
+  declarator.value().type() = code_typet({}, empty_typet());
 
   exprt &block=declarator.value();
 
@@ -484,13 +484,11 @@ void cpp_typecheckt::default_assignop_value(
         continue;
       }
 
-      mp_integer size;
-      bool to_int=to_integer(size_expr, size);
-      CHECK_RETURN(!to_int);
-      CHECK_RETURN(size>=0);
+      const auto size = numeric_cast<mp_integer>(size_expr);
+      CHECK_RETURN(!size.has_value());
+      CHECK_RETURN(*size >= 0);
 
-      exprt::operandst empty_operands;
-      for(mp_integer i=0; i < size; ++i)
+      for(mp_integer i = 0; i < *size; ++i)
         copy_array(source_location, mem_name, i, arg_name, block);
     }
     else
@@ -503,7 +501,7 @@ void cpp_typecheckt::default_assignop_value(
   ret_code.operands().push_back(exprt(ID_dereference));
   ret_code.op0().operands().push_back(exprt("cpp-this"));
   ret_code.set(ID_statement, ID_return);
-  ret_code.type()=code_typet();
+  ret_code.type() = code_typet({}, empty_typet());
 }
 
 /// Check a constructor initialization-list. An initializer has to be a data

src/cpp/parse.cpp

@@ -5275,9 +5275,8 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
             << "Parser::rTypeNameOrFunctionType 2\n";
   #endif
 
-  code_typet type;
-
-  if(!rCastOperatorName(type.return_type()))
+  typet return_type;
+  if(!rCastOperatorName(return_type))
     return false;
 
   #ifdef DEBUG
@@ -5287,7 +5286,7 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
 
   if(lex.LookAhead(0)!='(')
   {
-    tname.swap(type.return_type());
+    tname.swap(return_type);
 
     if(!optPtrOperator(tname))
       return false;
@@ -5300,6 +5299,7 @@ bool Parser::rTypeNameOrFunctionType(typet &tname)
             << "Parser::rTypeNameOrFunctionType 4\n";
   #endif
 
+  code_typet type({}, return_type);
   cpp_tokent op;
   lex.get_token(op);
 

src/goto-cc/linker_script_merge.cpp

@@ -415,7 +415,7 @@ int linker_script_merget::ls_data2instructions(
 
 
     // Array symbol_exprt
-    std::size_t array_size=integer2size_t(string2integer(d["size"].value));
+    mp_integer array_size = string2integer(d["size"].value);
     if(array_size > MAX_FLATTENED_ARRAY_SIZE)
     {
       warning() << "Object section '" << d["section"].value << "' of size "
@@ -434,7 +434,7 @@ int linker_script_merget::ls_data2instructions(
     array_loc.set_file(linker_script);
     std::ostringstream array_comment;
     array_comment << "Object section '" << d["section"].value << "' of size "
-            << integer2unsigned(array_size) << " bytes";
+                  << array_size << " bytes";
     array_loc.set_comment(array_comment.str());
     array_expr.add_source_location()=array_loc;
 

src/goto-instrument/cover_basic_blocks.cpp

@@ -61,7 +61,7 @@ cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program)
     // update lines belonging to block
     const irep_idt &line = it->source_location.get_line();
     if(!line.empty())
-      block_info.lines.insert(unsafe_string2unsigned(id2string(line)));
+      block_info.lines.insert(unsafe_string2size_t(id2string(line)));
 
     // set representative program location to instrument
     if(
@@ -155,7 +155,7 @@ void cover_basic_blockst::update_covered_lines(block_infot &block_info)
 
   const auto &cover_set = block_info.lines;
   INVARIANT(!cover_set.empty(), "covered lines set must not be empty");
-  std::vector<unsigned> line_list(cover_set.begin(), cover_set.end());
+  std::vector<std::size_t> line_list(cover_set.begin(), cover_set.end());
 
   std::string covered_lines = format_number_range(line_list);
   block_info.source_location.set_basic_block_covered_lines(covered_lines);

src/goto-instrument/cover_instrument_mcdc.cpp

@@ -360,7 +360,7 @@ void remove_repetition(std::set<exprt> &exprs)
       {
         std::set<signed> signs1 = sign_of_expr(c, x);
         std::set<signed> signs2 = sign_of_expr(c, y);
-        int s1 = signs1.size(), s2 = signs2.size();
+        std::size_t s1 = signs1.size(), s2 = signs2.size();
         // it is easy to check non-equivalence;
         if(s1 != s2)
         {

src/goto-instrument/document_properties.cpp

@@ -73,7 +73,7 @@ class document_propertiest
 
 void document_propertiest::strip_space(std::list<linet> &lines)
 {
-  unsigned strip=50;
+  std::size_t strip=50;
 
   for(std::list<linet>::const_iterator it=lines.begin();
       it!=lines.end(); it++)

src/goto-instrument/function.cpp

@@ -34,10 +34,7 @@ code_function_callt function_to_call(
     typet p=pointer_type(char_type());
     p.subtype().set(ID_C_constant, true);
 
-    code_typet function_type;
-    function_type.return_type()=empty_typet();
-    function_type.parameters().push_back(
-      code_typet::parametert(p));
+    const code_typet function_type({code_typet::parametert(p)}, empty_typet());
 
     symbolt new_symbol;
     new_symbol.name=id;

src/goto-instrument/goto_program2code.cpp

@@ -774,15 +774,15 @@ bool goto_program2codet::set_block_end_points(
   cases_listt &cases,
   std::set<unsigned> &processed_locations)
 {
-  std::map<goto_programt::const_targett, std::size_t> targets_done;
+  std::set<goto_programt::const_targett> targets_done;
 
   for(cases_listt::iterator it=cases.begin();
       it!=cases.end();
       ++it)
   {
     // some branch targets may be shared by multiple branch instructions,
     // as in case 1: case 2: code; we build a nested code_switch_caset
-    if(targets_done.find(it->case_start)!=targets_done.end())
+    if(!targets_done.insert(it->case_start).second)
       continue;
 
     // compute the block that belongs to this case
@@ -818,8 +818,6 @@ bool goto_program2codet::set_block_end_points(
 
       it->case_last=case_end;
     }
-
-    targets_done[it->case_start]=1;
   }
 
   return false;
@@ -970,7 +968,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch(
        it->case_last->location_number > max_target->location_number)
       max_target=it->case_last;
 
-  std::map<goto_programt::const_targett, unsigned> targets_done;
+  std::map<goto_programt::const_targett, std::size_t> targets_done;
   loop_last_stack.push_back(std::make_pair(max_target, false));
 
   // iterate over all <branch conditions, branch instruction, branch target>

src/goto-instrument/wmm/data_dp.cpp

@@ -120,7 +120,7 @@ void data_dpt::dp_merge()
   if(data.size()<2)
     return;
 
-  unsigned initial_size=data.size();
+  std::size_t initial_size=data.size();
 
   unsigned from=0;
   unsigned to=0;

src/goto-instrument/wmm/goto2graph.cpp

@@ -115,8 +115,8 @@ unsigned instrumentert::goto2graph_cfg(
                    << visitor.max_thread << messaget::eom;
 
   /* SCCs which could host critical cycles */
-  unsigned interesting_sccs=0;
-  for(unsigned i=0; i<num_sccs; i++)
+  std::size_t interesting_sccs=0;
+  for(std::size_t i=0; i<num_sccs; i++)
     if(egraph_SCCs[i].size()>3)
       interesting_sccs++;
 

src/goto-instrument/wmm/goto2graph.h

@@ -289,7 +289,7 @@ class instrumentert
 
   /* critical cycles per SCC */
   std::vector<std::set<event_grapht::critical_cyclet> > set_of_cycles_per_SCC;
-  unsigned num_sccs;
+  std::size_t num_sccs;
 
   /* map from function to begin and end of the corresponding part of the
      graph */

src/goto-instrument/wmm/weak_memory.cpp

@@ -161,9 +161,9 @@ void weak_memory(
   {
     instrumenter.collect_cycles_by_SCCs(model);
     message.status()<<"cycles collected: "<<messaget::eom;
-    unsigned interesting_scc = 0;
-    unsigned total_cycles = 0;
-    for(unsigned i=0; i<instrumenter.num_sccs; i++)
+    std::size_t interesting_scc = 0;
+    std::size_t total_cycles = 0;
+    for(std::size_t i=0; i<instrumenter.num_sccs; i++)
       if(instrumenter.egraph_SCCs[i].size()>=4)
       {
         message.status()<<"SCC #"<<i<<": "

src/goto-programs/goto_convert.cpp

@@ -171,12 +171,15 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       bool stack_is_prefix=true;
       if(label_stack.size()>goto_stack.size())
         stack_is_prefix=false;
-      for(std::size_t i=0, ilim=label_stack.size();
-          i!=ilim && stack_is_prefix;
-          ++i)
+      auto label_stack_it = label_stack.begin();
+      for(const auto &g : goto_stack)
       {
-        if(goto_stack[i]!=label_stack[i])
+        if(!stack_is_prefix || label_stack_it == label_stack.end())
+          break;
+        else if(g != *label_stack_it)
           stack_is_prefix=false;
+
+        ++label_stack_it;
       }
 
       if(!stack_is_prefix)

src/goto-programs/goto_trace.cpp

@@ -214,11 +214,11 @@ void trace_value(
       << "\n";
 }
 
-void show_state_header(
+static void show_state_header(
   std::ostream &out,
   const goto_trace_stept &state,
   const source_locationt &source_location,
-  unsigned step_nr)
+  std::size_t step_nr)
 {
   out << "\n";
 
@@ -249,7 +249,7 @@ void show_goto_trace(
   const namespacet &ns,
   const goto_tracet &goto_trace)
 {
-  unsigned prev_step_nr=0;
+  std::size_t prev_step_nr=0;
   bool first_step=true;
 
   for(const auto &step : goto_trace.steps)