C++11 cleanup

src/aa-path-symex/locs.h

@@ -104,12 +104,4 @@ class target_to_loc_mapt
   mapt map;
 };
 
-#define forall_locs(it, locs) \
-  for(locst::loc_vectort::const_iterator it=(locs).loc_vector.begin(); \
-      it!=(locs).loc_vector.end(); it++)
-
-#define Forall_locs(it, locs) \
-  for(exprt::operandst::iterator it=(expr).loc_vector.begin(); \
-      it!=(locs).loc_vector.end(); it++)
-
 #endif // CPROVER_AA_PATH_SYMEX_LOCS_H

src/aa-path-symex/path_symex.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/simplify_expr.h>
 #include <util/byte_operators.h>
-#include <util/i2string.h>
 #include <util/pointer_offset_size.h>
 #include <util/expr_util.h>
 #include <util/base_type.h>
@@ -319,7 +318,7 @@ void path_symext::symex_malloc(
 
       symbolt size_symbol;
 
-      size_symbol.base_name="dynamic_object_size"+i2string(dynamic_count);
+      size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_count);
       size_symbol.name="symex::"+id2string(size_symbol.base_name);
       size_symbol.is_lvalue=true;
       size_symbol.type=tmp_size.type();
@@ -338,7 +337,7 @@ void path_symext::symex_malloc(
   // value
   symbolt value_symbol;
 
-  value_symbol.base_name="dynamic_object"+i2string(state.var_map.dynamic_count);
+  value_symbol.base_name="dynamic_object"+std::to_string(state.var_map.dynamic_count);
   value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name);
   value_symbol.is_lvalue=true;
   value_symbol.type=object_type;

src/aa-path-symex/path_symex_state.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/decision_procedure.h>
-#include <util/i2string.h>
 
 #include <ansi-c/c_types.h>
 
@@ -328,7 +327,7 @@ exprt path_symex_statet::instantiate_rec(
 
     if(statement==ID_nondet)
     {
-      irep_idt id="symex::nondet"+i2string(var_map.nondet_count);
+      irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
       var_map.nondet_count++;
       return symbol_exprt(id, src.type());
     }

src/aa-path-symex/var_map.cpp

@@ -8,7 +8,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/symbol.h>
 #include <util/std_expr.h>
-#include <util/i2string.h>
 #include <util/prefix.h>
 
 #include "var_map.h"
@@ -115,5 +114,5 @@ Function: var_mapt::var_infot::ssa_identifier
 irep_idt var_mapt::var_infot::ssa_identifier() const
 {
   return id2string(full_identifier)+
-         "#"+i2string(ssa_counter);
+         "#"+std::to_string(ssa_counter);
 }

src/analyses/ai.h

@@ -280,7 +280,7 @@ class ait:public ai_baset
   }
 
 protected:
-  typedef hash_map_cont<locationt, domainT, const_target_hash> state_mapt;
+  typedef std::unordered_map<locationt, domainT, const_target_hash> state_mapt;
   state_mapt state_map;
 
   // this one creates states, if need be

src/analyses/dirty.h

@@ -11,13 +11,15 @@ Date: March 2013
 #ifndef CPROVER_ANALYSES_DIRTY_H
 #define CPROVER_ANALYSES_DIRTY_H
 
+#include <unordered_set>
+
 #include <util/std_expr.h>
 #include <goto-programs/goto_functions.h>
 
 class dirtyt
 {
 public:
-  typedef hash_set_cont<irep_idt, irep_id_hash> id_sett;
+  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   typedef goto_functionst::goto_functiont goto_functiont;
 
   explicit dirtyt(const goto_functiont &goto_function)

src/analyses/flow_insensitive_analysis.cpp

@@ -309,7 +309,7 @@ bool flow_insensitive_analysis_baset::visit(
 
 //  {
 //    static unsigned state_cntr=0;
-//    std::string s("pastate"); s += i2string(state_cntr);
+//    std::string s("pastate"); s += std::to_string(state_cntr);
 //    std::ofstream f(s.c_str());
 //    goto_program.output_instruction(ns, "", f, l);
 //    f << std::endl;

src/analyses/flow_insensitive_analysis.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <queue>
 #include <map>
 #include <iosfwd>
+#include <unordered_set>
 
 #include <goto-programs/goto_functions.h>
 
@@ -44,7 +45,7 @@ class flow_insensitive_abstract_domain_baset
   {
   }
 
-  typedef hash_set_cont<exprt, irep_hash> expr_sett;
+  typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
   virtual void get_reference_set(
     const namespacet &ns,

src/analyses/goto_rw.h

@@ -84,7 +84,7 @@ class rw_range_sett
   #ifdef USE_DSTRING
   typedef std::map<irep_idt, range_domain_baset*> objectst;
   #else
-  typedef hash_map_cont<irep_idt, range_domain_baset*, string_hash> objectst;
+  typedef std::unordered_map<irep_idt, range_domain_baset*, string_hash> objectst;
   #endif
 
   virtual ~rw_range_sett();

src/analyses/interval_domain.h

@@ -11,9 +11,9 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/ieee_float.h>
 #include <util/mp_arith.h>
-#include <util/interval_template.h>
 
 #include "ai.h"
+#include "interval_template.h"
 
 typedef interval_template<mp_integer> integer_intervalt;
 typedef interval_template<ieee_floatt> ieee_float_intervalt;

src/util/interval_template.h → src/analyses/interval_template.h

@@ -10,9 +10,9 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_INTERVAL_TEMPLATE_H
 
 #include <algorithm>
-#include <ostream>
+#include <iosfwd>
 
-#include "threeval.h"
+#include <util/threeval.h>
 
 template<class T> class interval_template
 {

src/analyses/invariant_propagation.cpp

@@ -78,7 +78,7 @@ void invariant_propagationt::add_objects(
   goto_program.get_decl_identifiers(locals);
 
   // cache the list for the locals to speed things up
-  typedef hash_map_cont<irep_idt, object_listt, irep_id_hash> object_cachet;
+  typedef std::unordered_map<irep_idt, object_listt, irep_id_hash> object_cachet;
   object_cachet object_cache;
 
   for(goto_programt::instructionst::const_iterator
@@ -226,7 +226,7 @@ void invariant_propagationt::add_objects(
     const goto_programt &goto_program=f_it->second.body;
 
     // cache the list for the locals to speed things up
-    typedef hash_map_cont<irep_idt, object_listt, irep_id_hash> object_cachet;
+    typedef std::unordered_map<irep_idt, object_listt, irep_id_hash> object_cachet;
     object_cachet object_cache;
 
     for(goto_programt::instructionst::const_iterator

src/analyses/invariant_set.h

@@ -14,10 +14,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/union_find.h>
 #include <util/threeval.h>
 #include <util/mp_arith.h>
-#include <util/interval_template.h>
 
 #include <pointer-analysis/value_sets.h>
 
+#include "interval_template.h"
+
 class inv_object_storet
 {
 public:

src/analyses/reaching_definitions.h

@@ -47,7 +47,7 @@ class sparse_bitvector_analysist
 protected:
   typedef typename std::map<V, std::size_t> inner_mapt;
   std::vector<typename inner_mapt::const_iterator> values;
-  hash_map_cont<irep_idt, inner_mapt, irep_id_hash> value_map;
+  std::unordered_map<irep_idt, inner_mapt, irep_id_hash> value_map;
 };
 
 struct reaching_definitiont
@@ -135,14 +135,14 @@ class rd_range_domaint:public ai_domain_baset
   #ifdef USE_DSTRING
   typedef std::map<irep_idt, values_innert> valuest;
   #else
-  typedef hash_map_cont<irep_idt, values_innert, irep_id_hash> valuest;
+  typedef std::unordered_map<irep_idt, values_innert, irep_id_hash> valuest;
   #endif
   valuest values;
 
   #ifdef USE_DSTRING
   typedef std::map<irep_idt, ranges_at_loct> export_cachet;
   #else
-  typedef hash_map_cont<irep_idt, ranges_at_loct, irep_id_hash>
+  typedef std::unordered_map<irep_idt, ranges_at_loct, irep_id_hash>
     export_cachet;
   #endif
   mutable export_cachet export_cache;

src/analyses/static_analysis.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <map>
 #include <iosfwd>
+#include <unordered_set>
 
 #include <goto-programs/goto_functions.h>
 
@@ -60,7 +61,7 @@ class domain_baset
   {
   }
 
-  typedef hash_set_cont<exprt, irep_hash> expr_sett;
+  typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
   // will go away
   virtual void get_reference_set(

src/ansi-c/Makefile

@@ -14,7 +14,7 @@ SRC = c_typecast.cpp ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_parser.cpp \
       literals/convert_float_literal.cpp \
       literals/convert_character_literal.cpp \
       literals/convert_integer_literal.cpp \
-      literals/convert_string_literal.cpp
+      literals/convert_string_literal.cpp c_misc.cpp
 
 INCLUDES= -I ..
 

src/ansi-c/ansi_c_entry_point.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
-#include <util/i2string.h>
 
 #include <ansi-c/c_types.h>
 #include <ansi-c/string_constant.h>
@@ -52,7 +51,7 @@ exprt::operandst build_function_environment(
   for(const auto & p : parameters)
   {
     irep_idt base_name=p.get_base_name();
-    if(base_name.empty()) base_name="argument#"+i2string(i);
+    if(base_name.empty()) base_name="argument#"+std::to_string(i);
     irep_idt identifier=id2string(goto_functionst::entry_point())+
       "::"+id2string(base_name);
 

src/ansi-c/ansi_c_internal_additions.cpp

@@ -6,7 +6,6 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/i2string.h>
 #include <util/config.h>
 
 #include "ansi_c_internal_additions.h"
@@ -94,7 +93,7 @@ static std::string architecture_string(int value, const char *s)
 {
   return std::string("const int __CPROVER_architecture_")+
          std::string(s)+
-         "="+i2string(value)+";\n";
+         "="+std::to_string(value)+";\n";
 }
 
 /*******************************************************************\
@@ -193,7 +192,7 @@ void ansi_c_internal_additions(std::string &code)
     "double __CPROVER_inf(void);\n"
     "float __CPROVER_inff(void);\n"
     "long double __CPROVER_infl(void);\n"
-    "int __CPROVER_thread_local __CPROVER_rounding_mode="+i2string(config.ansi_c.rounding_mode)+";\n"
+    "int __CPROVER_thread_local __CPROVER_rounding_mode="+std::to_string(config.ansi_c.rounding_mode)+";\n"
 
     // absolute value
     "int __CPROVER_abs(int x);\n"

src/ansi-c/ansi_c_parser.h

@@ -13,9 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/parser.h>
 #include <util/expr.h>
-#include <util/hash_cont.h>
 #include <util/string_hash.h>
-#include <util/i2string.h>
 #include <util/mp_arith.h>
 #include <util/config.h>
 

src/ansi-c/ansi_c_scope.h

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_ANSI_C_SCOPE_H
 #define CPROVER_ANSI_C_ANSI_C_SCOPE_H
 
-#include <util/hash_cont.h>
 #include <util/irep.h>
 
 typedef enum { ANSI_C_UNKNOWN, ANSI_C_SYMBOL, ANSI_C_TYPEDEF,
@@ -31,7 +30,7 @@ class ansi_c_scopet
 public:
   // This maps "scope names" (tag-X, label-X, X) to
   // ansi_c_identifiert.
-  typedef hash_map_cont<irep_idt, ansi_c_identifiert, irep_id_hash> name_mapt;
+  typedef std::unordered_map<irep_idt, ansi_c_identifiert, irep_id_hash> name_mapt;
   name_mapt name_map;
 
   std::string prefix;

src/util/c_misc.cpp → src/ansi-c/c_misc.cpp

@@ -28,7 +28,7 @@ Function: MetaChar
 
 \*******************************************************************/
 
-void MetaChar(std::string &out, char c, bool inString)
+static void MetaChar(std::string &out, char c, bool inString)
 {
   switch(c)
   {
@@ -101,6 +101,7 @@ void MetaChar(std::string &out, char c, bool inString)
   }
 }
 
+#if 0
 /*******************************************************************\
 
 Function: MetaChar
@@ -113,12 +114,13 @@ Function: MetaChar
 
 \*******************************************************************/
 
-std::string MetaChar(char c)
+static std::string MetaChar(char c)
 {
   std::string result;
   MetaChar(result, c, false);
   return result;
 }
+#endif
 
 /*******************************************************************\
 

src/util/c_misc.h → src/ansi-c/c_misc.h

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <string>
 
-std::string MetaChar(char c);
 std::string MetaString(const std::string &in);
 
 #endif // CPROVER_UTIL_C_MISC_H

src/ansi-c/c_preprocess.cpp

@@ -22,7 +22,6 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 
 #include <util/config.h>
-#include <util/i2string.h>
 #include <util/message.h>
 #include <util/tempfile.h>
 #include <util/unicode.h>
@@ -769,7 +768,7 @@ bool c_preprocess_gcc_clang(
 
   command +=" -E -undef -D__CPROVER__";
 
-  command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
+  command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
 
   command+=" -D__DBL_MIN_EXP__=\"(-1021)\"";
   command+=" -D__FLT_MIN__=1.17549435e-38F";
@@ -1087,9 +1086,9 @@ bool c_preprocess_arm(
 
   command="armcc -E -D__CPROVER__";
 
-//  command+=" -D__sizeof_int="+i2string(config.ansi_c.int_width/8);
-//  command+=" -D__sizeof_long="+i2string(config.ansi_c.long_int_width/8);
-//  command+=" -D__sizeof_ptr="+i2string(config.ansi_c.pointer_width/8);
+//  command+=" -D__sizeof_int="+std::to_string(config.ansi_c.int_width/8);
+//  command+=" -D__sizeof_long="+std::to_string(config.ansi_c.long_int_width/8);
+//  command+=" -D__sizeof_ptr="+std::to_string(config.ansi_c.pointer_width/8);
   //command+=" -D__EDG_VERSION__=308";
   //command+=" -D__EDG__";
 //  command+=" -D__CC_ARM=1";
@@ -1104,7 +1103,7 @@ bool c_preprocess_arm(
 
   if(config.ansi_c.os!=configt::ansi_ct::ost::OS_WIN)
   {
-    command+=" -D__WORDSIZE="+i2string(config.ansi_c.pointer_width);
+    command+=" -D__WORDSIZE="+std::to_string(config.ansi_c.pointer_width);
 
     if(config.ansi_c.int_width==16)
       command+=GCC_DEFINES_16;