diff --git a/src/aa-path-symex/locs.h b/src/aa-path-symex/locs.h index 9d5f45730fc..75e0ae29f7e 100644 --- a/src/aa-path-symex/locs.h +++ b/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 diff --git a/src/aa-path-symex/path_symex.cpp b/src/aa-path-symex/path_symex.cpp index 6ea307ca058..83e56461136 100644 --- a/src/aa-path-symex/path_symex.cpp +++ b/src/aa-path-symex/path_symex.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -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; diff --git a/src/aa-path-symex/path_symex_state.cpp b/src/aa-path-symex/path_symex_state.cpp index 08397535741..c0d316ced05 100644 --- a/src/aa-path-symex/path_symex_state.cpp +++ b/src/aa-path-symex/path_symex_state.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include @@ -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()); } diff --git a/src/aa-path-symex/var_map.cpp b/src/aa-path-symex/var_map.cpp index a487db47bfd..941a8645a6f 100644 --- a/src/aa-path-symex/var_map.cpp +++ b/src/aa-path-symex/var_map.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #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); } diff --git a/src/analyses/ai.h b/src/analyses/ai.h index af93bef3a8e..41838836da3 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -280,7 +280,7 @@ class ait:public ai_baset } protected: - typedef hash_map_cont state_mapt; + typedef std::unordered_map state_mapt; state_mapt state_map; // this one creates states, if need be diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index e1d5b6aa64e..61ab0b0cb40 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -11,13 +11,15 @@ Date: March 2013 #ifndef CPROVER_ANALYSES_DIRTY_H #define CPROVER_ANALYSES_DIRTY_H +#include + #include #include class dirtyt { public: - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; typedef goto_functionst::goto_functiont goto_functiont; explicit dirtyt(const goto_functiont &goto_function) diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index e4782b76e73..77333faf4e8 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/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; diff --git a/src/analyses/flow_insensitive_analysis.h b/src/analyses/flow_insensitive_analysis.h index 00c8ad4f798..3c64f5a0f63 100644 --- a/src/analyses/flow_insensitive_analysis.h +++ b/src/analyses/flow_insensitive_analysis.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -44,7 +45,7 @@ class flow_insensitive_abstract_domain_baset { } - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; virtual void get_reference_set( const namespacet &ns, diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index 8aa1aa33f57..f4b289e9491 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -84,7 +84,7 @@ class rw_range_sett #ifdef USE_DSTRING typedef std::map objectst; #else - typedef hash_map_cont objectst; + typedef std::unordered_map objectst; #endif virtual ~rw_range_sett(); diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 9dd73b992f9..7f1059b63b2 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "ai.h" +#include "interval_template.h" typedef interval_template integer_intervalt; typedef interval_template ieee_float_intervalt; diff --git a/src/util/interval_template.h b/src/analyses/interval_template.h similarity index 98% rename from src/util/interval_template.h rename to src/analyses/interval_template.h index 068edb83e5c..97ccf7a10d7 100644 --- a/src/util/interval_template.h +++ b/src/analyses/interval_template.h @@ -10,9 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_INTERVAL_TEMPLATE_H #include -#include +#include -#include "threeval.h" +#include template class interval_template { diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index 56e285247e0..d73ad724eee 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/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 object_cachet; + typedef std::unordered_map 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 object_cachet; + typedef std::unordered_map object_cachet; object_cachet object_cache; for(goto_programt::instructionst::const_iterator diff --git a/src/analyses/invariant_set.h b/src/analyses/invariant_set.h index b24d0c75ab8..fc9ad07d59f 100644 --- a/src/analyses/invariant_set.h +++ b/src/analyses/invariant_set.h @@ -14,10 +14,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include +#include "interval_template.h" + class inv_object_storet { public: diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 7b29b9e03db..90c91df8c5e 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -47,7 +47,7 @@ class sparse_bitvector_analysist protected: typedef typename std::map inner_mapt; std::vector values; - hash_map_cont value_map; + std::unordered_map value_map; }; struct reaching_definitiont @@ -135,14 +135,14 @@ class rd_range_domaint:public ai_domain_baset #ifdef USE_DSTRING typedef std::map valuest; #else - typedef hash_map_cont valuest; + typedef std::unordered_map valuest; #endif valuest values; #ifdef USE_DSTRING typedef std::map export_cachet; #else - typedef hash_map_cont + typedef std::unordered_map export_cachet; #endif mutable export_cachet export_cache; diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h index f25387d08f7..3e49425bbeb 100644 --- a/src/analyses/static_analysis.h +++ b/src/analyses/static_analysis.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -60,7 +61,7 @@ class domain_baset { } - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; // will go away virtual void get_reference_set( diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 5d6381c6b00..bed65d0d7b6 100644 --- a/src/ansi-c/Makefile +++ b/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 .. diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 1acfb7d4459..de3b4bc675c 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -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); diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index ca4cf92f637..b41c436d0da 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #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" diff --git a/src/ansi-c/ansi_c_parser.h b/src/ansi-c/ansi_c_parser.h index 7e078abd7e5..2b35b56f34a 100644 --- a/src/ansi-c/ansi_c_parser.h +++ b/src/ansi-c/ansi_c_parser.h @@ -13,9 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include -#include #include #include diff --git a/src/ansi-c/ansi_c_scope.h b/src/ansi-c/ansi_c_scope.h index c23f5eb2363..3e1d81e09f8 100644 --- a/src/ansi-c/ansi_c_scope.h +++ b/src/ansi-c/ansi_c_scope.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_ANSI_C_SCOPE_H #define CPROVER_ANSI_C_ANSI_C_SCOPE_H -#include #include 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 name_mapt; + typedef std::unordered_map name_mapt; name_mapt name_map; std::string prefix; diff --git a/src/util/c_misc.cpp b/src/ansi-c/c_misc.cpp similarity index 94% rename from src/util/c_misc.cpp rename to src/ansi-c/c_misc.cpp index 01fc2347dce..80d63e75717 100644 --- a/src/util/c_misc.cpp +++ b/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 /*******************************************************************\ diff --git a/src/util/c_misc.h b/src/ansi-c/c_misc.h similarity index 92% rename from src/util/c_misc.h rename to src/ansi-c/c_misc.h index b40f186db1f..a315a1efab2 100644 --- a/src/util/c_misc.h +++ b/src/ansi-c/c_misc.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -std::string MetaChar(char c); std::string MetaString(const std::string &in); #endif // CPROVER_UTIL_C_MISC_H diff --git a/src/ansi-c/c_preprocess.cpp b/src/ansi-c/c_preprocess.cpp index 4f383e99828..00b82f1414d 100644 --- a/src/ansi-c/c_preprocess.cpp +++ b/src/ansi-c/c_preprocess.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -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; diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index be7c58cc197..8d81099916e 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "c_typecheck_base.h" #include "expr2c.h" @@ -655,7 +654,7 @@ void c_typecheck_baset::typecheck_function_body(symbolt &symbol) // may be anonymous if(p_it->get_base_name()==irep_idt()) { - irep_idt base_name="#anon"+i2string(anon_counter++); + irep_idt base_name="#anon"+std::to_string(anon_counter++); p_it->set_base_name(base_name); } diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 9d79fe18429..6e3a566fd21 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -60,7 +60,7 @@ class c_typecheck_baset: const irep_idt mode; irep_idt current_symbol_id; - typedef hash_map_cont id_type_mapt; + typedef std::unordered_map id_type_mapt; id_type_mapt parameter_map; // overload to use language specific syntax @@ -253,7 +253,7 @@ class c_typecheck_baset: src.id()==ID_c_bit_field; } - typedef hash_map_cont asm_label_mapt; + typedef std::unordered_map asm_label_mapt; asm_label_mapt asm_label_map; void apply_asm_label(const irep_idt &asm_label, symbolt &symbol); diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 94a861e7a7d..1748d5eba40 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 3002bd5c7d5..dcfb2ea5ccf 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -6,11 +6,12 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include + #include #include #include #include -#include #include #include @@ -566,7 +567,7 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type) do { - suffix="$array_size"+i2string(count); + suffix="$array_size"+std::to_string(count); temp_identifier=id2string(base_symbol.name)+suffix; count++; } @@ -909,14 +910,14 @@ void c_typecheck_baset::typecheck_compound_body( { if(it->get_name()!=irep_idt()) continue; - it->set_name("$anon"+i2string(anon_member_counter++)); + it->set_name("$anon"+std::to_string(anon_member_counter++)); it->set_anonymous(true); } // scan for duplicate members { - hash_set_cont members; + std::unordered_set members; for(struct_union_typet::componentst::iterator it=components.begin(); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 78ced9c86a3..8c69d099364 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -20,21 +20,22 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include -#include #include #include #include #include #include +#include #include #include #include #include +#include "c_misc.h" +#include "c_qualifiers.h" #include "expr2c.h" #include "c_types.h" #include "expr2c_class.h" @@ -288,11 +289,11 @@ std::string expr2ct::convert_rec( return q+"long double"+d; } const std::size_t fraction_bits=to_fixedbv_type(src).get_fraction_bits(); - return q+"__CPROVER_fixedbv["+i2string(width)+"]["+i2string(fraction_bits)+"]"+d; + return q+"__CPROVER_fixedbv["+std::to_string(width)+"]["+std::to_string(fraction_bits)+"]"+d; } else if(src.id()==ID_c_bit_field) { - std::string width=i2string(to_c_bit_field_type(src).get_width()); + std::string width=std::to_string(to_c_bit_field_type(src).get_width()); return q+convert(src.subtype())+d+" : "+width; } else if(src.id()==ID_signedbv || @@ -1894,7 +1895,7 @@ std::string expr2ct::convert_symbol( dest=src.op0().get_string(ID_identifier); else { - hash_map_cont::const_iterator + std::unordered_map::const_iterator entry=shorthands.find(id); // we might be called from conversion of a type if(entry==shorthands.end()) diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 4048cf0f9ae..836837e7846 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -10,13 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANSI_C_EXPR2C_CLASS_H #include +#include +#include -#include #include #include -#include -#include "c_qualifiers.h" +class c_qualifierst; +class namespacet; class expr2ct { @@ -39,10 +40,10 @@ class expr2ct static std::string indent_str(unsigned indent); - hash_map_cont, + std::unordered_map, irep_id_hash> ns_collision; - hash_map_cont shorthands; + std::unordered_map shorthands; unsigned sizeof_nesting; diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp index 51e7b9b6fdc..f76af2eefa6 100644 --- a/src/ansi-c/literals/convert_character_literal.cpp +++ b/src/ansi-c/literals/convert_character_literal.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "../c_types.h" @@ -71,7 +70,7 @@ exprt convert_character_literal( result=from_integer(x, type); } else - throw "wide literals with "+i2string(value.size())+ + throw "wide literals with "+std::to_string(value.size())+ " characters are not supported"; } else @@ -104,7 +103,7 @@ exprt convert_character_literal( result=from_integer(x, signed_int_type()); } else - throw "literals with "+i2string(value.size())+ + throw "literals with "+std::to_string(value.size())+ " characters are not supported"; } diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp index c7a66c60f04..a7e256bf869 100644 --- a/src/ansi-c/literals/convert_float_literal.cpp +++ b/src/ansi-c/literals/convert_float_literal.cpp @@ -91,7 +91,7 @@ exprt convert_float_literal(const std::string &src) if(integer_bits==irep_idt()) fraction_bits=width/2; // default else - fraction_bits=width-safe_string2int(id2string(integer_bits)); + fraction_bits=width-std::stoi(id2string(integer_bits)); mp_integer factor=mp_integer(1)< #include -#include #include #include #include @@ -160,7 +159,7 @@ void add_padding(struct_typet &type, const namespacet &ns) struct_typet::componentt component; component.type()=padding_type; - component.set_name("$bit_field_pad"+i2string(padding_counter++)); + component.set_name("$bit_field_pad"+std::to_string(padding_counter++)); component.set_is_padding(true); it=components.insert(it, component); @@ -181,7 +180,7 @@ void add_padding(struct_typet &type, const namespacet &ns) struct_typet::componentt component; component.type()=padding_type; - component.set_name("$bit_field_pad"+i2string(padding_counter++)); + component.set_name("$bit_field_pad"+std::to_string(padding_counter++)); component.set_is_padding(true); components.push_back(component); @@ -256,7 +255,7 @@ void add_padding(struct_typet &type, const namespacet &ns) struct_typet::componentt component; component.type()=padding_type; - component.set_name("$pad"+i2string(padding_counter++)); + component.set_name("$pad"+std::to_string(padding_counter++)); component.set_is_padding(true); it=components.insert(it, component); @@ -314,7 +313,7 @@ void add_padding(struct_typet &type, const namespacet &ns) // we insert after any final 'flexible member' struct_typet::componentt component; component.type()=padding_type; - component.set_name("$pad"+i2string(padding_counter++)); + component.set_name("$pad"+std::to_string(padding_counter++)); component.set_is_padding(true); components.push_back(component); diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index f23bff63918..c4335525180 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -2206,7 +2206,7 @@ compound_scope: /* nothing */ { unsigned prefix=++PARSER.current_scope().compound_counter; - PARSER.new_scope(i2string(prefix)+"::"); + PARSER.new_scope(std::to_string(prefix)+"::"); } ; @@ -2302,7 +2302,7 @@ iteration_statement: if(PARSER.for_has_scope) { unsigned prefix=++PARSER.current_scope().compound_counter; - PARSER.new_scope(i2string(prefix)+"::"); + PARSER.new_scope(std::to_string(prefix)+"::"); } } '(' declaration_or_expression_statement diff --git a/src/ansi-c/parser_static.inc b/src/ansi-c/parser_static.inc index 7e0936727a4..08a81c93e0d 100644 --- a/src/ansi-c/parser_static.inc +++ b/src/ansi-c/parser_static.inc @@ -2,7 +2,6 @@ #include #include #include -#include #include #include "c_types.h" diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp index f34ee45d29f..8087f6a6845 100644 --- a/src/ansi-c/type2name.cpp +++ b/src/ansi-c/type2name.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include #include #include @@ -15,7 +14,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include "type2name.h" -typedef hash_map_cont, irep_id_hash> +typedef std::unordered_map, irep_id_hash> symbol_numbert; static std::string type2name( @@ -64,7 +63,7 @@ static std::string type2name_symbol( // new entry, add definition if(entry.second) { - result="SYM#"+i2string(entry.first->second.first); + result="SYM#"+std::to_string(entry.first->second.first); result+="={"; result+=type2name(symbol->type, ns, symbol_number); result+='}'; @@ -74,7 +73,7 @@ static std::string type2name_symbol( #if 0 // in recursion, print the shorthand only else if(entry.first->second.second) - result="SYM#"+i2string(entry.first->second.first); + result="SYM#"+std::to_string(entry.first->second.first); // entering recursion else { @@ -85,7 +84,7 @@ static std::string type2name_symbol( #else // shorthand only as structs/unions are always symbols else - result="SYM#"+i2string(entry.first->second.first); + result="SYM#"+std::to_string(entry.first->second.first); #endif return result; diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 290c2f14a18..9ef6cb53dfa 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -108,7 +108,7 @@ safety_checkert::resultt bmc_all_propertiest::operator()() // this is likely an unwinding assertion property_id=id2string( it->source.pc->source_location.get_function())+".unwind."+ - i2string(it->source.pc->loop_number); + std::to_string(it->source.pc->loop_number); goal_map[property_id].description=it->comment; } else diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ba970e659c8..c0741fb700a 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -328,7 +327,7 @@ void bmct::show_program() if(!step.guard.is_true()) { languages.from_expr(step.guard, string_value); - std::cout << std::string(i2string(count).size()+3, ' '); + std::cout << std::string(std::to_string(count).size()+3, ' '); std::cout << "guard: " << string_value << "\n"; } @@ -344,7 +343,7 @@ void bmct::show_program() if(!step.guard.is_true()) { languages.from_expr(step.guard, string_value); - std::cout << std::string(i2string(count).size()+3, ' '); + std::cout << std::string(std::to_string(count).size()+3, ' '); std::cout << "guard: " << string_value << "\n"; } @@ -360,7 +359,7 @@ void bmct::show_program() if(!step.guard.is_true()) { languages.from_expr(step.guard, string_value); - std::cout << std::string(i2string(count).size()+3, ' '); + std::cout << std::string(std::to_string(count).size()+3, ' '); std::cout << "guard: " << string_value << "\n"; } @@ -385,7 +384,7 @@ void bmct::show_program() if(!step.guard.is_true()) { languages.from_expr(step.guard, string_value); - std::cout << std::string(i2string(count).size()+3, ' '); + std::cout << std::string(std::to_string(count).size()+3, ' '); std::cout << "guard: " << string_value << "\n"; } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index a99d859b19d..8206a7ec876 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index 72e45362437..df33aac8673 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -403,8 +403,8 @@ bool bmc_covert::operator()() if(goal.source_location.is_not_nil()) result["sourceLocation"]=json(goal.source_location); } - json_result["totalGoals"]=json_numbert(i2string(goal_map.size())); - json_result["goalsCovered"]=json_numbert(i2string(goals_covered)); + json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size())); + json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); json_arrayt &tests_array=json_result["tests"].make_array(); for(const auto & test : tests) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 08955180271..3514e908c04 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include diff --git a/src/cbmc/cbmc_solvers.h b/src/cbmc/cbmc_solvers.h index c834b4875d0..35ded2a5c92 100644 --- a/src/cbmc/cbmc_solvers.h +++ b/src/cbmc/cbmc_solvers.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index b4ae665079e..d97e241360e 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "symex_bmc.h" diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index 76026b3757f..07ce88834ed 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_CBMC_SYMEX_BMC_H #define CPROVER_CBMC_SYMEX_BMC_H -#include #include #include @@ -60,7 +59,7 @@ class symex_bmct: unsigned max_unwind; bool max_unwind_is_set; - typedef hash_map_cont loop_limitst; + typedef std::unordered_map loop_limitst; loop_limitst loop_limits; typedef std::map thread_loop_limitst; @@ -85,7 +84,7 @@ class symex_bmct: virtual void no_body(const irep_idt &identifier); - hash_set_cont body_warnings; + std::unordered_set body_warnings; }; #endif // CPROVER_CBMC_SYMEX_BMC_H diff --git a/src/cegis/control/value/float_helper.cpp b/src/cegis/control/value/float_helper.cpp index 712f6b226dd..4f8fb9dce9c 100644 --- a/src/cegis/control/value/float_helper.cpp +++ b/src/cegis/control/value/float_helper.cpp @@ -2,9 +2,9 @@ #include #include +#include #include #include -#include #include diff --git a/src/cegis/instrument/meta_variables.cpp b/src/cegis/instrument/meta_variables.cpp index 437bafec83e..41e163d425f 100644 --- a/src/cegis/instrument/meta_variables.cpp +++ b/src/cegis/instrument/meta_variables.cpp @@ -1,5 +1,3 @@ -#include - #include #include diff --git a/src/cegis/invariant/constant/literals_constant_strategy.cpp b/src/cegis/invariant/constant/literals_constant_strategy.cpp index 2259473be02..ec12572494b 100644 --- a/src/cegis/invariant/constant/literals_constant_strategy.cpp +++ b/src/cegis/invariant/constant/literals_constant_strategy.cpp @@ -2,7 +2,6 @@ #include #include -#include #include #include diff --git a/src/cegis/invariant/symex/learn/replace_operators.cpp b/src/cegis/invariant/symex/learn/replace_operators.cpp index b7c2dc2bdf0..e46db87a394 100644 --- a/src/cegis/invariant/symex/learn/replace_operators.cpp +++ b/src/cegis/invariant/symex/learn/replace_operators.cpp @@ -1,4 +1,4 @@ -#include +#include #include #include diff --git a/src/cpp/cpp_parser.h b/src/cpp/cpp_parser.h index 6251c377f96..f2db8e6c2f7 100644 --- a/src/cpp/cpp_parser.h +++ b/src/cpp/cpp_parser.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include #include diff --git a/src/cpp/cpp_scopes.cpp b/src/cpp/cpp_scopes.cpp index 2fa0dcc17a8..d3274b50f43 100644 --- a/src/cpp/cpp_scopes.cpp +++ b/src/cpp/cpp_scopes.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include "cpp_scopes.h" @@ -27,7 +26,7 @@ Function: cpp_scopest::new_block_scope cpp_scopet &cpp_scopest::new_block_scope() { unsigned prefix=++current_scope().compound_counter; - return new_scope(i2string(prefix), cpp_idt::BLOCK_SCOPE); + return new_scope(std::to_string(prefix), cpp_idt::BLOCK_SCOPE); } /*******************************************************************\ diff --git a/src/cpp/cpp_scopes.h b/src/cpp/cpp_scopes.h index 8ab73a98d15..0c2e0420383 100644 --- a/src/cpp/cpp_scopes.h +++ b/src/cpp/cpp_scopes.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include @@ -63,7 +62,7 @@ class cpp_scopest } // mapping from function/class/scope names to their cpp_idt - typedef hash_map_cont id_mapt; + typedef std::unordered_map id_mapt; id_mapt id_map; cpp_scopet *current_scope_ptr; diff --git a/src/cpp/cpp_type2name.cpp b/src/cpp/cpp_type2name.cpp index 95c33c778ff..ac745f89ffb 100644 --- a/src/cpp/cpp_type2name.cpp +++ b/src/cpp/cpp_type2name.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include /*******************************************************************\ @@ -28,7 +27,7 @@ static std::string do_prefix(const std::string &s) { if(s.find(',')!=std::string::npos || (s!="" && isdigit(s[0]))) - return i2string(s.size())+"_"+s; + return std::to_string(s.size())+"_"+s; return s; } diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 09706ac4795..951a72e758d 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index c6f97931455..50822b74788 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include #include diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 502a0ba3517..e60bd707691 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include #include #include #include @@ -162,7 +161,7 @@ void cpp_typecheckt::typecheck_compound_type( // most of these should be named by now; see // cpp_declarationt::name_anon_struct_union() - base_name=std::string("#anon_")+i2string(++anon_counter); + base_name=std::string("#anon_")+std::to_string(++anon_counter); type.set(ID_C_is_anonymous, true); dest_scope=&cpp_scopes.current_scope(); } @@ -654,7 +653,7 @@ void cpp_typecheckt::typecheck_compound_declarator( irep_idt base_name = arg.get_base_name(); if(base_name==irep_idt()) - base_name="arg"+i2string(i); + base_name="arg"+std::to_string(i); symbolt arg_symb; arg_symb.name = id2string(func_symb.name) + "::"+ id2string(base_name); @@ -1582,7 +1581,7 @@ void cpp_typecheckt::convert_anon_struct_union_member( } // produce an anonymous member - irep_idt base_name="#anon_member"+i2string(components.size()); + irep_idt base_name="#anon_member"+std::to_string(components.size()); irep_idt identifier= cpp_scopes.current_scope().prefix+ diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index 1d7fec47c9f..6771d58aa6c 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \********************************************************************/ -#include #include #include "cpp_typecheck.h" @@ -66,7 +65,7 @@ void cpp_typecheckt::convert_anonymous_union( new_code.reserve_operands(declaration.declarators().size()); // unnamed object - std::string identifier="#anon_union"+i2string(anon_counter++); + std::string identifier="#anon_union"+std::to_string(anon_counter++); irept name(ID_name); name.set(ID_identifier, identifier); diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index abff4131755..1813ee060d0 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index d057883067d..8e98bf1a937 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include #include diff --git a/src/cpp/cpp_typecheck_function.cpp b/src/cpp/cpp_typecheck_function.cpp index 5b3b1c1c917..e0e1c5bf822 100644 --- a/src/cpp/cpp_typecheck_function.cpp +++ b/src/cpp/cpp_typecheck_function.cpp @@ -6,8 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include -#include #include #include @@ -37,7 +35,7 @@ void cpp_typecheckt::convert_parameter( if(base_name.empty()) { - base_name="#anon_arg"+i2string(anon_counter++); + base_name="#anon_arg"+std::to_string(anon_counter++); parameter.set_base_name(base_name); } diff --git a/src/cpp/cpp_typecheck_method_bodies.cpp b/src/cpp/cpp_typecheck_method_bodies.cpp index 5635cf5005e..86e35e9f4d4 100644 --- a/src/cpp/cpp_typecheck_method_bodies.cpp +++ b/src/cpp/cpp_typecheck_method_bodies.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ -#include #include "cpp_typecheck.h" diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 81867bac864..3974920870c 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include #include #include diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index e2ef50d8fee..73997bb5aff 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu \*******************************************************************/ #include -#include #include #include "cpp_type2name.h" @@ -525,9 +524,9 @@ std::string cpp_typecheckt::class_template_identifier( if(counter!=0) identifier+=','; if(it->id()==ID_type) - identifier+="Type"+i2string(counter); + identifier+="Type"+std::to_string(counter); else - identifier+="Non_Type"+i2string(counter); + identifier+="Non_Type"+std::to_string(counter); counter++; } @@ -855,7 +854,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( assert(type.id()==ID_template); - std::string id_suffix="template::"+i2string(template_counter++); + std::string id_suffix="template::"+std::to_string(template_counter++); // produce a new scope for the template parameters cpp_scopet &template_scope= @@ -894,7 +893,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters( if(declarator.name().is_nil()) { irept name(ID_name); - name.set(ID_identifier, "anon#"+i2string(++anon_count)); + name.set(ID_identifier, "anon#"+std::to_string(++anon_count)); declarator.name()=cpp_namet(); declarator.name().get_sub().push_back(name); } diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 38779ec8581..1ed05750739 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -11,11 +11,12 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include #include -#include -#include #include #include +#include +#include +#include #include #include "expr2cpp.h" @@ -51,7 +52,7 @@ class expr2cppt:public expr2ct const c_qualifierst &qualifiers, const std::string &declarator); - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; }; /*******************************************************************\ diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index e0d1ee023ba..e07b21c55bf 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -5,7 +5,6 @@ #include #include #include -#include #include @@ -114,7 +113,7 @@ class new_scopet irep_idt get_anon_id() { ++anon_count; - return "#anon"+i2string(anon_count); + return "#anon"+std::to_string(anon_count); } std::string full_name() const @@ -536,7 +535,7 @@ bool Parser::SyntaxError() { source_locationt source_location; source_location.set_file(t[0].filename); - source_location.set_line(i2string(t[0].line_no)); + source_location.set_line(std::to_string(t[0].line_no)); std::string message="parse error before `"; diff --git a/src/goto-cc/xml_binaries/xml_irep_hashing.h b/src/goto-cc/xml_binaries/xml_irep_hashing.h index d329bfceee0..5fe4df7bb20 100644 --- a/src/goto-cc/xml_binaries/xml_irep_hashing.h +++ b/src/goto-cc/xml_binaries/xml_irep_hashing.h @@ -13,7 +13,6 @@ Date: July 2006 #include #include -#include class xml_irep_convertt { private: @@ -50,9 +49,9 @@ class xml_irep_convertt { public: class ireps_containert { public: - typedef hash_map_cont id_containert; + typedef std::unordered_map id_containert; id_containert id_container; - typedef hash_map_cont content_containert; + typedef std::unordered_map content_containert; content_containert content_container; typedef std::map id_replace_mapt; id_replace_mapt id_replace_map; diff --git a/src/goto-diff/change_impact.cpp b/src/goto-diff/change_impact.cpp index bd53f1f3727..a8ab174ee68 100644 --- a/src/goto-diff/change_impact.cpp +++ b/src/goto-diff/change_impact.cpp @@ -120,7 +120,7 @@ void full_slicert::operator()( #ifdef DEBUG_FULL_SLICERT else { - std::string c="ins:"+i2string(i_it->location_number); + std::string c="ins:"+std::to_string(i_it->location_number); c+=" req by:"; for(std::set::const_iterator req_it=cfg[e].required_by.begin(); @@ -128,7 +128,7 @@ void full_slicert::operator()( ++req_it) { if(req_it!=cfg[e].required_by.begin()) c+=","; - c+=i2string(*req_it); + c+=std::to_string(*req_it); } i_it->source_location.set_column(c); // for show-goto-functions i_it->source_location.set_comment(c); // for dump-c diff --git a/src/goto-diff/goto_diff_base.cpp b/src/goto-diff/goto_diff_base.cpp index a8f1ff4f9ea..248c161b8eb 100644 --- a/src/goto-diff/goto_diff_base.cpp +++ b/src/goto-diff/goto_diff_base.cpp @@ -6,7 +6,6 @@ Author: Peter Schrammel \*******************************************************************/ -#include #include #include "goto_diff.h" @@ -68,7 +67,7 @@ std::ostream &goto_difft::output_functions(std::ostream &out) const { json_objectt json_result; json_result["totalNumberOfFunctions"]= - json_stringt(i2string(total_functions_count)); + json_stringt(std::to_string(total_functions_count)); convert_function_group (json_result["newFunctions"].make_array(), new_functions); convert_function_group( diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 1943c7c5ced..c819d1537d0 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/src/goto-diff/goto_diff_parse_options.cpp @@ -15,7 +15,6 @@ Author: Peter Schrammel #include #include #include -#include #include #include diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h index 4f2c10be9a9..e4ed3700e87 100644 --- a/src/goto-instrument/accelerate/accelerate.h +++ b/src/goto-instrument/accelerate/accelerate.h @@ -2,7 +2,6 @@ #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H #include -#include #include #include diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 384ff5db56e..7d3227984a0 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -22,7 +22,6 @@ #include #include #include -#include #include #include #include @@ -1117,7 +1116,7 @@ symbolt acceleration_utilst::fresh_symbol(std::string base, typet type) { static int num_symbols = 0; - std::string name = base + "_" + i2string(num_symbols++); + std::string name = base + "_" + std::to_string(num_symbols++); symbolt ret; ret.module = "scratch"; ret.name = name; diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index 3275a25c687..02aba5cb387 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -5,7 +5,6 @@ #include #include -#include #include #include @@ -18,7 +17,7 @@ #include "accelerator.h" #include "cone_of_influence.h" -typedef hash_map_cont expr_mapt; +typedef std::unordered_map expr_mapt; class acceleration_utilst { public: diff --git a/src/goto-instrument/accelerate/cone_of_influence.h b/src/goto-instrument/accelerate/cone_of_influence.h index cc8ebd1cdde..59512c1853a 100644 --- a/src/goto-instrument/accelerate/cone_of_influence.h +++ b/src/goto-instrument/accelerate/cone_of_influence.h @@ -5,10 +5,9 @@ #include #include -#include #include -typedef hash_set_cont expr_sett; +typedef std::unordered_set expr_sett; void cone_of_influence(goto_programt &program, expr_sett &targets, @@ -34,7 +33,7 @@ class cone_of_influencet { expr_sett &targets); void gather_rvalues(const exprt &expr, expr_sett &rvals); - typedef hash_map_cont cone_mapt; + typedef std::unordered_map cone_mapt; cone_mapt cone_map; const goto_programt &program; diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index c22ae123fc7..65c8056b4a1 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -22,7 +22,6 @@ #include #include #include -#include #include #include #include diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index a13eb34a9c4..f8badf492ed 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -18,7 +18,6 @@ #include #include #include -#include #include #include #include diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 3ce3eaf1888..a46608f2a57 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -22,7 +22,6 @@ #include #include #include -#include #include #include #include diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 8798b18c0e2..87d1b8bf3b8 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -1,4 +1,3 @@ -#include #include #include diff --git a/src/goto-instrument/call_sequences.cpp b/src/goto-instrument/call_sequences.cpp index c39119972af..67f4dae9598 100644 --- a/src/goto-instrument/call_sequences.cpp +++ b/src/goto-instrument/call_sequences.cpp @@ -10,6 +10,7 @@ Date: April 2013 #include #include +#include #include @@ -212,7 +213,7 @@ class check_call_sequencet } }; - typedef hash_set_cont statest; + typedef std::unordered_set statest; statest states; }; diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index d05c7bdbcf8..2e66c11bf87 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -8,7 +8,6 @@ Date: February 2016 \*******************************************************************/ -#include #include #include @@ -41,7 +40,7 @@ class code_contractst unsigned temporary_counter; - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; id_sett summarized; void code_contracts(goto_functionst::goto_functiont &goto_function); @@ -297,7 +296,7 @@ const symbolt &code_contractst::new_tmp_symbol( do { - new_symbol.base_name="tmp_cc$"+i2string(++temporary_counter); + new_symbol.base_name="tmp_cc$"+std::to_string(++temporary_counter); new_symbol.name=new_symbol.base_name; } while(symbol_table.move(new_symbol, symbol_ptr)); diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 5a92186fda7..2988b8637d2 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -9,15 +9,16 @@ Date: December 2012 \*******************************************************************/ #include +#include #include #include #include "count_eloc.h" -typedef hash_set_cont linest; -typedef hash_map_cont filest; -typedef hash_map_cont working_dirst; +typedef std::unordered_set linest; +typedef std::unordered_map filest; +typedef std::unordered_map working_dirst; /*******************************************************************\ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fba2f5fe4dc..5f02f91a0ee 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -12,7 +12,6 @@ Date: May 2016 #include #include -#include #include #include "cover.h" @@ -1120,7 +1119,7 @@ void instrument_cover_goals( unsigned block_nr=basic_blocks[i_it]; if(blocks_done.insert(block_nr).second) { - std::string b=i2string(block_nr); + std::string b=std::to_string(block_nr); std::string id=id2string(i_it->function)+"#"+b; source_locationt source_location= basic_blocks.source_location_map[block_nr]; @@ -1165,7 +1164,7 @@ void instrument_cover_goals( if(i_it->is_goto() && !i_it->guard.is_true()) { - std::string b=i2string(basic_blocks[i_it]); + std::string b=std::to_string(basic_blocks[i_it]); std::string true_comment= "function "+id2string(i_it->function)+" block "+b+" branch true"; std::string false_comment= diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp index 77e1df0a2cb..ad672236a5d 100644 --- a/src/goto-instrument/document_properties.cpp +++ b/src/goto-instrument/document_properties.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -286,7 +285,7 @@ void document_propertiest::get_code( for(std::list::iterator it=lines.begin(); it!=lines.end(); it++) { - std::string line_no=i2string(it->line_number); + std::string line_no=std::to_string(it->line_number); std::string tmp; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 1d6d7cc712e..7fcd310fa31 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -102,7 +101,7 @@ void dump_ct::operator()(std::ostream &os) forall_symbols(it, symbols_transparent.symbols) copied_symbol_table.add(it->second); - typedef hash_map_cont unique_tagst; + typedef std::unordered_map unique_tagst; unique_tagst unique_tags; // add tags to anonymous union/struct/enum, @@ -148,7 +147,7 @@ void dump_ct::operator()(std::ostream &os) unique_entry=unique_tags.insert(std::make_pair(new_tag, 0))) { new_tag=new_tag_base+"$"+ - i2string(unique_entry.first->second); + std::to_string(unique_entry.first->second); ++(unique_entry.first->second); } diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h index a84841ca9b9..6bb7b79638e 100644 --- a/src/goto-instrument/dump_c_class.h +++ b/src/goto-instrument/dump_c_class.h @@ -46,16 +46,16 @@ class dump_ct const namespacet ns; languaget *language; - typedef hash_set_cont convertedt; + typedef std::unordered_set convertedt; convertedt converted_compound, converted_global, converted_enum; std::set system_headers; - typedef hash_map_cont + typedef std::unordered_map system_library_mapt; system_library_mapt system_library_map; - typedef hash_map_cont + typedef std::unordered_map declared_enum_constants_mapt; declared_enum_constants_mapt declared_enum_constants; @@ -102,7 +102,7 @@ class dump_ct const typet &type, std::ostream &os); - typedef hash_map_cont + typedef std::unordered_map local_static_declst; void convert_global_variable( diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index ede5bfb2676..04f4b97a1ea 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #ifdef DEBUG_FULL_SLICERT -#include #endif #include @@ -409,7 +408,7 @@ void full_slicert::operator()( #ifdef DEBUG_FULL_SLICERT else { - std::string c="ins:"+i2string(i_it->location_number); + std::string c="ins:"+std::to_string(i_it->location_number); c+=" req by:"; for(std::set::const_iterator req_it=cfg[e].required_by.begin(); @@ -417,7 +416,7 @@ void full_slicert::operator()( ++req_it) { if(req_it!=cfg[e].required_by.begin()) c+=","; - c+=i2string(*req_it); + c+=std::to_string(*req_it); } i_it->source_location.set_column(c); // for show-goto-functions i_it->source_location.set_comment(c); // for dump-c diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index 5ba76686d3f..bc743a7830d 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -67,7 +67,7 @@ class full_slicert typedef std::vector dep_node_to_cfgt; typedef std::stack queuet; typedef std::list jumpst; - typedef hash_map_cont decl_deadt; + typedef std::unordered_map decl_deadt; void fixedpoint( goto_functionst &goto_functions, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 23d681c5644..37b223e3535 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -158,7 +158,7 @@ int goto_instrument_parse_optionst::doit() int k=-1; if(unwind) - k=safe_string2int (cmdline.get_value("unwind")); + k=std::stoi(cmdline.get_value("unwind")); unwind_sett unwind_set; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index edcc18a3792..e1698675af4 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "goto_program2code.h" @@ -2306,10 +2305,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) { unsigned count; for(count=0; - symbol_table.symbols.find("nondet_"+i2string(count))!= + symbol_table.symbols.find("nondet_"+std::to_string(count))!= symbol_table.symbols.end(); count++); - base_name="nondet_"+i2string(count); + base_name="nondet_"+std::to_string(count); } code_typet code_type; diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h index 02346e388ef..7d04c4accd4 100644 --- a/src/goto-instrument/goto_program2code.h +++ b/src/goto-instrument/goto_program2code.h @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com class goto_program2codet { typedef std::list id_listt; - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; typedef std::map loopt; - typedef hash_map_cont dead_mapt; + typedef std::unordered_map dead_mapt; typedef std::list > loop_last_stackt; @@ -78,7 +78,7 @@ class goto_program2codet id_listt &local_static; id_listt &type_names; std::set &system_headers; - hash_set_cont va_list_expr; + std::unordered_set va_list_expr; natural_loopst loops; loopt loop_map; diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index 78ab7648cd2..098e8378e18 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -14,7 +14,6 @@ Date: September 2011 #include #if 0 -#include #include #include #include diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 6c15573ec27..3ca605b55c6 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -8,7 +8,6 @@ Date: February 2006 \*******************************************************************/ -#include #include #include #include diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 9f30f74b2d2..c502c2a33ae 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index 129607487a0..4719ca6ed3d 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -15,7 +15,6 @@ Date: February 2006 #include #include -#include #include #include #include @@ -51,7 +50,7 @@ class rw_set_baset } }; - typedef hash_map_cont entriest; + typedef std::unordered_map entriest; entriest r_entries, w_entries; void swap(rw_set_baset &other) diff --git a/src/goto-instrument/show_locations.cpp b/src/goto-instrument/show_locations.cpp index 35ec08d9766..6527a29d437 100644 --- a/src/goto-instrument/show_locations.cpp +++ b/src/goto-instrument/show_locations.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -46,7 +45,7 @@ void show_locations( { xmlt xml("program_location"); xml.new_element("function").data=id2string(function_id); - xml.new_element("id").data=i2string(it->location_number); + xml.new_element("id").data=std::to_string(it->location_number); xmlt &l=xml.new_element(); l.name="location"; diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index d281f72210f..36f0d486773 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -13,7 +13,6 @@ Date: November 2011 #include #include #include -#include #include @@ -80,7 +79,7 @@ void stack_depth( assert_ins->source_location=first->source_location; assert_ins->function=first->function; - assert_ins->source_location.set_comment("Stack depth exceeds "+i2string(i_depth)); + assert_ins->source_location.set_comment("Stack depth exceeds "+std::to_string(i_depth)); assert_ins->source_location.set_property_class("stack-depth"); goto_programt::targett plus_ins=goto_program.insert_before(first); diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index 6d33bbe3a11..54fd4ec399f 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -472,9 +472,9 @@ jsont goto_unwindt::unwind_logt::output_log_json() const goto_programt::const_targett target=it->first; unsigned location_number=it->second; - object["original_location_number"]=json_numbert(i2string( + object["original_location_number"]=json_numbert(std::to_string( location_number)); - object["new_location_number"]=json_numbert(i2string( + object["new_location_number"]=json_numbert(std::to_string( target->location_number)); } diff --git a/src/goto-instrument/unwind.h b/src/goto-instrument/unwind.h index ec7613e99c1..ccd83bac589 100644 --- a/src/goto-instrument/unwind.h +++ b/src/goto-instrument/unwind.h @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_INSTRUMENT_UNWIND_H #define CPROVER_GOTO_INSTRUMENT_UNWIND_H -#include #include #include #include diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp index 79ed0b6a13f..f1d63cd33cd 100644 --- a/src/goto-instrument/wmm/event_graph.cpp +++ b/src/goto-instrument/wmm/event_graph.cpp @@ -10,7 +10,6 @@ Date: 2012 #include "event_graph.h" -#include #include #include @@ -1121,7 +1120,7 @@ std::string event_grapht::critical_cyclet::print() const { std::string cycle = "Cycle: "; for(const_iterator it=begin(); it!=end(); ++it) - cycle += i2string(egraph[*it].id) + "; "; + cycle += std::to_string(egraph[*it].id) + "; "; return cycle + " End of cycle."; } @@ -1230,7 +1229,7 @@ std::string event_grapht::critical_cyclet::print_output() const const abstract_eventt& it_evt=egraph[*it]; cycle += id2string(it_evt.variable) + " ("; cycle += it_evt.source_location.as_string(); - cycle += " thread " + i2string(it_evt.thread) + ") "; + cycle += " thread " + std::to_string(it_evt.thread) + ") "; } return cycle; } @@ -1261,15 +1260,15 @@ std::string event_grapht::critical_cyclet::print_detail( + " (" + it_evt.source_location.as_string() + ")"; if(map_var2id.find(var_name)!=map_var2id.end()) { - cycle += "t" + i2string(it_evt.thread) + " ("; + cycle += "t" + std::to_string(it_evt.thread) + " ("; cycle += map_var2id[var_name] + ") "; } else { - const std::string new_id = "var@" + i2string(map_var2id.size()); + const std::string new_id = "var@" + std::to_string(map_var2id.size()); map_var2id[var_name] = new_id; map_id2var[new_id] = var_name; - cycle += "t" + i2string(it_evt.thread) + " ("; + cycle += "t" + std::to_string(it_evt.thread) + " ("; cycle += new_id + ") "; } } diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 59e7f97f903..c157f07c1ac 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -20,7 +20,6 @@ Date: 2012 #include #include #include -#include #include #include "../rw_set.h" @@ -1770,7 +1769,7 @@ void instrumentert::print_outputs(memory_modelt model, bool hide_internals) for(unsigned i=0; i #include -#include #include "goto2graph.h" @@ -327,7 +326,7 @@ void inline instrumentert::instrument_minimum_interference_inserter( ++e_i) { ++i; - std::string name="e_"+i2string(i); + std::string name="e_"+std::to_string(i); glp_set_col_name(lp, i, name.c_str()); glp_set_col_bnds(lp, i, GLP_LO, 0.0, 0.0); glp_set_obj_coef(lp, i, cost(*e_i)); @@ -343,7 +342,7 @@ void inline instrumentert::instrument_minimum_interference_inserter( ++C_j) { ++i; - std::string name="C_"+i2string(i); + std::string name="C_"+std::to_string(i); glp_set_row_name(lp, i, name.c_str()); glp_set_row_bnds(lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ } diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp index 4bc6236768a..b008f5148aa 100644 --- a/src/goto-instrument/wmm/shared_buffers.cpp +++ b/src/goto-instrument/wmm/shared_buffers.cpp @@ -1,4 +1,3 @@ -#include #include "shared_buffers.h" #include "fence.h" @@ -19,8 +18,8 @@ Function: shared_buffert::unique std::string shared_bufferst::unique (void) { - message.debug()<<"$fresh#"+i2string(uniq)< #include -#include #include #include @@ -79,7 +78,7 @@ void introduce_temporaries( symbolt new_symbol; new_symbol.base_name="$tmp_guard"; - new_symbol.name=id2string(function)+"$tmp_guard"+i2string(tmp_counter++); + new_symbol.name=id2string(function)+"$tmp_guard"+std::to_string(tmp_counter++); new_symbol.type=bool_typet(); new_symbol.is_static_lifetime=true; new_symbol.is_thread_local=true; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 2f90b0f8443..fdf09c2c670 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include #include @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index c97a11f3f8f..ff9a8068c34 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include @@ -40,7 +39,7 @@ symbol_exprt goto_convertt::make_compound_literal( do { - new_symbol.base_name="literal$"+i2string(++temporary_counter); + new_symbol.base_name="literal$"+std::to_string(++temporary_counter); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.is_static_lifetime=source_location.get_function().empty(); new_symbol.value=expr; diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 78b5cc9067f..2a1c8bad6f5 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -2566,7 +2565,7 @@ symbolt &goto_convertt::new_tmp_symbol( do { - new_symbol.base_name="tmp_"+suffix+"$"+i2string(++temporary_counter); + new_symbol.base_name="tmp_"+suffix+"$"+std::to_string(++temporary_counter); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.type=type; new_symbol.location=source_location; diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp index 78d6d8b762e..badeebc29fb 100644 --- a/src/goto-programs/goto_convert_function_call.cpp +++ b/src/goto-programs/goto_convert_function_call.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include diff --git a/src/goto-programs/goto_convert_new_switch_case.cpp b/src/goto-programs/goto_convert_new_switch_case.cpp index 7f0b0007e6e..1bbde509419 100644 --- a/src/goto-programs/goto_convert_new_switch_case.cpp +++ b/src/goto-programs/goto_convert_new_switch_case.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -2509,7 +2508,7 @@ symbolt &goto_convertt::new_tmp_symbol( do { - new_symbol.base_name="tmp_"+suffix+"$"+i2string(++temporary_counter); + new_symbol.base_name="tmp_"+suffix+"$"+std::to_string(++temporary_counter); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.type=type; new_symbol.location=source_location; diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 4e51390026b..da2d8ca7cad 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -427,7 +426,7 @@ void goto_convertt::remove_function_call( new_base_name+='_'; new_base_name+=id2string(symbol.base_name); - new_base_name+="$"+i2string(++temporary_counter); + new_base_name+="$"+std::to_string(++temporary_counter); new_symbol.base_name=new_base_name; new_symbol.mode=symbol.mode; @@ -501,7 +500,7 @@ void goto_convertt::remove_cpp_new( auxiliary_symbolt new_symbol; - new_symbol.base_name="new_ptr$"+i2string(++temporary_counter); + new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter); new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); @@ -576,7 +575,7 @@ void goto_convertt::remove_malloc( { auxiliary_symbolt new_symbol; - new_symbol.base_name="malloc_value$"+i2string(++temporary_counter); + new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter); new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.location=expr.source_location(); diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 88053ef932c..8ffb33d010b 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H +#include + #include #include "goto_functions.h" @@ -76,13 +78,13 @@ class goto_inlinet:public messaget const code_typet &code_type, goto_programt &dest); - typedef hash_set_cont recursion_sett; + typedef std::unordered_set recursion_sett; recursion_sett recursion_set; - typedef hash_set_cont no_body_sett; + typedef std::unordered_set no_body_sett; no_body_sett no_body_set; - typedef hash_set_cont finished_inlining_sett; + typedef std::unordered_set finished_inlining_sett; finished_inlining_sett finished_inlining_set; }; diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index b83c1a10efd..f914488310a 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -511,7 +510,7 @@ std::string as_string( gt_it++) { if(gt_it!=i.targets.begin()) result+=", "; - result+=i2string((*gt_it)->target_number); + result+=std::to_string((*gt_it)->target_number); } return result; @@ -563,7 +562,7 @@ std::string as_string( result+="START THREAD "; if(i.targets.size()==1) - result+=i2string(i.targets.front()->target_number); + result+=std::to_string(i.targets.front()->target_number); return result; case END_THREAD: diff --git a/src/goto-programs/goto_program_irep.cpp b/src/goto-programs/goto_program_irep.cpp index cbf78acd295..efc76ea3069 100644 --- a/src/goto-programs/goto_program_irep.cpp +++ b/src/goto-programs/goto_program_irep.cpp @@ -11,7 +11,6 @@ Date: May 2007 #include #include -#include #include "goto_program_irep.h" @@ -49,7 +48,7 @@ void convert(const goto_programt::instructiont &instruction, irept &irep) it!=instruction.targets.end(); it++) { - irept t(i2string((*it)->location_number)); + irept t(std::to_string((*it)->location_number)); tgts.move_to_sub(t); } } diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 910603bdc39..e3fc77c328d 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -402,7 +402,7 @@ class goto_program_templatet inline static irep_idt loop_id(const_targett target) { return id2string(target->function)+"."+ - i2string(target->loop_number); + std::to_string(target->loop_number); } //! Is the program empty? diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index f5236227de6..d9f73ec7ebb 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening \*******************************************************************/ #include -#include #include #include #include @@ -186,7 +185,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) const graphmlt::node_indext node=graphml.add_node(); graphml[node].node_name= - i2string(it->pc->location_number)+"."+i2string(it->step_nr); + std::to_string(it->pc->location_number)+"."+std::to_string(it->step_nr); graphml[node].file=source_location.get_file(); graphml[node].line=source_location.get_line(); graphml[node].thread_nr=it->thread_nr; diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 94fab6ed8d4..9a3133e9f1c 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -36,7 +36,7 @@ class interpretert const namespacet ns; const goto_functionst &goto_functions; - typedef hash_map_cont memory_mapt; + typedef std::unordered_map memory_mapt; memory_mapt memory_map; class memory_cellt diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index 3d2cbf3c352..48964921aa7 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening #include -#include #include #include @@ -62,14 +61,14 @@ void convert( { property_id= id2string(it.pc->source_location.get_function())+".unwind."+ - i2string(it.pc->loop_number); + std::to_string(it.pc->loop_number); } json_objectt &json_failure=dest_array.push_back().make_object(); json_failure["stepType"]=json_stringt("failure"); json_failure["hidden"]=jsont::json_boolean(it.hidden); - json_failure["thread"]=json_numbert(i2string(it.thread_nr)); + json_failure["thread"]=json_numbert(std::to_string(it.thread_nr)); json_failure["reason"]=json_stringt(id2string(it.comment)); json_failure["property"]=json_stringt(id2string(property_id)); @@ -119,7 +118,7 @@ void convert( json_assignment["value"]=full_lhs_value; json_assignment["lhs"]=json_stringt(full_lhs_string); json_assignment["hidden"]=jsont::json_boolean(it.hidden); - json_assignment["thread"]=json_numbert(i2string(it.thread_nr)); + json_assignment["thread"]=json_numbert(std::to_string(it.thread_nr)); json_assignment["assignmentType"]= json_stringt(it.assignment_type==goto_trace_stept::ACTUAL_PARAMETER? @@ -133,7 +132,7 @@ void convert( json_output["stepType"]=json_stringt("output"); json_output["hidden"]=jsont::json_boolean(it.hidden); - json_output["thread"]=json_numbert(i2string(it.thread_nr)); + json_output["thread"]=json_numbert(std::to_string(it.thread_nr)); json_output["outputID"]=json_stringt(id2string(it.io_id)); json_arrayt &json_values=json_output["values"].make_array(); @@ -157,7 +156,7 @@ void convert( json_input["stepType"]=json_stringt("input"); json_input["hidden"]=jsont::json_boolean(it.hidden); - json_input["thread"]=json_numbert(i2string(it.thread_nr)); + json_input["thread"]=json_numbert(std::to_string(it.thread_nr)); json_input["inputID"]=json_stringt(id2string(it.io_id)); json_arrayt &json_values=json_input["values"].make_array(); @@ -185,7 +184,7 @@ void convert( json_call_return["stepType"]=json_stringt(tag); json_call_return["hidden"]=jsont::json_boolean(it.hidden); - json_call_return["thread"]=json_numbert(i2string(it.thread_nr)); + json_call_return["thread"]=json_numbert(std::to_string(it.thread_nr)); const symbolt &symbol=ns.lookup(it.identifier); json_objectt &json_function=json_call_return["function"].make_object(); @@ -208,7 +207,7 @@ void convert( json_objectt &json_location_only=dest_array.push_back().make_object(); json_location_only["stepType"]=json_stringt("location-only"); json_location_only["hidden"]=jsont::json_boolean(it.hidden); - json_location_only["thread"]=json_numbert(i2string(it.thread_nr)); + json_location_only["thread"]=json_numbert(std::to_string(it.thread_nr)); json_location_only["sourceLocation"]=json_location; } } diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index 93119cecb93..30c0ce838f0 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "loop_ids.h" @@ -81,7 +80,7 @@ void show_loop_ids( if(it->is_backwards_goto()) { unsigned loop_id=it->loop_number; - std::string id=id2string(it->function)+"."+i2string(loop_id); + std::string id=id2string(it->function)+"."+std::to_string(loop_id); xmlt xml_loop("loop"); xml_loop.set_attribute("name", id); @@ -111,7 +110,7 @@ void show_loop_ids_json( if(it->is_backwards_goto()) { unsigned loop_id=it->loop_number; - std::string id=id2string(it->function)+"."+i2string(loop_id); + std::string id=id2string(it->function)+"."+std::to_string(loop_id); json_objectt &loop=loops.push_back().make_object(); loop["name"]=json_stringt(id); diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp index cbc9a9af64d..9ae9ed5a29a 100644 --- a/src/goto-programs/read_goto_binary.cpp +++ b/src/goto-programs/read_goto_binary.cpp @@ -16,6 +16,7 @@ Module: Read Goto Programs #endif #include +#include #include #include @@ -284,7 +285,7 @@ static bool link_functions( const symbol_tablet &src_symbol_table, goto_functionst &src_functions, const rename_symbolt &rename_symbol, - const hash_set_cont &weak_symbols) + const std::unordered_set &weak_symbols) { namespacet ns(dest_symbol_table); namespacet src_ns(src_symbol_table); @@ -409,7 +410,7 @@ bool read_object_and_link( message_handler)) return true; - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; id_sett weak_symbols; forall_symbols(it, symbol_table.symbols) if(it->second.is_weak) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 5054f351a05..a58770bd1c8 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -138,7 +137,7 @@ symbolt &remove_function_pointerst::new_tmp_symbol() do { - new_symbol.base_name="tmp_return_val$"+i2string(++temporary_counter); + new_symbol.base_name="tmp_return_val$"+std::to_string(++temporary_counter); new_symbol.name="remove_function_pointers::"+id2string(new_symbol.base_name); } while(symbol_table.move(new_symbol, symbol_ptr)); diff --git a/src/goto-programs/set_properties.cpp b/src/goto-programs/set_properties.cpp index d6949449411..095fb43d235 100644 --- a/src/goto-programs/set_properties.cpp +++ b/src/goto-programs/set_properties.cpp @@ -7,9 +7,8 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include -#include -#include #include "set_properties.h" @@ -27,7 +26,7 @@ Function: set_properties void set_properties( goto_programt &goto_program, - hash_set_cont &property_set) + std::unordered_set &property_set) { for(goto_programt::instructionst::iterator it=goto_program.instructions.begin(); @@ -38,7 +37,7 @@ void set_properties( irep_idt property_id=it->source_location.get_property_id(); - hash_set_cont::iterator + std::unordered_set::iterator c_it=property_set.find(property_id); if(c_it==property_set.end()) @@ -110,7 +109,7 @@ void label_properties( count++; - std::string property_id=prefix+i2string(count); + std::string property_id=prefix+std::to_string(count); it->source_location.set_property_id(property_id); } @@ -169,7 +168,7 @@ void set_properties( goto_functionst &goto_functions, const std::list &properties) { - hash_set_cont property_set; + std::unordered_set property_set; for(std::list::const_iterator it=properties.begin(); diff --git a/src/goto-programs/show_goto_functions.cpp b/src/goto-programs/show_goto_functions.cpp index 85733c43dba..ef600a748cc 100644 --- a/src/goto-programs/show_goto_functions.cpp +++ b/src/goto-programs/show_goto_functions.cpp @@ -10,7 +10,6 @@ Author: Peter Schrammel #include #include -#include #include #include #include diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index e8ea32ca682..fb078873f1d 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 229607ffa88..3c5e736e2b8 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -379,7 +378,7 @@ Function: string_abstractiont::declare_define_locals void string_abstractiont::declare_define_locals(goto_programt &dest) { - typedef hash_map_cont + typedef std::unordered_map available_declst; available_declst available_decls; @@ -1250,7 +1249,7 @@ exprt string_abstractiont::build_unknown(const typet &type, bool write) // create an uninitialized dummy symbol // because of a lack of contextual information we can't build a nice name // here, but moving that into locals should suffice for proper operation - irep_idt identifier="$tmp::nondet_str#str$"+i2string(++temporary_counter); + irep_idt identifier="$tmp::nondet_str#str$"+std::to_string(++temporary_counter); // ensure decl and initialization locals[identifier]=identifier; diff --git a/src/goto-programs/string_abstraction.h b/src/goto-programs/string_abstraction.h index 12e66893092..f3e3a3e0526 100644 --- a/src/goto-programs/string_abstraction.h +++ b/src/goto-programs/string_abstraction.h @@ -135,7 +135,7 @@ class string_abstractiont:public messaget typet string_struct; goto_programt initialization; - typedef hash_map_cont localst; + typedef std::unordered_map localst; localst locals; void abstract(goto_programt &dest); diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp index a6e2c7d55c6..8b24655f304 100644 --- a/src/goto-programs/wp.cpp +++ b/src/goto-programs/wp.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "wp.h" @@ -63,7 +62,7 @@ void approximate_nondet_rec(exprt &dest, unsigned &count) to_side_effect_expr(dest).get_statement()==ID_nondet) { count++; - dest.set(ID_identifier, "wp::nondet::"+i2string(count)); + dest.set(ID_identifier, "wp::nondet::"+std::to_string(count)); dest.id(ID_nondet_symbol); return; } diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp index 161bc399cca..ac46ba776d7 100644 --- a/src/goto-programs/xml_goto_trace.cpp +++ b/src/goto-programs/xml_goto_trace.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening #include #include -#include #include #include @@ -61,14 +60,14 @@ void convert( { property_id= id2string(it.pc->source_location.get_function())+".unwind."+ - i2string(it.pc->loop_number); + std::to_string(it.pc->loop_number); } xmlt &xml_failure=dest.new_element("failure"); xml_failure.set_attribute_bool("hidden", it.hidden); - xml_failure.set_attribute("thread", i2string(it.thread_nr)); - xml_failure.set_attribute("step_nr", i2string(it.step_nr)); + xml_failure.set_attribute("thread", std::to_string(it.thread_nr)); + xml_failure.set_attribute("step_nr", std::to_string(it.step_nr)); xml_failure.set_attribute("reason", id2string(it.comment)); xml_failure.set_attribute("property", id2string(property_id)); @@ -120,11 +119,11 @@ void convert( xml_assignment.new_element("value").data=value_string; xml_assignment.set_attribute_bool("hidden", it.hidden); - xml_assignment.set_attribute("thread", i2string(it.thread_nr)); + xml_assignment.set_attribute("thread", std::to_string(it.thread_nr)); xml_assignment.set_attribute("identifier", id2string(identifier)); xml_assignment.set_attribute("base_name", id2string(base_name)); xml_assignment.set_attribute("display_name", id2string(display_name)); - xml_assignment.set_attribute("step_nr", i2string(it.step_nr)); + xml_assignment.set_attribute("step_nr", std::to_string(it.step_nr)); xml_assignment.set_attribute("assignment_type", it.assignment_type==goto_trace_stept::ACTUAL_PARAMETER?"actual_parameter": @@ -145,8 +144,8 @@ void convert( xml_output.new_element("text").data=text; xml_output.set_attribute_bool("hidden", it.hidden); - xml_output.set_attribute("thread", i2string(it.thread_nr)); - xml_output.set_attribute("step_nr", i2string(it.step_nr)); + xml_output.set_attribute("thread", std::to_string(it.thread_nr)); + xml_output.set_attribute("step_nr", std::to_string(it.step_nr)); if(xml_location.name!="") xml_output.new_element().swap(xml_location); @@ -166,8 +165,8 @@ void convert( xml_input.new_element("input_id").data=id2string(it.io_id); xml_input.set_attribute_bool("hidden", it.hidden); - xml_input.set_attribute("thread", i2string(it.thread_nr)); - xml_input.set_attribute("step_nr", i2string(it.step_nr)); + xml_input.set_attribute("thread", std::to_string(it.thread_nr)); + xml_input.set_attribute("step_nr", std::to_string(it.step_nr)); for(const auto & l_it : it.io_args) { @@ -189,8 +188,8 @@ void convert( xmlt &xml_call_return=dest.new_element(tag); xml_call_return.set_attribute_bool("hidden", it.hidden); - xml_call_return.set_attribute("thread", i2string(it.thread_nr)); - xml_call_return.set_attribute("step_nr", i2string(it.step_nr)); + xml_call_return.set_attribute("thread", std::to_string(it.thread_nr)); + xml_call_return.set_attribute("step_nr", std::to_string(it.step_nr)); const symbolt &symbol=ns.lookup(it.identifier); xmlt &xml_function=xml_call_return.new_element("function"); @@ -212,8 +211,8 @@ void convert( xmlt &xml_location_only=dest.new_element("location-only"); xml_location_only.set_attribute_bool("hidden", it.hidden); - xml_location_only.set_attribute("thread", i2string(it.thread_nr)); - xml_location_only.set_attribute("step_nr", i2string(it.step_nr)); + xml_location_only.set_attribute("thread", std::to_string(it.thread_nr)); + xml_location_only.set_attribute("step_nr", std::to_string(it.step_nr)); xml_location_only.new_element().swap(xml_location); } diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp index b06a86691ec..a561984bf30 100644 --- a/src/goto-symex/auto_objects.cpp +++ b/src/goto-symex/auto_objects.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include #include @@ -33,7 +32,7 @@ exprt goto_symext::make_auto_object(const typet &type) // produce auto-object symbol symbolt symbol; - symbol.base_name="auto_object"+i2string(dynamic_counter); + symbol.base_name="auto_object"+std::to_string(dynamic_counter); symbol.name="symex::"+id2string(symbol.base_name); symbol.is_lvalue=true; symbol.type=type; diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index fa6d5841817..a3d55220e8d 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -49,7 +49,7 @@ void goto_symext::replace_nondet(exprt &expr) expr.get(ID_statement)==ID_nondet) { exprt new_expr(ID_nondet_symbol, expr.type()); - new_expr.set(ID_identifier, "symex::nondet"+i2string(nondet_count++)); + new_expr.set(ID_identifier, "symex::nondet"+std::to_string(nondet_count++)); new_expr.add_source_location()=expr.source_location(); expr.swap(new_expr); } diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 2063d210764..cf4cdb38f5a 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -10,10 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H #include +#include #include #include -#include #include #include @@ -64,7 +64,7 @@ class goto_symex_statet ++current_names[identifier].second; } - void get_variables(hash_set_cont &vars) const + void get_variables(std::unordered_set &vars) const { for(current_namest::const_iterator it=current_names.begin(); it!=current_names.end(); @@ -173,7 +173,7 @@ class goto_symex_statet void get_l1_name(exprt &expr) const; // this maps L1 names to (L2) types - typedef hash_map_cont l1_typest; + typedef std::unordered_map l1_typest; l1_typest l1_types; public: @@ -202,7 +202,7 @@ class goto_symex_statet } // the below replicate levelt2 member functions - void level2_get_variables(hash_set_cont &vars) const + void level2_get_variables(std::unordered_set &vars) const { for(level2t::current_namest::const_iterator it=level2_current_names.begin(); @@ -264,7 +264,7 @@ class goto_symex_statet unsigned count; bool is_recursion; }; - typedef hash_map_cont + typedef std::unordered_map loop_iterationst; loop_iterationst loop_iterations; }; @@ -302,9 +302,9 @@ class goto_symex_statet // threads unsigned atomic_section_id; typedef std::pair > a_s_r_entryt; - typedef hash_map_cont read_in_atomic_sectiont; + typedef std::unordered_map read_in_atomic_sectiont; typedef std::list a_s_w_entryt; - typedef hash_map_cont written_in_atomic_sectiont; + typedef std::unordered_map written_in_atomic_sectiont; read_in_atomic_sectiont read_in_atomic_section; written_in_atomic_sectiont written_in_atomic_section; diff --git a/src/goto-symex/memory_model.cpp b/src/goto-symex/memory_model.cpp index 702fefe57b6..77730a80d24 100644 --- a/src/goto-symex/memory_model.cpp +++ b/src/goto-symex/memory_model.cpp @@ -7,7 +7,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk \*******************************************************************/ #include -#include #include "memory_model.h" @@ -61,7 +60,7 @@ symbol_exprt memory_model_baset::nondet_bool_symbol( const std::string &prefix) { return symbol_exprt( - "memory_model::choice_"+prefix+i2string(var_cnt++), + "memory_model::choice_"+prefix+std::to_string(var_cnt++), bool_typet()); } diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp index eeeda91e2b6..0cac966402f 100644 --- a/src/goto-symex/memory_model_sc.cpp +++ b/src/goto-symex/memory_model_sc.cpp @@ -7,7 +7,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk \*******************************************************************/ #include -#include #include "memory_model_sc.h" diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp index e9c1eb72e95..0c39dbafc5f 100644 --- a/src/goto-symex/partial_order_concurrency.cpp +++ b/src/goto-symex/partial_order_concurrency.cpp @@ -8,7 +8,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #include -#include #include #include @@ -62,7 +61,7 @@ Function: partial_order_concurrencyt::add_init_writes void partial_order_concurrencyt::add_init_writes( symex_target_equationt &equation) { - hash_set_cont init_done; + std::unordered_set init_done; bool spawn_seen=false; symex_target_equationt::SSA_stepst init_steps; @@ -185,9 +184,9 @@ irep_idt partial_order_concurrencyt::rw_clock_id( axiomt axiom) { if(event->is_shared_write()) - return id2string(id(event))+"$wclk$"+i2string(axiom); + return id2string(id(event))+"$wclk$"+std::to_string(axiom); else if(event->is_shared_read()) - return id2string(id(event))+"$rclk$"+i2string(axiom); + return id2string(id(event))+"$rclk$"+std::to_string(axiom); else assert(false); @@ -227,8 +226,8 @@ symbol_exprt partial_order_concurrencyt::clock( { assert(is_spawn(event)); identifier= - "t"+i2string(event->source.thread_nr+1)+"$"+ - i2string(numbering[event])+"$spwnclk$"+i2string(axiom); + "t"+std::to_string(event->source.thread_nr+1)+"$"+ + std::to_string(numbering[event])+"$spwnclk$"+std::to_string(axiom); } else assert(false); diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp index 4be55beaa65..003f0ac60a8 100644 --- a/src/goto-symex/postcondition.cpp +++ b/src/goto-symex/postcondition.cpp @@ -255,7 +255,7 @@ bool postconditiont::is_used( value_setst::valuest expr_set; value_set.get_value_set(expr.op0(), expr_set, ns); - hash_set_cont symbols; + std::unordered_set symbols; for(value_setst::valuest::const_iterator it=expr_set.begin(); diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp index d7874b9f3b8..4c392e57d94 100644 --- a/src/goto-symex/precondition.cpp +++ b/src/goto-symex/precondition.cpp @@ -171,7 +171,7 @@ void preconditiont::compute_rec(exprt &dest) value_setst::valuest expr_set; value_sets.get_values(target, dest.op0(), expr_set); - hash_set_cont symbols; + std::unordered_set symbols; for(value_setst::valuest::const_iterator it=expr_set.begin(); diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp index 8421e5f30b2..5e2594c656d 100644 --- a/src/goto-symex/slice.cpp +++ b/src/goto-symex/slice.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include "slice.h" diff --git a/src/goto-symex/slice.h b/src/goto-symex/slice.h index 410725b5a59..1fd15969274 100644 --- a/src/goto-symex/slice.h +++ b/src/goto-symex/slice.h @@ -23,7 +23,7 @@ void slice(symex_target_equationt &equation, // Collects "open" variables that are used but not assigned -typedef hash_set_cont symbol_sett; +typedef std::unordered_set symbol_sett; void collect_open_variables( const symex_target_equationt &equation, diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp index 8928b0524d7..922f66b3eb5 100644 --- a/src/goto-symex/slice_by_trace.cpp +++ b/src/goto-symex/slice_by_trace.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -611,8 +610,9 @@ std::set symex_slice_by_tracet::implied_guards(exprt e) if (e.id() == ID_symbol) { // Guard or merge - const char* merge_loc = strstr(e.get(ID_identifier).c_str(),"merge#"); - if(merge_loc == NULL) + const std::string &id_string=id2string(e.get(ID_identifier)); + std::string::size_type merge_loc=id_string.find("merge#"); + if(merge_loc==std::string::npos) { exprt e_copy (e); simplify(e_copy, ns); @@ -621,7 +621,7 @@ std::set symex_slice_by_tracet::implied_guards(exprt e) } else { - int i = unsafe_c_str2int(merge_loc+1); + int i=unsafe_string2int(id_string.substr(merge_loc+6)); if (merge_impl_cache_back[i].first) { return merge_impl_cache_back[i].second; diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 0a1fbbf8505..ed9c6262ee4 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -143,7 +142,7 @@ void goto_symext::symex_malloc( symbolt size_symbol; - size_symbol.base_name="dynamic_object_size"+i2string(dynamic_counter); + size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_counter); size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name); size_symbol.is_lvalue=true; size_symbol.type=tmp_size.type(); @@ -161,7 +160,7 @@ void goto_symext::symex_malloc( // value symbolt value_symbol; - value_symbol.base_name="dynamic_object"+i2string(dynamic_counter); + value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter); value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name); value_symbol.is_lvalue=true; value_symbol.type=object_type; @@ -249,7 +248,7 @@ void goto_symext::symex_gcc_builtin_va_arg_next( std::string base=id2string(function_identifier)+"::va_arg"; if(has_prefix(id2string(id), base)) - id=base+i2string( + id=base+std::to_string( safe_string2unsigned( std::string(id2string(id), base.size(), std::string::npos))+1); else @@ -464,7 +463,7 @@ void goto_symext::symex_cpp_new( dynamic_counter++; - const std::string count_string(i2string(dynamic_counter)); + const std::string count_string(std::to_string(dynamic_counter)); // value symbolt symbol; diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index c2d5d30ebd9..16574d5679f 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -161,18 +160,18 @@ void goto_symext::parameter_assignments( // These are va_arg arguments; their types may differ from call to call unsigned va_count=0; const symbolt *va_sym=0; - while(!ns.lookup(id2string(function_identifier)+"::va_arg"+i2string(va_count), + while(!ns.lookup(id2string(function_identifier)+"::va_arg"+std::to_string(va_count), va_sym)) ++va_count; for( ; it1!=arguments.end(); it1++, va_count++) { - irep_idt id=id2string(function_identifier)+"::va_arg"+i2string(va_count); + irep_idt id=id2string(function_identifier)+"::va_arg"+std::to_string(va_count); // add to symbol table symbolt symbol; symbol.name=id; - symbol.base_name="va_arg"+i2string(va_count); + symbol.base_name="va_arg"+std::to_string(va_count); symbol.type=it1->type(); new_symbol_table.move(symbol); diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index cb808b729e2..17149677965 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "goto_symex.h" @@ -297,12 +296,12 @@ void goto_symext::phi_function( statet &dest_state) { // go over all variables to see what changed - hash_set_cont variables; + std::unordered_set variables; goto_state.level2_get_variables(variables); dest_state.level2.get_variables(variables); - for(hash_set_cont::const_iterator + for(std::unordered_set::const_iterator it=variables.begin(); it!=variables.end(); it++) @@ -333,7 +332,7 @@ void goto_symext::phi_function( // only later be removed from level2.current_names by pop_frame // once the thread is executed) if(!it->get_level_0().empty() && - it->get_level_0()!=i2string(dest_state.source.thread_nr)) + it->get_level_0()!=std::to_string(dest_state.source.thread_nr)) continue; exprt goto_state_rhs=*it, dest_state_rhs=*it; @@ -427,7 +426,7 @@ void goto_symext::loop_bound_exceeded( { // Generate VCC for unwinding assertion. vcc(negated_cond, - "unwinding assertion loop "+i2string(loop_number), + "unwinding assertion loop "+std::to_string(loop_number), state); // add to state guard to prevent further assignments diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 2f6051177d4..8c4e48f8a2e 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include @@ -894,7 +893,7 @@ void symex_target_equationt::convert_io( { symbol_exprt symbol; symbol.type()=tmp.type(); - symbol.set_identifier("symex::io::"+i2string(io_count++)); + symbol.set_identifier("symex::io::"+std::to_string(io_count++)); equal_exprt eq(tmp, symbol); merge_irep(eq); diff --git a/src/java_bytecode/expr2java.cpp b/src/java_bytecode/expr2java.cpp index 14b033a68fe..10476044889 100644 --- a/src/java_bytecode/expr2java.cpp +++ b/src/java_bytecode/expr2java.cpp @@ -8,12 +8,13 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include +#include #include #include #include -#include #include +#include #include #include "java_types.h" @@ -50,7 +51,7 @@ class expr2javat:public expr2ct const c_qualifierst &qualifiers, const std::string &declarator); - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; }; /*******************************************************************\ diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 4fd33ae121a..c4a91cff14f 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -156,7 +155,7 @@ class java_bytecode_convert_methodt:public messaget symbol_exprt tmp_variable(const std::string &prefix, const typet &type) { - irep_idt base_name=prefix+"_tmp"+i2string(tmp_vars.size()); + irep_idt base_name=prefix+"_tmp"+std::to_string(tmp_vars.size()); irep_idt identifier=id2string(current_method)+"::"+id2string(base_name); auxiliary_symbolt tmp_symbol; @@ -346,7 +345,7 @@ void java_bytecode_convert_methodt::convert( { const typet &type=parameters[i].type(); char suffix=java_char_from_type(type); - base_name="arg"+i2string(param_index)+suffix; + base_name="arg"+std::to_string(param_index)+suffix; identifier=id2string(method_identifier)+"::"+id2string(base_name); } @@ -1525,7 +1524,7 @@ codet java_bytecode_convert_methodt::convert_instructions( const codet &c=it.second.code; if(targets.find(address)!=targets.end()) - code.add(code_labelt(label(i2string(address)), c)); + code.add(code_labelt(label(std::to_string(address)), c)); else if(c.get_statement()!=ID_skip) code.add(c); } diff --git a/src/java_bytecode/java_bytecode_parser.cpp b/src/java_bytecode/java_bytecode_parser.cpp index 449e5954295..45cbffa1035 100644 --- a/src/java_bytecode/java_bytecode_parser.cpp +++ b/src/java_bytecode/java_bytecode_parser.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 96bbd5764bb..19f195cf007 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 854c086df04..15735f62539 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -192,7 +191,7 @@ symbolt &new_tmp_symbol(symbol_tablet &symbol_table) do { - new_symbol.name="tmp_object_factory$"+i2string(++temporary_counter); + new_symbol.name="tmp_object_factory$"+std::to_string(++temporary_counter); new_symbol.base_name=new_symbol.name; new_symbol.mode=ID_java; } while(symbol_table.move(new_symbol, symbol_ptr)); diff --git a/src/jsil/jsil_typecheck.h b/src/jsil/jsil_typecheck.h index c8fa8c1a3b1..f515147a297 100644 --- a/src/jsil/jsil_typecheck.h +++ b/src/jsil/jsil_typecheck.h @@ -9,6 +9,8 @@ Author: Michael Tautschnig, tautschn@amazon.com #ifndef CPROVER_JSIL_JSIL_TYPECHECK_H #define CPROVER_JSIL_JSIL_TYPECHECK_H +#include + #include #include #include @@ -89,7 +91,7 @@ class jsil_typecheckt:public typecheckt virtual std::string to_string(const exprt &expr); virtual std::string to_string(const typet &type); - hash_set_cont already_typechecked; + std::unordered_set already_typechecked; }; #endif // CPROVER_JSIL_JSIL_TYPECHECK_H diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp index c0876c3faed..d409dc1947e 100644 --- a/src/langapi/language_ui.cpp +++ b/src/langapi/language_ui.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include #include -#include #include #include #include diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 90a578cc331..3ff4d09de22 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -222,8 +221,8 @@ void linkingt::detailed_conflict_report_rec( if(components1.size()!=components2.size()) { msg="number of members is different ("; - msg+=i2string(components1.size())+'/'; - msg+=i2string(components2.size())+')'; + msg+=std::to_string(components1.size())+'/'; + msg+=std::to_string(components2.size())+')'; } else for(std::size_t i=0; i type_sett; + typedef std::unordered_set type_sett; type_sett parent_types; exprt e=conflict_path_before; @@ -310,22 +309,22 @@ void linkingt::detailed_conflict_report_rec( else if(members1.size()!=members2.size()) { msg="number of enum members is different ("; - msg+=i2string(members1.size())+'/'; - msg+=i2string(members2.size())+')'; + msg+=std::to_string(members1.size())+'/'; + msg+=std::to_string(members2.size())+')'; } else for(std::size_t i=0; i0) detailed_conflict_report_rec( @@ -380,7 +379,7 @@ void linkingt::detailed_conflict_report_rec( { conflict_path= index_exprt(conflict_path, - constant_exprt(i2string(i), integer_typet())); + constant_exprt(std::to_string(i), integer_typet())); if(depth>0) detailed_conflict_report_rec( @@ -498,7 +497,7 @@ irep_idt linkingt::rename(const irep_idt id) while(true) { irep_idt new_identifier= - id2string(id)+"$link"+i2string(++cnt); + id2string(id)+"$link"+std::to_string(++cnt); if(main_symbol_table.symbols.find(new_identifier)!= main_symbol_table.symbols.end()) diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h index c40ce92530c..fa14f520330 100644 --- a/src/linking/linking_class.h +++ b/src/linking/linking_class.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -35,7 +34,7 @@ class linkingt:public typecheckt protected: - typedef hash_set_cont id_sett; + typedef std::unordered_set id_sett; bool needs_renaming_type( const symbolt &old_symbol, @@ -170,7 +169,7 @@ class linkingt:public typecheckt namespacet ns; // X -> Y iff Y uses X for new symbol type IDs X and Y - typedef hash_map_cont used_byt; + typedef std::unordered_map used_byt; irep_idt rename(irep_idt); diff --git a/src/musketeer/fence_inserter.cpp b/src/musketeer/fence_inserter.cpp index c939285537f..3ec27b597f0 100644 --- a/src/musketeer/fence_inserter.cpp +++ b/src/musketeer/fence_inserter.cpp @@ -6,7 +6,6 @@ Author: Vincent Nimal \*******************************************************************/ -#include #include #include @@ -287,14 +286,14 @@ void inline fence_insertert::mip_set_var(ilpt& ilp, if(model==Power || model==Unknown) { /* dp variable for e */ - const std::string name_dp="dp_"+i2string(i); + const std::string name_dp="dp_"+std::to_string(i); glp_set_col_name(ilp.lp, i, name_dp.c_str()); glp_set_col_bnds(ilp.lp, i, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i, (has_cost?fence_cost(Dp):0)*freq_sum); glp_set_col_kind(ilp.lp, i, GLP_BV); /* fence variable for e */ - const std::string name_f="f_"+i2string(i); + const std::string name_f="f_"+std::to_string(i); glp_set_col_name(ilp.lp, i+1, name_f.c_str()); glp_set_col_bnds(ilp.lp, i+1, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i+1, (has_cost?fence_cost(Fence):0)*freq_sum); @@ -303,14 +302,14 @@ void inline fence_insertert::mip_set_var(ilpt& ilp, // Note: uncomment for br and cf fences #if 0 /* br variable for e */ - const std::string name_br="br_"+i2string(i); + const std::string name_br="br_"+std::to_string(i); glp_set_col_name(ilp.lp, i+2, name_br.c_str()); glp_set_col_bnds(ilp.lp, i+2, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i+2, (has_cost?fence_cost(Branching):0)*freq_sum); glp_set_col_kind(ilp.lp, i+2, GLP_BV); /* cf variable for e */ - const std::string name_cf="cf_"+i2string(i); + const std::string name_cf="cf_"+std::to_string(i); glp_set_col_name(ilp.lp, i+3, name_cf.c_str()); glp_set_col_bnds(ilp.lp, i+3, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i+3, (has_cost?fence_cost(Ctlfence):0)*freq_sum); @@ -319,7 +318,7 @@ void inline fence_insertert::mip_set_var(ilpt& ilp, if(model==Power) { /* lwf variable for e */ - const std::string name_lwf="lwf_"+i2string(i); + const std::string name_lwf="lwf_"+std::to_string(i); glp_set_col_name(ilp.lp, i+2/*4*/, name_lwf.c_str()); glp_set_col_bnds(ilp.lp, i+2/*4*/, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i+2/*4*/, @@ -329,7 +328,7 @@ void inline fence_insertert::mip_set_var(ilpt& ilp, } else { /* fence variable for e */ - const std::string name_f="f_"+i2string(i); + const std::string name_f="f_"+std::to_string(i); glp_set_col_name(ilp.lp, i, name_f.c_str()); glp_set_col_bnds(ilp.lp, i, GLP_LO, 0.0, 0.0); glp_set_obj_coef(ilp.lp, i, (has_cost?fence_cost(Fence):0)*freq_sum); @@ -370,7 +369,7 @@ void inline fence_insertert::mip_set_cst(ilpt& ilp, unsigned& i) /* for all e */ for(unsigned j=1; j<=c_wr_it->size(); ++j) { - std::string name="C_"+i2string(i)+"_c_wr_"+i2string(j); + std::string name="C_"+std::to_string(i)+"_c_wr_"+std::to_string(j); glp_set_row_name(ilp.lp, i, name.c_str()); glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ ++i; @@ -387,7 +386,7 @@ void inline fence_insertert::mip_set_cst(ilpt& ilp, unsigned& i) /* for all e */ for(unsigned j=1; j<=c_ww_it->size(); ++j) { - std::string name="C_"+i2string(i)+"_c_ww_"+i2string(j); + std::string name="C_"+std::to_string(i)+"_c_ww_"+std::to_string(j); glp_set_row_name(ilp.lp, i, name.c_str()); glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ ++i; @@ -404,7 +403,7 @@ void inline fence_insertert::mip_set_cst(ilpt& ilp, unsigned& i) /* for all e */ for(unsigned j=1; j<=c_rw_it->size(); ++j) { - std::string name="C_"+i2string(i)+"_c_rw_"+i2string(j); + std::string name="C_"+std::to_string(i)+"_c_rw_"+std::to_string(j); glp_set_row_name(ilp.lp, i, name.c_str()); glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ ++i; @@ -421,7 +420,7 @@ void inline fence_insertert::mip_set_cst(ilpt& ilp, unsigned& i) /* for all e */ for(unsigned j=1; j<=c_rr_it->size(); ++j) { - std::string name="C_"+i2string(i)+"_c_rr_"+i2string(j); + std::string name="C_"+std::to_string(i)+"_c_rr_"+std::to_string(j); glp_set_row_name(ilp.lp, i, name.c_str()); glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ ++i; @@ -438,7 +437,7 @@ void inline fence_insertert::mip_set_cst(ilpt& ilp, unsigned& i) /* for all e */ for(unsigned j=1; j<=c_it->size(); ++j) { - std::string name="C_"+i2string(i)+"_c_"+i2string(j); + std::string name="C_"+std::to_string(i)+"_c_"+std::to_string(j); glp_set_row_name(ilp.lp, i, name.c_str()); glp_set_row_bnds(ilp.lp, i, GLP_LO, 1.0, 0.0); /* >= 1*/ ++i; diff --git a/src/musketeer/fence_shared.cpp b/src/musketeer/fence_shared.cpp index f4f95501472..c3557d712af 100644 --- a/src/musketeer/fence_shared.cpp +++ b/src/musketeer/fence_shared.cpp @@ -13,7 +13,6 @@ Author: Vincent Nimal #include #include -#include #include #include #include diff --git a/src/musketeer/fencer.cpp b/src/musketeer/fencer.cpp index a372355dc08..bbcb1db1d2d 100644 --- a/src/musketeer/fencer.cpp +++ b/src/musketeer/fencer.cpp @@ -6,7 +6,6 @@ Author: Vincent Nimal \*******************************************************************/ -#include #include #include #include diff --git a/src/musketeer/pensieve.cpp b/src/musketeer/pensieve.cpp index f28d8eccfc0..42ae7b61a49 100644 --- a/src/musketeer/pensieve.cpp +++ b/src/musketeer/pensieve.cpp @@ -6,7 +6,6 @@ Author: Vincent Nimal \*******************************************************************/ -#include #include #include #include diff --git a/src/musketeer/propagate_const_function_pointers.cpp b/src/musketeer/propagate_const_function_pointers.cpp index ec6597d2bfa..253d601a056 100644 --- a/src/musketeer/propagate_const_function_pointers.cpp +++ b/src/musketeer/propagate_const_function_pointers.cpp @@ -2,8 +2,6 @@ #include #include #include -#include -#include #include #include @@ -21,16 +19,16 @@ class const_function_pointer_propagationt { const namespacet ns; messaget& message; - hash_map_cont map_unique; + std::unordered_map map_unique; /* maps const pointer to function (expression + arguments at call) */ - hash_map_cont pointer_to_fun; + std::unordered_map pointer_to_fun; /* maps const pointer to where it was defined in the call function stack */ - hash_map_cont pointer_to_stack; + std::unordered_map pointer_to_stack; /* where a const function to inline was the first time invoked */ - hash_map_cont fun_id_to_invok; + std::unordered_map fun_id_to_invok; /* stack of callsites: provides functions and location in the goto-program */ goto_programt::const_targetst callsite_stack; @@ -176,12 +174,12 @@ void const_function_pointer_propagationt::dup_caller_and_inline_callee( { /* unique suffix */ if(map_unique.find(function_id)!=map_unique.end()) { - suffix+=i2string(map_unique[function_id]); + suffix+=std::to_string(map_unique[function_id]); ++map_unique[function_id]; } else { map_unique[function_id]=0; - suffix+=i2string(map_unique[function_id]); + suffix+=std::to_string(map_unique[function_id]); ++map_unique[function_id]; } @@ -366,7 +364,7 @@ void const_function_pointer_propagationt::arg_stackt::add_args( //cfpp.symbol_table.lookup(arg_symbol_expr.get_identifier()); // debug - for(hash_map_cont::const_iterator + for(std::unordered_map::const_iterator it=cfpp.fun_id_to_invok.begin(); it!=cfpp.fun_id_to_invok.end(); ++it) diff --git a/src/path-symex/locs.h b/src/path-symex/locs.h index 5978fae2d01..f45349b420d 100644 --- a/src/path-symex/locs.h +++ b/src/path-symex/locs.h @@ -109,12 +109,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_PATH_SYMEX_LOCS_H diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp index 45fb7bb9e5a..d1f1f411f3a 100644 --- a/src/path-symex/path_symex.cpp +++ b/src/path-symex/path_symex.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -240,7 +239,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(); @@ -259,7 +258,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; diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp index 5e9886a0368..3cd0cd0d269 100644 --- a/src/path-symex/path_symex_state.cpp +++ b/src/path-symex/path_symex_state.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp index c527e383d3b..33aab3c5fc5 100644 --- a/src/path-symex/path_symex_state_read.cpp +++ b/src/path-symex/path_symex_state_read.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -305,7 +304,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()); } diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp index e408909df12..984d1049abc 100644 --- a/src/path-symex/var_map.cpp +++ b/src/path-symex/var_map.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "var_map.h" @@ -156,7 +155,7 @@ 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); } /*******************************************************************\ diff --git a/src/pointer-analysis/object_numbering.h b/src/pointer-analysis/object_numbering.h index 714f3190252..beddfb76ab6 100644 --- a/src/pointer-analysis/object_numbering.h +++ b/src/pointer-analysis/object_numbering.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H #define CPROVER_POINTER_ANALYSIS_OBJECT_NUMBERING_H -#include #include #include diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 08330f06078..500dbd23bcf 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -1619,7 +1618,7 @@ void value_sett::do_function_call( for(unsigned i=0; itype()); + symbol_exprt("value_set::dummy_arg_"+std::to_string(i), it->type()); exprt actual_lhs=symbol_exprt(identifier, it->type()); assign(actual_lhs, v_expr, ns, true, true); diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 7902fc04fb8..70b7f15d698 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -115,7 +115,7 @@ class value_sett #ifdef USE_DSTRING typedef std::map valuest; #else - typedef hash_map_cont valuest; + typedef std::unordered_map valuest; #endif void get_value_set( diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp index 17e28ee8b41..cba409fa8f5 100644 --- a/src/pointer-analysis/value_set_analysis_fi.cpp +++ b/src/pointer-analysis/value_set_analysis_fi.cpp @@ -80,7 +80,7 @@ void value_set_analysis_fit::add_vars( goto_program.get_decl_identifiers(locals); // cache the list for the locals to speed things up - typedef hash_map_cont entry_cachet; + typedef std::unordered_map entry_cachet; entry_cachet entry_cache; value_set_fit &v=state.value_set; diff --git a/src/pointer-analysis/value_set_analysis_fivr.cpp b/src/pointer-analysis/value_set_analysis_fivr.cpp index e864606ed5c..3ed0538bb1c 100644 --- a/src/pointer-analysis/value_set_analysis_fivr.cpp +++ b/src/pointer-analysis/value_set_analysis_fivr.cpp @@ -80,7 +80,7 @@ void value_set_analysis_fivrt::add_vars( goto_program.get_decl_identifiers(locals); // cache the list for the locals to speed things up - typedef hash_map_cont entry_cachet; + typedef std::unordered_map entry_cachet; entry_cachet entry_cache; value_set_fivrt &v=state.value_set; diff --git a/src/pointer-analysis/value_set_analysis_fivrns.cpp b/src/pointer-analysis/value_set_analysis_fivrns.cpp index 865b1a3e247..4fbe598ae13 100644 --- a/src/pointer-analysis/value_set_analysis_fivrns.cpp +++ b/src/pointer-analysis/value_set_analysis_fivrns.cpp @@ -80,7 +80,7 @@ void value_set_analysis_fivrnst::add_vars( goto_program.get_decl_identifiers(locals); // cache the list for the locals to speed things up - typedef hash_map_cont entry_cachet; + typedef std::unordered_map entry_cachet; entry_cachet entry_cache; value_set_fivrnst &v=state.value_set; diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 57c6b3682fd..e19110a1c93 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -17,11 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include -#include #include #include #include @@ -199,7 +197,7 @@ exprt value_set_dereferencet::dereference( // else: produce new symbol symbolt symbol; - symbol.name="symex::invalid_object"+i2string(invalid_counter++); + symbol.name="symex::invalid_object"+std::to_string(invalid_counter++); symbol.base_name="invalid_object"; symbol.type=type; diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 5fc40f6fe25..60daefd8d4d 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -9,10 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H #define CPROVER_POINTER_ANALYSIS_VALUE_SET_DEREFERENCE_H -#include -#include +#include -#include #include #include "dereference_callback.h" @@ -73,7 +71,7 @@ class value_set_dereferencet */ static bool has_dereference(const exprt &expr); - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; private: const namespacet &ns; diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index d758e40c987..e1157b49324 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -1565,7 +1564,7 @@ void value_set_fit::do_function_call( for(unsigned i=0; itype()); + "argument$"+std::to_string(i), it->type()); exprt actual_lhs=symbol_exprt(identifier, it->type()); assign(actual_lhs, v_expr, ns); @@ -1613,7 +1612,7 @@ void value_set_fit::do_end_function( { if(lhs.is_nil()) return; - std::string rvs = "value_set::return_value" + i2string(from_function); + std::string rvs = "value_set::return_value" + std::to_string(from_function); symbol_exprt rhs(rvs, lhs.type()); assign(lhs, rhs, ns); @@ -1711,7 +1710,7 @@ void value_set_fit::apply_code( // this is turned into an assignment if(code.operands().size()==1) { - std::string rvs = "value_set::return_value" + i2string(from_function); + std::string rvs = "value_set::return_value" + std::to_string(from_function); symbol_exprt lhs(rvs, code.op0().type()); assign(lhs, code.op0(), ns); } diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 83affdb4ad4..fa8ddb551b6 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -10,7 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FI_H +#include #include +#include #include #include @@ -148,20 +150,20 @@ class value_set_fit } }; - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; #ifdef USE_DSTRING typedef std::map valuest; typedef std::set flatten_seent; - typedef hash_set_cont gvs_recursion_sett; - typedef hash_set_cont recfind_recursion_sett; - typedef hash_set_cont assign_recursion_sett; + typedef std::unordered_set gvs_recursion_sett; + typedef std::unordered_set recfind_recursion_sett; + typedef std::unordered_set assign_recursion_sett; #else - typedef hash_map_cont valuest; - typedef hash_set_cont flatten_seent; - typedef hash_set_cont gvs_recursion_sett; - typedef hash_set_cont recfind_recursion_sett; - typedef hash_set_cont assign_recursion_sett; + typedef std::unordered_map valuest; + typedef std::unordered_set flatten_seent; + typedef std::unordered_set gvs_recursion_sett; + typedef std::unordered_set recfind_recursion_sett; + typedef std::unordered_set assign_recursion_sett; #endif void get_value_set( diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index 872e5ba27f2..c6c5c8920d2 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include #include -#include #include #include #include @@ -123,7 +122,7 @@ void value_set_fivrt::output( { const exprt &o=object_numbering[o_it->first]; - std::string result="<"; //+i2string(o_it->first) + ","; + std::string result="<"; //+std::to_string(o_it->first) + ","; if(o.id()==ID_invalid) { @@ -1720,7 +1719,7 @@ void value_set_fivrt::do_function_call( for(unsigned i=0; itype()); + "argument$"+std::to_string(i), it->type()); exprt actual_lhs=symbol_exprt(identifier, it->type()); assign(actual_lhs, v_expr, ns, true); @@ -1779,7 +1778,7 @@ void value_set_fivrt::do_end_function( { if(lhs.is_nil()) return; - std::string rvs = "value_set::return_value" + i2string(from_function); + std::string rvs = "value_set::return_value" + std::to_string(from_function); symbol_exprt rhs(rvs, lhs.type()); assign(lhs, rhs, ns); @@ -1877,7 +1876,7 @@ void value_set_fivrt::apply_code( // this is turned into an assignment if(code.operands().size()==1) { - std::string rvs = "value_set::return_value" + i2string(from_function); + std::string rvs = "value_set::return_value" + std::to_string(from_function); symbol_exprt lhs(rvs, code.op0().type()); assign(lhs, code.op0(), ns); } diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h index d93aab134bc..e0bb75c0428 100644 --- a/src/pointer-analysis/value_set_fivr.h +++ b/src/pointer-analysis/value_set_fivr.h @@ -10,6 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVR_H +#include +#include +#include + #include #include #include @@ -187,20 +191,20 @@ class value_set_fivrt } }; - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; #ifdef USE_DSTRING typedef std::map valuest; - typedef hash_set_cont flatten_seent; - typedef hash_set_cont gvs_recursion_sett; - typedef hash_set_cont recfind_recursion_sett; - typedef hash_set_cont assign_recursion_sett; + typedef std::unordered_set flatten_seent; + typedef std::unordered_set gvs_recursion_sett; + typedef std::unordered_set recfind_recursion_sett; + typedef std::unordered_set assign_recursion_sett; #else - typedef hash_map_cont valuest; - typedef hash_set_cont flatten_seent; - typedef hash_set_cont gvs_recursion_sett; - typedef hash_set_cont recfind_recursion_sett; - typedef hash_set_cont assign_recursion_sett; + typedef std::unordered_map valuest; + typedef std::unordered_set flatten_seent; + typedef std::unordered_set gvs_recursion_sett; + typedef std::unordered_set recfind_recursion_sett; + typedef std::unordered_set assign_recursion_sett; #endif void get_value_set( diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 239ff5e0d73..10e7c94006a 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com, #include #include #include -#include #include #include #include @@ -126,7 +125,7 @@ void value_set_fivrnst::output_entry( { const exprt &o=object_numbering[o_it->first]; - std::string result="<"; //+i2string(o_it->first) + ","; + std::string result="<"; //+std::to_string(o_it->first) + ","; if(o.id()==ID_invalid) { @@ -1351,7 +1350,7 @@ void value_set_fivrnst::do_function_call( for(unsigned i=0; itype()); + "argument$"+std::to_string(i), it->type()); exprt actual_lhs=symbol_exprt(identifier, it->type()); assign(actual_lhs, v_expr, ns, true); @@ -1411,7 +1410,7 @@ void value_set_fivrnst::do_end_function( if(lhs.is_nil()) return; irep_idt rvs = std::string("value_set::return_value") + - i2string(from_function); + std::to_string(from_function); add_var(rvs, ""); symbol_exprt rhs(rvs, lhs.type()); @@ -1511,7 +1510,7 @@ void value_set_fivrnst::apply_code( if(code.operands().size()==1) { irep_idt rvs = std::string("value_set::return_value") + - i2string(from_function); + std::to_string(from_function); add_var(rvs, ""); symbol_exprt lhs(rvs, code.op0().type()); assign(lhs, code.op0(), ns); diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h index b6b02f3c93b..8031f760e18 100644 --- a/src/pointer-analysis/value_set_fivrns.h +++ b/src/pointer-analysis/value_set_fivrns.h @@ -10,6 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H #define CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H +#include +#include +#include +#include + #include #include #include @@ -186,12 +191,12 @@ class value_set_fivrnst } }; - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; #ifdef USE_DSTRING typedef std::map valuest; #else - typedef hash_map_cont valuest; + typedef std::unordered_map valuest; #endif void get_value_set( diff --git a/src/solvers/cvc/cvc_conv.cpp b/src/solvers/cvc/cvc_conv.cpp index c1c7badc682..2a39409d5e3 100644 --- a/src/solvers/cvc/cvc_conv.cpp +++ b/src/solvers/cvc/cvc_conv.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -129,7 +128,7 @@ std::string cvc_convt::cvc_pointer_type() { assert(config.ansi_c.pointer_width!=0); return "[# object: INT, offset: BITVECTOR("+ - i2string(config.ansi_c.pointer_width)+") #]"; + std::to_string(config.ansi_c.pointer_width)+") #]"; } /*******************************************************************\ @@ -147,7 +146,7 @@ Function: cvc_convt::array_index_type std::string cvc_convt::array_index_type() { return std::string("BITVECTOR(")+ - i2string(32)+")"; + std::to_string(32)+")"; } /*******************************************************************\ @@ -1304,7 +1303,7 @@ void cvc_convt::set_to(const exprt &expr, bool value) if(id.type.is_nil()) { - hash_set_cont s_set; + std::unordered_set s_set; ::find_symbols(expr.op1(), s_set); diff --git a/src/solvers/cvc/cvc_conv.h b/src/solvers/cvc/cvc_conv.h index 87f8a1c65ca..edf9720d0eb 100644 --- a/src/solvers/cvc/cvc_conv.h +++ b/src/solvers/cvc/cvc_conv.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_CVC_CVC_CONV_H #define CPROVER_SOLVERS_CVC_CVC_CONV_H -#include #include #include @@ -56,7 +55,7 @@ class cvc_convt:public prop_convt } }; - typedef hash_map_cont + typedef std::unordered_map identifier_mapt; identifier_mapt identifier_map; diff --git a/src/solvers/cvc/cvc_dec.cpp b/src/solvers/cvc/cvc_dec.cpp index 2a3832b62e2..3b174ac4c2f 100644 --- a/src/solvers/cvc/cvc_dec.cpp +++ b/src/solvers/cvc/cvc_dec.cpp @@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #define getpid _getpid #endif -#include #include #include @@ -44,7 +43,7 @@ Function: cvc_temp_filet::cvc_temp_filet cvc_temp_filet::cvc_temp_filet() { - temp_out_filename="cvc_dec_out_"+i2string(getpid())+".tmp"; + temp_out_filename="cvc_dec_out_"+std::to_string(getpid())+".tmp"; temp_out.open( temp_out_filename.c_str(), @@ -94,7 +93,7 @@ decision_proceduret::resultt cvc_dect::dec_solve() temp_out.close(); temp_result_filename= - "cvc_dec_result_"+i2string(getpid())+".tmp"; + "cvc_dec_result_"+std::to_string(getpid())+".tmp"; std::string command= "cvcl "+temp_out_filename+" > "+temp_result_filename+" 2>&1"; @@ -167,7 +166,7 @@ void cvc_dect::read_assert(std::istream &in, std::string &line) if(line[0]=='l') { - unsigned number=unsafe_c_str2unsigned(line.c_str()+1); + unsigned number=unsafe_string2unsigned(line.substr(1)); assert(number #include -#include #include "cvc_prop.h" @@ -565,9 +564,9 @@ std::string cvc_propt::cvc_literal(literalt l) return "TRUE"; if(l.sign()) - return "(NOT l"+i2string(l.var_no())+")"; + return "(NOT l"+std::to_string(l.var_no())+")"; - return "l"+i2string(l.var_no()); + return "l"+std::to_string(l.var_no()); } /*******************************************************************\ diff --git a/src/solvers/dplib/dplib_conv.cpp b/src/solvers/dplib/dplib_conv.cpp index 7055c5c0015..58b7702f927 100644 --- a/src/solvers/dplib/dplib_conv.cpp +++ b/src/solvers/dplib/dplib_conv.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -59,7 +58,7 @@ std::string dplib_convt::dplib_pointer_type() { assert(config.ansi_c.pointer_width!=0); return "[# object: INT, offset: BITVECTOR("+ - i2string(config.ansi_c.pointer_width)+") #]"; + std::to_string(config.ansi_c.pointer_width)+") #]"; } /*******************************************************************\ @@ -76,7 +75,7 @@ Function: dplib_convt::array_index_type std::string dplib_convt::array_index_type() { - return std::string("SIGNED [")+i2string(32)+"]"; + return std::string("SIGNED [")+std::to_string(32)+"]"; } /*******************************************************************\ @@ -1128,7 +1127,7 @@ void dplib_convt::set_to(const exprt &expr, bool value) if(id.type.is_nil()) { - hash_set_cont s_set; + std::unordered_set s_set; ::find_symbols(expr.op1(), s_set); diff --git a/src/solvers/dplib/dplib_conv.h b/src/solvers/dplib/dplib_conv.h index 494bcb1fb12..a4f2f0558f4 100644 --- a/src/solvers/dplib/dplib_conv.h +++ b/src/solvers/dplib/dplib_conv.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H #define CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H -#include #include #include @@ -64,7 +63,7 @@ class dplib_convt:public prop_convt } }; - typedef hash_map_cont + typedef std::unordered_map identifier_mapt; identifier_mapt identifier_map; diff --git a/src/solvers/dplib/dplib_dec.cpp b/src/solvers/dplib/dplib_dec.cpp index 31403a1b2f3..c4775cb5007 100644 --- a/src/solvers/dplib/dplib_dec.cpp +++ b/src/solvers/dplib/dplib_dec.cpp @@ -23,7 +23,6 @@ Author: Daniel Kroening, kroening@kroening.com #define getpid _getpid #endif -#include #include #include @@ -43,7 +42,7 @@ Function: dplib_temp_filet::dplib_temp_filet dplib_temp_filet::dplib_temp_filet() { - temp_out_filename="dplib_dec_out_"+i2string(getpid())+".tmp"; + temp_out_filename="dplib_dec_out_"+std::to_string(getpid())+".tmp"; temp_out.open( temp_out_filename.c_str(), @@ -95,7 +94,7 @@ decision_proceduret::resultt dplib_dect::dec_solve() temp_out.close(); temp_result_filename= - "dplib_dec_result_"+i2string(getpid())+".tmp"; + "dplib_dec_result_"+std::to_string(getpid())+".tmp"; std::string command= "dplibl "+temp_out_filename+" > "+temp_result_filename+" 2>&1"; diff --git a/src/solvers/dplib/dplib_prop.cpp b/src/solvers/dplib/dplib_prop.cpp index 7f94b1184b3..ea9e169ffda 100644 --- a/src/solvers/dplib/dplib_prop.cpp +++ b/src/solvers/dplib/dplib_prop.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include "dplib_prop.h" @@ -542,9 +541,9 @@ std::string dplib_propt::dplib_literal(literalt l) return "TRUE"; if(l.sign()) - return "(NOT l"+i2string(l.var_no())+")"; + return "(NOT l"+std::to_string(l.var_no())+")"; - return "l"+i2string(l.var_no()); + return "l"+std::to_string(l.var_no()); } /*******************************************************************\ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 16a3cd467e8..ca602dcd6b6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -800,7 +799,7 @@ void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest) bv_sub.resize(bv.size()); for(std::size_t i=0; i #include #include #include @@ -111,7 +110,7 @@ class boolbvt:public arrayst bvt conversion_failed(const exprt &expr); - typedef hash_map_cont bv_cachet; + typedef std::unordered_map bv_cachet; bv_cachet bv_cache; bool type_conversion( diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp index ab9a1c99d51..8fedbbaed8d 100644 --- a/src/solvers/flattening/boolbv_equality.cpp +++ b/src/solvers/flattening/boolbv_equality.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 1a6177138e9..7ec5a6987c4 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include -#include #include "boolbv.h" diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index 35cbb8f54e1..e01b18ea5c0 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include "boolbv.h" @@ -124,7 +123,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) std::string identifier= "__CPROVER_internal_uniform_array_"+ - i2string(uniform_array_counter++); + std::to_string(uniform_array_counter++); symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); @@ -165,7 +164,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) std::string identifier= "__CPROVER_internal_actual_array_"+ - i2string(actual_array_counter++); + std::to_string(actual_array_counter++); symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); diff --git a/src/solvers/flattening/boolbv_map.h b/src/solvers/flattening/boolbv_map.h index 0d4bc2e1c4d..1f2b7458f93 100644 --- a/src/solvers/flattening/boolbv_map.h +++ b/src/solvers/flattening/boolbv_map.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include @@ -55,7 +54,7 @@ class boolbv_mapt std::string get_value(const propt &) const; }; - typedef hash_map_cont mappingt; + typedef std::unordered_map mappingt; mappingt mapping; void show() const; diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index 4d6b6fdb670..87c513ae5db 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -119,7 +119,7 @@ literalt boolbvt::convert_overflow(const exprt &expr) } else if(has_prefix(expr.id_string(), "overflow-typecast-")) { - std::size_t bits=unsafe_c_str2unsigned(expr.id().c_str()+18); + std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18)); const exprt::operandst &operands=expr.operands(); diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h index 80e27d03e5c..6014dd7b198 100644 --- a/src/solvers/flattening/boolbv_width.h +++ b/src/solvers/flattening/boolbv_width.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include class boolbv_widtht { @@ -42,7 +41,7 @@ class boolbv_widtht std::vector members; }; - typedef hash_map_cont cachet; + typedef std::unordered_map cachet; // the 'mutable' is allow const methods above mutable cachet cache; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index c6dee2eb4cd..b4d0382f27a 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -6,9 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include -#include #include #include #include diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index eafed0e6dfb..66253731cbc 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H -#include #include "boolbv.h" #include "pointer_logic.h" diff --git a/src/solvers/flattening/equality.h b/src/solvers/flattening/equality.h index 533f406e010..741552c76f3 100644 --- a/src/solvers/flattening/equality.h +++ b/src/solvers/flattening/equality.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include @@ -33,7 +32,7 @@ class equalityt:public prop_conv_solvert } protected: - typedef hash_map_cont elementst; + typedef std::unordered_map elementst; typedef std::map, literalt> equalitiest; typedef std::map elements_revt; @@ -44,7 +43,7 @@ class equalityt:public prop_conv_solvert equalitiest equalities; }; - typedef hash_map_cont typemapt; + typedef std::unordered_map typemapt; typemapt typemap; diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 4cb77d56b01..ff6568c969c 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include @@ -157,7 +156,7 @@ exprt pointer_logict::pointer_expr( if(pointer.object>=objects.size()) { constant_exprt result(type); - result.set_value("INVALID-"+i2string(pointer.object)); + result.set_value("INVALID-"+std::to_string(pointer.object)); return result; } diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 88232ef5e32..bcf18ca69f7 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H #include -#include #include #include diff --git a/src/solvers/floatbv/float_bv.h b/src/solvers/floatbv/float_bv.h index 10c2b4089e8..d71ef8be4e9 100644 --- a/src/solvers/floatbv/float_bv.h +++ b/src/solvers/floatbv/float_bv.h @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H #define CPROVER_SOLVERS_FLOATBV_FLOAT_BV_H -#include #include #include diff --git a/src/solvers/prop/aig.cpp b/src/solvers/prop/aig.cpp index 42c7713b364..5d5c9839f8e 100644 --- a/src/solvers/prop/aig.cpp +++ b/src/solvers/prop/aig.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "aig.h" @@ -27,7 +26,7 @@ Function: aigt::label std::string aigt::label(nodest::size_type v) const { - return "var("+i2string(v)+")"; + return "var("+std::to_string(v)+")"; } /*******************************************************************\ @@ -44,7 +43,7 @@ Function: aigt::dot_label std::string aigt::dot_label(nodest::size_type v) const { - return "var("+i2string(v)+")"; + return "var("+std::to_string(v)+")"; } /*******************************************************************\ diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h index d34372b300b..608be1694e2 100644 --- a/src/solvers/prop/bdd_expr.h +++ b/src/solvers/prop/bdd_expr.h @@ -39,7 +39,7 @@ class bdd_exprt miniBDD::mgr bdd_mgr; BDDt root; - typedef hash_map_cont expr_mapt; + typedef std::unordered_map expr_mapt; expr_mapt expr_map; typedef std::map node_mapt; node_mapt node_map; diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index 76b496be13a..f250ea9e00a 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -106,7 +105,7 @@ class prop_conv_solvert:public prop_convt virtual void clear_cache() { cache.clear();} typedef std::map symbolst; - typedef hash_map_cont cachet; + typedef std::unordered_map cachet; const cachet &get_cache() const { return cache; } const symbolst &get_symbols() const { return symbols; } diff --git a/src/solvers/qbf/qbf_bdd_core.cpp b/src/solvers/qbf/qbf_bdd_core.cpp index b4df80a92ca..4d4f17da6be 100644 --- a/src/solvers/qbf/qbf_bdd_core.cpp +++ b/src/solvers/qbf/qbf_bdd_core.cpp @@ -9,7 +9,6 @@ Author: CM Wintersteiger #include #include -#include #include #include @@ -192,8 +191,8 @@ propt::resultt qbf_bdd_coret::prop_solve() { std::string msg= solver_text() + ": "+ - i2string(no_variables())+" variables, "+ - i2string(matrix->nodeCount())+" nodes"; + std::to_string(no_variables())+" variables, "+ + std::to_string(matrix->nodeCount())+" nodes"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/qbf/qbf_bdd_core.h b/src/solvers/qbf/qbf_bdd_core.h index 801cf4417e9..4fc8fd1abaa 100644 --- a/src/solvers/qbf/qbf_bdd_core.h +++ b/src/solvers/qbf/qbf_bdd_core.h @@ -11,7 +11,6 @@ Author: CM Wintersteiger #include -#include #include "qdimacs_core.h" @@ -26,7 +25,7 @@ class qbf_bdd_certificatet : public qdimacs_coret typedef std::vector model_bddst; model_bddst model_bdds; - typedef hash_map_cont function_cachet; + typedef std::unordered_map function_cachet; function_cachet function_cache; public: diff --git a/src/solvers/qbf/qbf_skizzo_core.cpp b/src/solvers/qbf/qbf_skizzo_core.cpp index 91ebc01913b..127f4a9e42e 100644 --- a/src/solvers/qbf/qbf_skizzo_core.cpp +++ b/src/solvers/qbf/qbf_skizzo_core.cpp @@ -9,7 +9,6 @@ Author: CM Wintersteiger #include #include -#include #include #include // CUDD Library @@ -102,8 +101,8 @@ propt::resultt qbf_skizzo_coret::prop_solve() { std::string msg= "Skizzo: "+ - i2string(no_variables())+" variables, "+ - i2string(no_clauses())+" clauses"; + std::to_string(no_variables())+" variables, "+ + std::to_string(no_clauses())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/qbf/qbf_squolem.cpp b/src/solvers/qbf/qbf_squolem.cpp index 3033babc937..f6fa86278ab 100644 --- a/src/solvers/qbf/qbf_squolem.cpp +++ b/src/solvers/qbf/qbf_squolem.cpp @@ -6,7 +6,6 @@ Author: CM Wintersteiger \*******************************************************************/ -#include #include "qbf_squolem.h" @@ -94,8 +93,8 @@ propt::resultt qbf_squolemt::prop_solve() { std::string msg= "Squolem: "+ - i2string(no_variables())+" variables, "+ - i2string(no_clauses())+" clauses"; + std::to_string(no_variables())+" variables, "+ + std::to_string(no_clauses())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/qbf/qbf_squolem_core.cpp b/src/solvers/qbf/qbf_squolem_core.cpp index dba0b05f45e..e076e9341a2 100644 --- a/src/solvers/qbf/qbf_squolem_core.cpp +++ b/src/solvers/qbf/qbf_squolem_core.cpp @@ -8,7 +8,6 @@ Author: CM Wintersteiger #include -#include #include #include @@ -166,8 +165,8 @@ propt::resultt qbf_squolem_coret::prop_solve() { std::string msg= "Squolem: "+ - i2string(no_variables())+" variables, "+ - i2string(no_clauses())+" clauses"; + std::to_string(no_variables())+" variables, "+ + std::to_string(no_clauses())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/qbf/qbf_squolem_core.h b/src/solvers/qbf/qbf_squolem_core.h index 7227e5dee27..c09f7d69713 100644 --- a/src/solvers/qbf/qbf_squolem_core.h +++ b/src/solvers/qbf/qbf_squolem_core.h @@ -9,7 +9,6 @@ Author: CM Wintersteiger #ifndef CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H #define CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H -#include #include #include "qdimacs_core.h" @@ -47,7 +46,7 @@ class qbf_squolem_coret:public qdimacs_coret virtual const exprt f_get(literalt l); private: - typedef hash_map_cont function_cachet; + typedef std::unordered_map function_cachet; function_cachet function_cache; const exprt f_get_cnf(WitnessStack *wsp); diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index c319601e716..b6eb359bca7 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include "bv_refinement.h" @@ -87,7 +86,7 @@ decision_proceduret::resultt bv_refinementt::dec_solve() if(ui==ui_message_handlert::XML_UI) { xmlt xml("refinement-iteration"); - xml.data=i2string(iteration); + xml.data=std::to_string(iteration); std::cout << xml << '\n'; } diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 3e10a9e6c6a..eb774866c02 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include #include #include #include @@ -673,6 +672,6 @@ std::string bv_refinementt::approximationt::as_string() const #if 0 return from_expr(expr); #else - return i2string(id_nr)+"/"+id2string(expr.id()); + return std::to_string(id_nr)+"/"+id2string(expr.id()); #endif } diff --git a/src/solvers/sat/satcheck_booleforce.cpp b/src/solvers/sat/satcheck_booleforce.cpp index 5ea0ad75616..6fe9bb6784f 100644 --- a/src/solvers/sat/satcheck_booleforce.cpp +++ b/src/solvers/sat/satcheck_booleforce.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include "satcheck_booleforce.h" diff --git a/src/solvers/sat/satcheck_limmat.cpp b/src/solvers/sat/satcheck_limmat.cpp index 7f9deb899e0..f99db080c7a 100644 --- a/src/solvers/sat/satcheck_limmat.cpp +++ b/src/solvers/sat/satcheck_limmat.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include "satcheck_limmat.h" @@ -156,8 +155,8 @@ propt::resultt satcheck_limmatt::prop_solve() { std::string msg= - i2string(maxvar_Limmat(solver))+" variables, "+ - i2string(clauses_Limmat(solver))+" clauses"; + std::to_string(maxvar_Limmat(solver))+" variables, "+ + std::to_string(clauses_Limmat(solver))+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/src/solvers/sat/satcheck_lingeling.cpp index 4d7e8c55148..4b058569ecf 100644 --- a/src/solvers/sat/satcheck_lingeling.cpp +++ b/src/solvers/sat/satcheck_lingeling.cpp @@ -8,7 +8,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #include -#include #include #include "satcheck_lingeling.h" @@ -117,8 +116,8 @@ propt::resultt satcheck_lingelingt::prop_solve() // We start counting at 1, thus there is one variable fewer. { std::string msg= - i2string(no_variables()-1)+" variables, "+ - i2string(clause_counter)+" clauses"; + std::to_string(no_variables()-1)+" variables, "+ + std::to_string(clause_counter)+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp index 63b8168298a..c701ab88823 100644 --- a/src/solvers/sat/satcheck_picosat.cpp +++ b/src/solvers/sat/satcheck_picosat.cpp @@ -8,7 +8,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #include -#include #include #include "satcheck_picosat.h" @@ -118,8 +117,8 @@ propt::resultt satcheck_picosatt::prop_solve() { std::string msg= - i2string(_no_variables-1)+" variables, "+ - i2string(picosat_added_original_clauses(picosat))+" clauses"; + std::to_string(_no_variables-1)+" variables, "+ + std::to_string(picosat_added_original_clauses(picosat))+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/sat/satcheck_precosat.cpp b/src/solvers/sat/satcheck_precosat.cpp index a04bf21618f..7589d085678 100644 --- a/src/solvers/sat/satcheck_precosat.cpp +++ b/src/solvers/sat/satcheck_precosat.cpp @@ -8,7 +8,6 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #include -#include #include #include "satcheck_precosat.h" @@ -117,8 +116,8 @@ propt::resultt satcheck_precosatt::prop_solve() // We start counting at 1, thus there is one variable fewer. { std::string msg= - i2string(no_variables()-1)+" variables, "+ - i2string(solver->getAddedOrigClauses())+" clauses"; + std::to_string(no_variables()-1)+" variables, "+ + std::to_string(solver->getAddedOrigClauses())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/sat/satcheck_smvsat.cpp b/src/solvers/sat/satcheck_smvsat.cpp index 7feecb3bf0a..2316f07fd95 100644 --- a/src/solvers/sat/satcheck_smvsat.cpp +++ b/src/solvers/sat/satcheck_smvsat.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "satcheck_smvsat.h" diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp index 6af26cda57a..bcca0ff2f2b 100644 --- a/src/solvers/sat/satcheck_zchaff.cpp +++ b/src/solvers/sat/satcheck_zchaff.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include "satcheck_zchaff.h" @@ -151,8 +150,8 @@ propt::resultt satcheck_zchaff_baset::prop_solve() { std::string msg= - i2string(solver->num_variables())+" variables, "+ - i2string(solver->clauses().size())+" clauses"; + std::to_string(solver->num_variables())+" variables, "+ + std::to_string(solver->clauses().size())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/sat/satcheck_zcore.cpp b/src/solvers/sat/satcheck_zcore.cpp index 5749b482508..700d632bfec 100644 --- a/src/solvers/sat/satcheck_zcore.cpp +++ b/src/solvers/sat/satcheck_zcore.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "satcheck_zcore.h" @@ -100,8 +99,8 @@ propt::resultt satcheck_zcoret::prop_solve() // We start counting at 1, thus there is one variable fewer. { std::string msg= - i2string(no_variables()-1)+" variables, "+ - i2string(no_clauses())+" clauses"; + std::to_string(no_variables()-1)+" variables, "+ + std::to_string(no_clauses())+" clauses"; messaget::status() << msg << messaget::eom; } diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp index b89dc8b4525..44bb59cb63c 100644 --- a/src/solvers/smt1/smt1_conv.cpp +++ b/src/solvers/smt1/smt1_conv.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -674,7 +673,7 @@ std::string smt1_convt::convert_identifier(const irep_idt &identifier) else { dest+='.'; - dest.append(i2string(ch)); + dest.append(std::to_string(ch)); dest+='.'; } } @@ -3259,7 +3258,7 @@ void smt1_convt::find_symbols(const exprt &expr) { if(array_of_map.find(expr)==array_of_map.end()) { - irep_idt id="array_of'"+i2string(array_of_map.size()); + irep_idt id="array_of'"+std::to_string(array_of_map.size()); out << "; the following is a poor substitute for lambda i. x" << "\n"; out << ":extrafuns((" << id @@ -3296,7 +3295,7 @@ void smt1_convt::find_symbols(const exprt &expr) if(array_expr_map.find(expr)==array_expr_map.end()) { // introduce a temporary array. - irep_idt id="array_init'"+i2string(array_expr_map.size()); + irep_idt id="array_init'"+std::to_string(array_expr_map.size()); out << ":extrafuns((" << id << " "; @@ -3313,7 +3312,7 @@ void smt1_convt::find_symbols(const exprt &expr) string2array_map[expr]=t; // introduce a temporary array. - irep_idt id="string'"+i2string(array_expr_map.size()); + irep_idt id="string'"+std::to_string(array_expr_map.size()); out << ":extrafuns((" << id << " "; diff --git a/src/solvers/smt1/smt1_conv.h b/src/solvers/smt1/smt1_conv.h index 8785f3f70c0..a51eb8bd438 100644 --- a/src/solvers/smt1/smt1_conv.h +++ b/src/solvers/smt1/smt1_conv.h @@ -13,7 +13,6 @@ Revision: Roberto Bruttomesso, roberto.bruttomesso@unisi.ch #include #include -#include #include #include @@ -155,7 +154,7 @@ class smt1_convt:public prop_convt identifier.value=tmp; } - typedef hash_map_cont + typedef std::unordered_map identifier_mapt; identifier_mapt identifier_map; diff --git a/src/solvers/smt1/smt1_dec.cpp b/src/solvers/smt1/smt1_dec.cpp index 66a62a34234..ee1615ad48b 100644 --- a/src/solvers/smt1/smt1_dec.cpp +++ b/src/solvers/smt1/smt1_dec.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -251,7 +250,7 @@ decision_proceduret::resultt smt1_dect::read_result_boolector(std::istream &in) boolean_assignment.clear(); boolean_assignment.resize(no_boolean_variables, false); - typedef hash_map_cont valuest; + typedef std::unordered_map valuest; valuest values; while(std::getline(in, line)) @@ -306,7 +305,7 @@ decision_proceduret::resultt smt1_dect::read_result_boolector(std::istream &in) for(unsigned v=0; v valuest; + typedef std::unordered_map valuest; valuest values; while(std::getline(in, line)) @@ -471,7 +470,7 @@ decision_proceduret::resultt smt1_dect::read_result_mathsat(std::istream &in) // Booleans for(unsigned v=0; v valuest; + typedef std::unordered_map valuest; valuest values; while(std::getline(in, line)) @@ -537,7 +536,7 @@ decision_proceduret::resultt smt1_dect::read_result_z3(std::istream &in) // Booleans for(unsigned v=0; v valuest; + typedef std::unordered_map valuest; valuest values; while(std::getline(in, line)) @@ -786,7 +785,7 @@ decision_proceduret::resultt smt1_dect::read_result_cvc3(std::istream &in) // Booleans for(unsigned v=0; v -#include #include "smt1_prop.h" @@ -442,7 +441,7 @@ std::string smt1_propt::smt1_literal(literalt l) else if(l==const_literal(true)) return "true"; - std::string v="B"+i2string(l.var_no()); + std::string v="B"+std::to_string(l.var_no()); if(l.sign()) return "(not "+v+")"; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 5d83d2de701..1f66f7920dc 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -928,7 +927,7 @@ void smt2_convt::convert_literal(const literalt l) if(l.sign()) out << ")"; - smt2_identifiers.insert("B"+i2string(l.var_no())); + smt2_identifiers.insert("B"+std::to_string(l.var_no())); } } @@ -962,7 +961,7 @@ std::string smt2_convt::convert_identifier(const irep_idt &identifier) case '\\': case '&': // we use the & for escaping result+='&'; - result+=i2string(ch); + result+=std::to_string(ch); result+=';'; break; @@ -992,19 +991,19 @@ std::string smt2_convt::type2id(const typet &type) const if(type.id()==ID_floatbv) { ieee_float_spect spec(to_floatbv_type(type)); - return "f"+i2string(spec.width())+"_"+i2string(spec.f); + return "f"+std::to_string(spec.width())+"_"+std::to_string(spec.f); } else if(type.id()==ID_unsignedbv) { - return "u"+i2string(to_unsignedbv_type(type).get_width()); + return "u"+std::to_string(to_unsignedbv_type(type).get_width()); } else if(type.id()==ID_c_bool) { - return "u"+i2string(to_c_bool_type(type).get_width()); + return "u"+std::to_string(to_c_bool_type(type).get_width()); } else if(type.id()==ID_signedbv) { - return "s"+i2string(to_signedbv_type(type).get_width()); + return "s"+std::to_string(to_signedbv_type(type).get_width()); } else if(type.id()==ID_bool) { @@ -4618,7 +4617,7 @@ void smt2_convt::find_symbols(const exprt &expr) { if(defined_expressions.find(expr)==defined_expressions.end()) { - irep_idt id="array_of."+i2string(defined_expressions.size()); + irep_idt id="array_of."+std::to_string(defined_expressions.size()); out << "; the following is a substitute for lambda i. x" << "\n"; out << "(declare-fun " << id << " () "; convert_type(expr.type()); @@ -4642,7 +4641,7 @@ void smt2_convt::find_symbols(const exprt &expr) { const array_typet &array_type=to_array_type(expr.type()); - irep_idt id="array."+i2string(defined_expressions.size()); + irep_idt id="array."+std::to_string(defined_expressions.size()); out << "; the following is a substitute for an array constructor" << "\n"; out << "(declare-fun " << id << " () "; convert_type(array_type); @@ -4668,7 +4667,7 @@ void smt2_convt::find_symbols(const exprt &expr) exprt tmp=to_string_constant(expr).to_array_expr(); const array_typet &array_type=to_array_type(tmp.type()); - irep_idt id="string."+i2string(defined_expressions.size()); + irep_idt id="string."+std::to_string(defined_expressions.size()); out << "; the following is a substitute for a string" << "\n"; out << "(declare-fun " << id << " () "; convert_type(array_type); @@ -4696,7 +4695,7 @@ void smt2_convt::find_symbols(const exprt &expr) { if (object_sizes.find(expr)==object_sizes.end()) { - irep_idt id="object_size."+i2string(object_sizes.size()); + irep_idt id="object_size."+std::to_string(object_sizes.size()); out << "(declare-fun " << id << " () "; convert_type(expr.type()); out << ")" << "\n"; @@ -4753,7 +4752,7 @@ void smt2_convt::find_symbols(const exprt &expr) exprt tmp1=expr; for(unsigned i=0; i #include -#include #include #include @@ -165,7 +164,7 @@ class smt2_convt:public prop_convt // letification typedef std::pair let_count_id; - typedef hash_map_cont seen_expressionst; + typedef std::unordered_map seen_expressionst; unsigned let_id_count; const static unsigned LET_COUNT = 2; @@ -265,7 +264,7 @@ class smt2_convt:public prop_convt } }; - typedef hash_map_cont + typedef std::unordered_map identifier_mapt; identifier_mapt identifier_map; diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 362d18ece96..722a6b43bee 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include "smt2_dec.h" @@ -238,7 +237,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) boolean_assignment.clear(); boolean_assignment.resize(no_boolean_variables, false); - typedef hash_map_cont valuest; + typedef std::unordered_map valuest; valuest values; while(in) @@ -290,7 +289,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) // Booleans for(unsigned v=0; v -#include #include "smt2_prop.h" @@ -489,7 +488,7 @@ std::string smt2_propt::smt2_literal(literalt l) else if(l==const_literal(true)) return "true"; - std::string v="B"+i2string(l.var_no()); + std::string v="B"+std::to_string(l.var_no()); smt2_identifiers.insert(v); diff --git a/src/symex/symex_cover.cpp b/src/symex/symex_cover.cpp index 3f907a67477..2b4f88c6afc 100644 --- a/src/symex/symex_cover.cpp +++ b/src/symex/symex_cover.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include @@ -191,8 +190,8 @@ void symex_parse_optionst::report_cover( } } } - json_result["totalGoals"]=json_numbert(i2string(property_map.size())); - json_result["goalsCovered"]=json_numbert(i2string(goals_covered)); + json_result["totalGoals"]=json_numbert(std::to_string(property_map.size())); + json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); std::cout << ",\n" << json_result; break; } diff --git a/src/util/Makefile b/src/util/Makefile index 2fddfa618bb..f98b6588df8 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -1,5 +1,5 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ - expr.cpp expr_util.cpp i2string.cpp irep.cpp language.cpp \ + expr.cpp expr_util.cpp irep.cpp language.cpp \ lispexpr.cpp lispirep.cpp source_location.cpp message.cpp language_file.cpp \ mp_arith.cpp namespace.cpp parse_options.cpp rename.cpp \ replace_expr.cpp threeval.cpp typecheck.cpp graph.cpp \ @@ -9,7 +9,7 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \ simplify_expr_array.cpp simplify_expr_struct.cpp \ simplify_expr_boolean.cpp simplify_expr_pointer.cpp \ get_module.cpp string_hash.cpp string_container.cpp identifier.cpp \ - rational.cpp options.cpp c_misc.cpp dstring.cpp \ + rational.cpp options.cpp dstring.cpp \ find_symbols.cpp rational_tools.cpp ui_message.cpp simplify_utils.cpp \ time_stopping.cpp symbol.cpp irep_hash_container.cpp cout_message.cpp \ type_eq.cpp guard.cpp array_name.cpp message_stream.cpp \ diff --git a/src/util/config.cpp b/src/util/config.cpp index 6ffbd3505f0..48021c5754a 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "cmdline.h" #include "simplify_expr.h" -#include "i2string.h" #include "std_expr.h" #include "cprover_prefix.h" @@ -539,7 +538,7 @@ void configt::ansi_ct::set_arch_spec_mips(const irep_idt &subarch) case flavourt::GCC: defines.push_back("__mips__"); defines.push_back("mips"); - defines.push_back("_MIPS_SZPTR="+i2string(config.ansi_c.pointer_width)); + defines.push_back("_MIPS_SZPTR="+std::to_string(config.ansi_c.pointer_width)); break; case flavourt::VISUAL_STUDIO: diff --git a/src/util/endianness_map.h b/src/util/endianness_map.h index 4d5fd9825b6..efb09f195c0 100644 --- a/src/util/endianness_map.h +++ b/src/util/endianness_map.h @@ -17,11 +17,11 @@ Author: Daniel Kroening, kroening@kroening.com */ #include +#include #include -#include "expr.h" - class namespacet; +class typet; /*! \brief Maps a big-endian offset to a little-endian offset */ diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 63e57aa3640..135f64a6313 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -197,67 +197,6 @@ exprt gen_one(const typet &type) /*******************************************************************\ -Function: gen_not - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt gen_unary(const irep_idt &id, const typet &type, const exprt &op); - -exprt gen_not(const exprt &op) -{ - return gen_unary(ID_not, bool_typet(), op); -} - -/*******************************************************************\ - -Function: gen_unary - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt gen_unary(const irep_idt &id, const typet &type, const exprt &op) -{ - exprt result(id, type); - result.copy_to_operands(op); - return result; -} - -/*******************************************************************\ - -Function: gen_binary - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -exprt gen_binary( - const irep_idt &id, - const typet &type, - const exprt &op1, - const exprt &op2) -{ - exprt result(id, type); - result.copy_to_operands(op1, op2); - return result; -} - -/*******************************************************************\ - Function: make_next_state Inputs: diff --git a/src/util/expr_util.h b/src/util/expr_util.h index 513b7cfb342..95430d563ce 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -33,13 +33,6 @@ class namespacet; exprt gen_zero(const typet &type); /*! \copydoc gen_zero(const typet &) */ exprt gen_one(const typet &type); -/*! \copydoc gen_zero(const typet &) */ -exprt gen_not_old(const exprt &op); - -/*! \copydoc gen_zero(const typet &) */ -void gen_and_old(exprt &expr); -/*! \copydoc gen_zero(const typet &) */ -void gen_or_old(exprt &expr); /*! \copydoc gen_zero(const typet &) */ void make_next_state(exprt &); diff --git a/src/util/find_macros.h b/src/util/find_macros.h index 86f56e2ef8c..17b8282502c 100644 --- a/src/util/find_macros.h +++ b/src/util/find_macros.h @@ -9,13 +9,14 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_FIND_MACROS_H #define CPROVER_UTIL_FIND_MACROS_H -#include "hash_cont.h" +#include + #include "irep.h" class exprt; class namespacet; -typedef hash_set_cont find_macros_sett; +typedef std::unordered_set find_macros_sett; void find_macros( const exprt &src, diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h index 6f53cdc21b1..4ca899e4b40 100644 --- a/src/util/find_symbols.h +++ b/src/util/find_symbols.h @@ -10,15 +10,15 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_FIND_SYMBOLS_H #include +#include -#include "hash_cont.h" #include "irep.h" class exprt; class symbol_exprt; class typet; -typedef hash_set_cont find_symbols_sett; +typedef std::unordered_set find_symbols_sett; void find_symbols( const exprt &src, diff --git a/src/util/gcd.cpp b/src/util/gcd.cpp deleted file mode 100644 index baabead7436..00000000000 --- a/src/util/gcd.cpp +++ /dev/null @@ -1,49 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include - -#include "gcd.h" - -/*******************************************************************\ - -Function: gcd - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -#if 0 -mp_integer gcd(const mp_integer &_a, const mp_integer &_b) -{ - mp_integer a=_a, b=_b; - - if(a.is_negative()) a.negate(); - if(b.is_negative()) b.negate(); - - if(a==1) return a; - if(b==1) return b; - if(a==b) return a; - - while(!b.is_zero()) - { - mp_integer tmp_b=b; - b=a%b; - assert(b #include #include "get_module.h" #include "message.h" #include "symbol_table.h" +typedef std::list symbolptr_listt; + +#define forall_symbolptr_list(it, list) \ + for(symbolptr_listt::const_iterator it=(list).begin(); \ + it!=(list).end(); ++it) + +#define Forall_symbolptr_list(it, list) \ + for(symbolptr_listt::iterator it=(list).begin(); \ + it!=(list).end(); ++it) + /*******************************************************************\ Function: get_module_by_name diff --git a/src/util/guard.cpp b/src/util/guard.cpp index 4ca0b0fd2b6..e5362143018 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -285,6 +285,10 @@ Function: guardt::is_false \*******************************************************************/ +#define forall_guard(it, guard_list) \ + for(guardt::guard_listt::const_iterator it=(guard_list).begin(); \ + it!=(guard_list).end(); ++it) + bool guardt::is_false() const { forall_guard(it, guard_list) diff --git a/src/util/guard.h b/src/util/guard.h index 8a8508520fd..7344fc10d2e 100644 --- a/src/util/guard.h +++ b/src/util/guard.h @@ -88,14 +88,4 @@ class guardt:public exprt #endif }; -#if 0 -#define Forall_guard(it, guard_list) \ - for(guardt::guard_listt::iterator it=(guard_list).begin(); \ - it!=(guard_list).end(); ++it) - -#define forall_guard(it, guard_list) \ - for(guardt::guard_listt::const_iterator it=(guard_list).begin(); \ - it!=(guard_list).end(); ++it) -#endif - #endif // CPROVER_UTIL_GUARD_H diff --git a/src/util/hash_cont.h b/src/util/hash_cont.h deleted file mode 100644 index d6365bab7b1..00000000000 --- a/src/util/hash_cont.h +++ /dev/null @@ -1,93 +0,0 @@ -/*******************************************************************\ - -Module: STL Hash map / set - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_HASH_CONT_H -#define CPROVER_UTIL_HASH_CONT_H - -// You need to pick one of the following options: -// -// #define STL_HASH_NONE -// #define STL_HASH_STDEXT -// #define STL_HASH_GNU -// #define STL_HASH_TR1 -// #define STL_HASH_STD -// -// The default is 'STL_HASH_STD'. This file will go away one day. - -#if !defined(STL_HASH_NONE) && !defined(STL_HASH_STDEXT) && \ - !defined(STL_HASH_GNU) && !defined(STL_HASH_TR1) && \ - !defined(STL_HASH_STD) -#define STL_HASH_STD -#endif - -#if defined(STL_HASH_NONE) - -#include -#include - -template -typedef std::map hash_map_cont; - -template -typedef std::set hash_set_cont; - -template -typedef std::multiset hash_multiset_cont; - -#elif defined(STL_HASH_STDEXT) - -#include -#include - -// for Visual Studio >= 2003 - -#define hash_map_cont stdext::hash_map -#define hash_set_cont stdext::hash_set -#define hash_multiset_cont stdext::hash_multiset - -#elif defined(STL_HASH_GNU) - -#include -#include - -// for new g++ libraries >= 3.2 - -#define hash_map_cont __gnu_cxx::hash_map -#define hash_set_cont __gnu_cxx::hash_set -#define hash_multiset_cont __gnu_cxx::hash_multiset - -#elif defined(STL_HASH_TR1) - -#ifdef _MSC_VER -#include -#include -#else -#include -#include -#endif - -#define hash_map_cont std::tr1::unordered_map -#define hash_set_cont std::tr1::unordered_set -#define hash_multiset_cont std::tr1::unordered_multiset - -#elif defined(STL_HASH_STD) - -#include -#include - -#define hash_map_cont std::unordered_map -#define hash_set_cont std::unordered_set -#define hash_multiset_cont std::unordered_multiset - -#else - -#error Please select hash container option - -#endif - -#endif // CPROVER_UTIL_HASH_CONT_H diff --git a/src/util/i2string.cpp b/src/util/i2string.cpp deleted file mode 100644 index 597c7b098a5..00000000000 --- a/src/util/i2string.cpp +++ /dev/null @@ -1,186 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#define USE_SPRINTF - -#ifdef USE_SPRINTF - -#include -#include - -#include "i2string.h" - -#ifdef _WIN32 -#ifndef __MINGW32__ -#define snprintf sprintf_s -#endif -#endif - -#include - -#include "i2string.h" - -#endif - -/*******************************************************************\ - -Function: i2string - - Inputs: signed integer - - Outputs: string class - - Purpose: convert signed integer to string class - -\*******************************************************************/ - -std::string i2string(int i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%d", i); - return buffer; - #else - std::ostringstream strInt; - strInt << i; - return strInt.str(); - #endif -} - -/*******************************************************************\ - -Function: i2string - - Inputs: signed long integer - - Outputs: string class - - Purpose: convert signed integer to string class - -\*******************************************************************/ - -std::string i2string(signed long int i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%ld", i); - return buffer; - #else - std::ostringstream strInt; - strInt << i; - return strInt.str(); - #endif -} - -/*******************************************************************\ - -Function: i2string - - Inputs: unsigned integer - - Outputs: string class - - Purpose: convert unsigned integer to string class - -\*******************************************************************/ - -std::string i2string(unsigned i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%u", i); - return buffer; - #else - std::ostringstream strInt; - strInt << i; - return strInt.str(); - #endif -} - -/*******************************************************************\ - -Function: i2string - - Inputs: unsigned long integer - - Outputs: string class - - Purpose: convert unsigned integer to string class - -\*******************************************************************/ - -std::string i2string(unsigned long int i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%lu", i); - return buffer; - #else - std::ostringstream strInt; - strInt << i; - return strInt.str(); - #endif -} - -/*******************************************************************\ - -Function: i2string - - Inputs: signed long long - - Outputs: string class - - Purpose: convert signed integer to string class - -\*******************************************************************/ - -std::string i2string(signed long long i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%lld", i); - return buffer; - #else - std::ostringstream strInt; - - strInt << i; - std::string str; - strstream2string(strInt, str); - - return str; - #endif -} - -/*******************************************************************\ - -Function: i2string - - Inputs: unsigned long long - - Outputs: string class - - Purpose: convert unsigned integer to string class - -\*******************************************************************/ - -std::string i2string(unsigned long long i) -{ - #ifdef USE_SPRINTF - char buffer[100]; - snprintf(buffer, sizeof(buffer), "%llu", i); - return buffer; - #else - std::ostringstream strInt; - - strInt << i; - std::string str; - strstream2string(strInt, str); - - return str; - #endif -} diff --git a/src/util/i2string.h b/src/util/i2string.h deleted file mode 100644 index 71f8eafbab0..00000000000 --- a/src/util/i2string.h +++ /dev/null @@ -1,23 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_I2STRING_H -#define CPROVER_UTIL_I2STRING_H - -#include - -// One day, the below will be replaced by C++11's std::to_string. - -std::string i2string(int i); -std::string i2string(signed long int i); -std::string i2string(signed long long int i); -std::string i2string(unsigned int i); -std::string i2string(unsigned long int i); -std::string i2string(unsigned long long int i); - -#endif // CPROVER_UTIL_I2STRING_H diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 57659139ae0..6ad3e417e39 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "std_types.h" #include "std_expr.h" #include "ieee_float.h" -#include "i2string.h" /*******************************************************************\ diff --git a/src/util/irep.cpp b/src/util/irep.cpp index ef67d57a32c..3adafe3d885 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "string2int.h" #include "irep.h" -#include "i2string.h" #include "string_hash.h" #include "irep_hash.h" @@ -426,7 +425,7 @@ Function: irept::set void irept::set(const irep_namet &name, const long long value) { - add(name).id(i2string(value)); + add(name).id(std::to_string(value)); } /*******************************************************************\ @@ -969,7 +968,7 @@ std::string irept::pretty(unsigned indent, unsigned max_indent) const result+="\n"; indent_str(result, indent); - result+=i2string(count++); + result+=std::to_string(count++); result+=": "; result+=it->pretty(indent+2, max_indent); diff --git a/src/util/irep_hash_container.h b/src/util/irep_hash_container.h index 6e9025da16c..45894b9d79d 100644 --- a/src/util/irep_hash_container.h +++ b/src/util/irep_hash_container.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "numbering.h" -#include "hash_cont.h" class irept; @@ -45,7 +44,7 @@ class irep_hash_container_baset } }; - typedef hash_map_cont ptr_hasht; + typedef std::unordered_map ptr_hasht; ptr_hasht ptr_hash; // this is the second level: content diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 7fd4f265f3f..2986decd223 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -14,7 +14,6 @@ Author: Peter Schrammel #include "fixedbv.h" #include "std_expr.h" #include "config.h" -#include "i2string.h" #include "json_expr.h" @@ -74,28 +73,28 @@ json_objectt json( { result["name"]=json_stringt("integer"); result["width"]= - json_numbert(i2string(to_unsignedbv_type(type).get_width())); + json_numbert(std::to_string(to_unsignedbv_type(type).get_width())); } else if(type.id()==ID_signedbv) { result["name"]=json_stringt("integer"); - result["width"]=json_numbert(i2string(to_signedbv_type(type).get_width())); + result["width"]=json_numbert(std::to_string(to_signedbv_type(type).get_width())); } else if(type.id()==ID_floatbv) { result["name"]=json_stringt("float"); - result["width"]=json_numbert(i2string(to_floatbv_type(type).get_width())); + result["width"]=json_numbert(std::to_string(to_floatbv_type(type).get_width())); } else if(type.id()==ID_bv) { result["name"]=json_stringt("integer"); - result["width"]=json_numbert(i2string(to_bv_type(type).get_width())); + result["width"]=json_numbert(std::to_string(to_bv_type(type).get_width())); } else if(type.id()==ID_c_bit_field) { result["name"]=json_stringt("integer"); result["width"]= - json_numbert(i2string(to_c_bit_field_type(type).get_width())); + json_numbert(std::to_string(to_c_bit_field_type(type).get_width())); } else if(type.id()==ID_c_enum_tag) { @@ -105,7 +104,7 @@ json_objectt json( else if(type.id()==ID_fixedbv) { result["name"]=json_stringt("fixed"); - result["width"]=json_numbert(i2string(to_fixedbv_type(type).get_width())); + result["width"]=json_numbert(std::to_string(to_fixedbv_type(type).get_width())); } else if(type.id()==ID_pointer) { @@ -189,7 +188,7 @@ json_objectt json( result["name"]=json_stringt("integer"); result["binary"]=json_stringt(expr.get_string(ID_value)); - result["width"]=json_numbert(i2string(width)); + result["width"]=json_numbert(std::to_string(width)); const typet &underlying_type= type.id()==ID_c_bit_field?type.subtype(): @@ -281,7 +280,7 @@ json_objectt json( forall_operands(it, expr) { json_objectt &e=elements.push_back().make_object(); - e["index"]=json_numbert(i2string(index)); + e["index"]=json_numbert(std::to_string(index)); e["value"]=json(*it, ns); index++; } diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp index eaaa1ea00b2..f7a49991d63 100644 --- a/src/util/language_file.cpp +++ b/src/util/language_file.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "i2string.h" #include "language.h" #include "language_file.h" @@ -172,7 +171,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table) while(modulemap.find(module_name)!=modulemap.end()) { - module_name=*mo_it+"#"+i2string(collision_counter); + module_name=*mo_it+"#"+std::to_string(collision_counter); collision_counter++; } diff --git a/src/util/merge_irep.h b/src/util/merge_irep.h index 647654386b4..a7f182e9b6b 100644 --- a/src/util/merge_irep.h +++ b/src/util/merge_irep.h @@ -9,8 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_MERGE_IREP_H #define CPROVER_UTIL_MERGE_IREP_H +#include + #include "irep.h" -#include "hash_cont.h" class merged_irept:public irept { @@ -82,10 +83,10 @@ class merged_irepst } protected: - typedef hash_set_cont merged_irep_storet; + typedef std::unordered_set merged_irep_storet; merged_irep_storet merged_irep_store; - typedef hash_set_cont to_be_merged_irep_storet; + typedef std::unordered_set to_be_merged_irep_storet; to_be_merged_irep_storet to_be_merged_irep_store; const merged_irept &merged(const irept &); @@ -101,7 +102,7 @@ class merge_irept void operator()(irept &); protected: - typedef hash_set_cont irep_storet; + typedef std::unordered_set irep_storet; irep_storet irep_store; const irept & merged(const irept &irep); @@ -113,7 +114,7 @@ class merge_full_irept void operator()(irept &); protected: - typedef hash_set_cont irep_storet; + typedef std::unordered_set irep_storet; irep_storet irep_store; const irept& merged(const irept &irep); diff --git a/src/util/message.cpp b/src/util/message.cpp index c1f0e36df18..bf2ef47e092 100644 --- a/src/util/message.cpp +++ b/src/util/message.cpp @@ -7,7 +7,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "message.h" -#include "i2string.h" /*******************************************************************\ diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp index 1222fddffb6..1c18d29da96 100644 --- a/src/util/namespace.cpp +++ b/src/util/namespace.cpp @@ -37,7 +37,8 @@ unsigned get_max( forall_symbols(it, symbols) if(has_prefix(id2string(it->first), prefix)) max_nr= - std::max(unsafe_c_str2unsigned(it->first.c_str()+prefix.size()), + std::max(unsafe_string2unsigned( + id2string(it->first).substr(prefix.size())), max_nr); return max_nr; diff --git a/src/util/namespace_utils.h b/src/util/namespace_utils.h deleted file mode 100644 index 3cbf117fd1c..00000000000 --- a/src/util/namespace_utils.h +++ /dev/null @@ -1,104 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -// THIS FILE IS DEPRECATED - -#ifndef CPROVER_UTIL_NAMESPACE_UTILS_H -#define CPROVER_UTIL_NAMESPACE_UTILS_H - -#include "namespace.h" -#include "base_type.h" -#include "type_eq.h" -#include "std_expr.h" - -// second: true <=> not found - -class namespace_utils_baset -{ - public: - virtual ~namespace_utils_baset() - { - } - - const symbolt &lookup(const irep_idt &name) const - { - const symbolt *symbol; - if(lookup(name, symbol)) - throw "identifier "+id2string(name)+" not found"; - return *symbol; - } - - const symbolt &lookup(const symbol_exprt &symbol_expr) const - { - const symbolt *symbol; - if(lookup(symbol_expr.get_identifier(), symbol)) - throw "identifier "+id2string(symbol_expr.get_identifier())+" not found"; - return *symbol; - } - - bool lookup(const irep_idt &name, const symbolt *&symbol) const - { - return ns().lookup(name, symbol); - } - - bool lookup_symbol(const exprt &symbol_expr, const symbolt *&symbol) const - { - return ns().lookup(symbol_expr.get(ID_identifier), symbol); - } - - void follow_symbol(irept &irep) const - { - ns().follow_symbol(irep); - } - - void follow_macros(exprt &expr) const - { - ns().follow_macros(expr); - } - - /* - void base_type(typet &type) - { - ::base_type(type, ns()); - } - - void base_type(exprt &expr) - { - ::base_type(expr, ns()); - } - */ - - bool type_eq(const typet &type1, const typet &type2) - { - return ::type_eq(type1, type2, ns()); - } - - bool base_type_eq(const typet &type1, const typet &type2) - { - return ::base_type_eq(type1, type2, ns()); - } - - protected: - virtual const namespacet &ns() const=0; -}; - -class namespace_utilst:public virtual namespace_utils_baset -{ - public: - namespace_utilst(const namespacet &_ns):__ns(_ns){} - - protected: - const namespacet &__ns; - - virtual const namespacet &ns() const - { - return __ns; - } -}; - -#endif // CPROVER_UTIL_NAMESPACE_UTILS_H diff --git a/src/util/numbering.h b/src/util/numbering.h index d4fccd81e9d..23aabfce0f2 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -11,9 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include "hash_cont.h" template class numbering:public std::vector @@ -108,7 +108,7 @@ class hash_numbering:public std::vector protected: typedef std::vector subt; - typedef hash_map_cont numberst; + typedef std::unordered_map numberst; numberst numbers; }; diff --git a/src/util/old/bitvector.cpp b/src/util/old/bitvector.cpp deleted file mode 100644 index 1c2fc7086e8..00000000000 --- a/src/util/old/bitvector.cpp +++ /dev/null @@ -1,56 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#if 0 -#include "string2int.h" -#include "type.h" -#include "bitvector.h" - -/*******************************************************************\ - -Function: bv_sem - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bv_semt bv_sem(const typet &type) -{ - if(type.id()==ID_bv) - return BV_NONE; - else if(type.id()==ID_unsignedbv) - return BV_UNSIGNED; - else if(type.id()==ID_signedbv) - return BV_SIGNED; - - return BV_UNKNOWN; -} - -/*******************************************************************\ - -Function: bv_width - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -unsigned bv_width(const typet &type) -{ - return unsafe_string2unsigned(type.get_string(ID_width)); -} - - -#endif diff --git a/src/util/old/bitvector.h b/src/util/old/bitvector.h deleted file mode 100644 index 76451fd8613..00000000000 --- a/src/util/old/bitvector.h +++ /dev/null @@ -1,10 +0,0 @@ -// This file is deprecated, and will disappear. - -//class typet; - -//typedef enum { BV_UNKNOWN, BV_NONE, BV_SIGNED, BV_UNSIGNED } bv_semt; - -//bv_semt bv_sem(const typet &type); - -// depreciated, and will disappear -//unsigned bv_width(const typet &type); diff --git a/src/util/old/cnf_simplify.cpp b/src/util/old/cnf_simplify.cpp deleted file mode 100644 index a47702e521d..00000000000 --- a/src/util/old/cnf_simplify.cpp +++ /dev/null @@ -1,247 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include - -#include "cnf_simplify.h" -#include "expr.h" - -void cnf_propagate_not(exprt &expr); -void cnf_join_binary(exprt &expr); -void propagate_not(exprt &expr); - -/*******************************************************************\ - -Function: cnf_simplify - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void cnf_simplify(exprt &expr) -{ - cnf_propagate_not(expr); - cnf_join_binary(expr); -} - -#if 0 -/*******************************************************************\ - -Function: - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void cnf_join_binary(exprt &expr) -{ - Forall_operands(it, expr) - cnf_join_binary(*it); - - if(expr.id()==ID_and || expr.id()==ID_or || expr.id()==ID_xor || - expr.id()==ID_bitand || expr.id()==ID_bitor || expr.id()==ID_bitxor) - { - exprt tmp; - - if(expr.operands().size()==1) - { - tmp.swap(expr.op0()); - expr.swap(tmp); - } - else - { - unsigned count=0; - - forall_operands(it, expr) - { - if(it->id()==expr.id()) - count+=it->operands().size(); - else - count++; - } - - tmp.operands().reserve(count); - - Forall_operands(it, expr) - { - if(it->id()==expr.id()) - { - Forall_operands(it2, *it) - tmp.move_to_operands(*it2); - } - else - tmp.move_to_operands(*it); - } - - expr.operands().swap(tmp.operands()); - } - } -} -#endif - -/*******************************************************************\ - -Function: cnf_join_binary_collect - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void cnf_join_binary_collect(exprt &expr, exprt::operandst &list) -{ - Forall_operands(it, expr) - { - if(it->id()==expr.id() && it->type()==expr.type()) - cnf_join_binary_collect(*it, list); - else - { - list.resize(list.size()+1); - list.back().swap(*it); - } - } -} - -/*******************************************************************\ - -Function: cnf_join_binary - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void cnf_join_binary(exprt &expr) -{ - if(expr.id()==ID_and || expr.id()==ID_or || expr.id()==ID_xor || - expr.id()==ID_bitand || expr.id()==ID_bitor || expr.id()==ID_bitxor) - { - exprt::operandst list; - - cnf_join_binary_collect(expr, list); - - if(list.size()==1) - expr.swap(list.front()); - else - expr.operands().swap(list); - } - - Forall_operands(it, expr) - cnf_join_binary(*it); -} - -/*******************************************************************\ - -Function: cnf_propagate_not - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void cnf_propagate_not(exprt &expr) -{ - if(expr.id()==ID_not) - { - if(expr.operands().size()==1) - { - exprt tmp; - - tmp.swap(expr.op0()); - propagate_not(tmp); - expr.swap(tmp); - } - } - else if(expr.id()==ID_nor) - { - expr.id(ID_or); - propagate_not(expr); - } - else if(expr.id()==ID_nand) - { - expr.id(ID_and); - propagate_not(expr); - } - else if(expr.id()==ID_implies) - { - if(expr.operands().size()==2) - { - expr.id(ID_or); - propagate_not(expr.op0()); - } - } - - Forall_operands(it, expr) - cnf_propagate_not(*it); -} - -/*******************************************************************\ - -Function: propagate_not - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void propagate_not(exprt &expr) -{ - if(expr.id()==ID_and || expr.id()==ID_or) - { - if(expr.id()==ID_and) - expr.id(ID_or); - else // or - expr.id(ID_and); - - Forall_operands(it, expr) - propagate_not(*it); - } - else if(expr.id()==ID_nor) - expr.id(ID_or); - else if(expr.id()==ID_nand) - expr.id(ID_and); - else if(expr.id()==ID_not) - { - assert(expr.operands().size()==1); - exprt tmp; - tmp.swap(expr.op0()); - expr.swap(tmp); - } - else if(expr.id()==ID_equal) - expr.id(ID_notequal); - else if(expr.id()==ID_notequal) - expr.id(ID_equal); - else - { - exprt tmp; - expr.swap(tmp); - expr.id(ID_not); - expr.type()=tmp.type(); - expr.move_to_operands(tmp); - } -} diff --git a/src/util/old/cnf_simplify.h b/src/util/old/cnf_simplify.h deleted file mode 100644 index 01f4ec3473b..00000000000 --- a/src/util/old/cnf_simplify.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef CPROVER_UTIL_OLD_CNF_SIMPLIFY_H -#define CPROVER_UTIL_OLD_CNF_SIMPLIFY_H - -class exprt; - -void cnf_simplify(exprt &expr); - -#endif // CPROVER_UTIL_OLD_CNF_SIMPLIFY_H diff --git a/src/util/old/collection.h b/src/util/old/collection.h deleted file mode 100644 index 83f7a9e41dd..00000000000 --- a/src/util/old/collection.h +++ /dev/null @@ -1,191 +0,0 @@ -/*******************************************************************\ - -Module: String Storage - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_OLD_COLLECTION_H -#define CPROVER_UTIL_OLD_COLLECTION_H - -#include "string_hash.h" -#include "hash_cont.h" - -template -class collection -{ -public: - typedef T valuet; - - typedef hash_map_cont member_mapt; - typedef std::vector member_vectort; - - typedef typename member_mapt::const_iterator const_iterator; - - const_iterator begin() const - { - return member_map.begin(); - } - - const_iterator end() const - { - return member_map.end(); - } - - class membert - { - public: - membert() - { - } - - friend bool operator < (const membert &a, const membert &b) - { - return a.nr result= - member_map.insert(std::pair(x, member_vector.size())); - - if(result.second) - member_vector.push_back(x); - - return membert(result.first->second); - } - - const T &operator [] (const membert m) const - { - return member_vector[m.nr]; - } - - const membert operator [] (const T &x) - { - return member(x); - } - - void clear() - { - member_map.clear(); - member_vector.clear(); - } - -protected: - member_mapt member_map; - member_vectort member_vector; -}; - -template -class collection_set -{ -public: - typedef T collectiont; - - collection_set():collection(NULL) - { - } - - void insert(unsigned nr) - { - if(members.size() memberst; - memberst members; - - void set_collection(collectiont &_collection) - { - if(collection==NULL) - collection=&_collection; - else - assert(collection==&_collection); - } - - collectiont *collection; -}; - -typedef collection_set > string_collection_set; - -#endif // CPROVER_UTIL_OLD_COLLECTION_H diff --git a/src/util/old/oexpr.cpp b/src/util/old/oexpr.cpp deleted file mode 100644 index e5c76870f38..00000000000 --- a/src/util/old/oexpr.cpp +++ /dev/null @@ -1,21 +0,0 @@ -/*******************************************************************\ - -Module: Expression Representation - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "oexpr.h" - -/*******************************************************************\ - -Function: - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ diff --git a/src/util/old/oexpr.h b/src/util/old/oexpr.h deleted file mode 100644 index b8d89b184f9..00000000000 --- a/src/util/old/oexpr.h +++ /dev/null @@ -1,163 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_OLD_OEXPR_H -#define CPROVER_UTIL_OLD_OEXPR_H - -#include "expr.h" -#include "std_types.h" - -class oexprt:public exprt -{ -public: - explicit inline oexprt(const exprt &src):exprt(src) - { - } - - inline oexprt(const irep_idt &_id, const typet &_type):exprt(_id, _type) - { - } - - inline oexprt( - const exprt &a, const irep_idt &_id, const exprt &b, - const typet &_type):exprt(_id, _type) - { - copy_to_operands(a, b); - } - - inline oexprt( - const irep_idt &_id, const exprt &a, - const typet &_type):exprt(_id, _type) - { - copy_to_operands(a); - } - - inline oexprt operator[](const exprt &_index) const - { - return oexprt(*this, ID_index, _index, type().subtype()); - } -}; - -inline oexprt operator+(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_plus, b, a.type()); -} - -inline oexprt operator-(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_minus, b, a.type()); -} - -inline oexprt operator-(const exprt &a) -{ - return oexprt(ID_unary_minus, a, a.type()); -} - -inline exprt operator*(const exprt &a, const oexprt &b) -{ - return oexprt(a, ID_mult, b, a.type()); -} - -inline exprt operator*(const exprt &a) -{ - return oexprt(ID_dereference, a, a.type().subtype()); -} - -inline oexprt operator/(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_div, b, a.type()); -} - -inline oexprt operator%(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_mod, b, a.type()); -} - -inline oexprt operator&&(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_and, b, bool_typet()); -} - -inline oexprt operator||(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_or, b, bool_typet()); -} - -inline oexprt operator&(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_bitand, b, a.type()); -} - -inline oexprt operator|(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_bitor, b, a.type()); -} - -inline oexprt operator~(const exprt &a) -{ - return oexprt(ID_bitnot, a, a.type()); -} - -inline oexprt operator>>(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_shr, b, a.type()); -} - -inline oexprt operator<<(const exprt &a, const exprt &b) -{ - return oexprt(a, ID_shl, b, a.type()); -} - -inline oexprt operator==(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_equal, b, bool_typet()); -} - -inline oexprt operator!=(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_notequal, b, bool_typet()); -} - -inline oexprt operator!(const oexprt &a) -{ - return oexprt(ID_not, a, bool_typet()); -} - -inline oexprt operator<(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_lt, b, bool_typet()); -} - -inline oexprt operator>(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_gt, b, bool_typet()); -} - -inline oexprt operator<=(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_le, b, bool_typet()); -} - -inline oexprt operator>=(const oexprt &a, const oexprt &b) -{ - return oexprt(a, ID_ge, b, bool_typet()); -} - -static inline oexprt ite(const oexprt &cond, const oexprt &a, const oexprt &b) -{ - oexprt result(ID_if, a.type()); - result.copy_to_operands(cond, a, b); - return result; -} - -static inline oexprt typecast(const oexprt &a, const typet &t) -{ - return oexprt(ID_typecast, a, t); -} - -#endif // CPROVER_UTIL_OLD_OEXPR_H diff --git a/src/util/old/set_stack.h b/src/util/old/set_stack.h deleted file mode 100644 index 6dcd155c4d3..00000000000 --- a/src/util/old/set_stack.h +++ /dev/null @@ -1,149 +0,0 @@ -#ifndef CPROVER_UTIL_OLD_SET_STACK_H -#define CPROVER_UTIL_OLD_SET_STACK_H - -#include -#include - -template -class set_stack -{ - protected: - typedef std::multiset sett; - typedef typename sett::iterator set_iterator; - typedef typename sett::const_iterator set_const_iterator; - typedef typename std::list listt; - typedef typename listt::size_type list_size_type; - - public: - typedef typename sett::const_iterator const_iterator; - - const T &front() const - { return *l.front(); } - - const T &back() const - { return *l.back(); } - - T &front() - { return *l.front(); } - - T &back() - { return *l.back(); } - - const_iterator begin() const - { return s.begin(); } - - const_iterator end() const - { return s.end(); } - - set_const_iterator find(const T &e) const - { return s.find(e); } - - void push_back(const T &e) - { l.push_back(s.insert(e)); } - - void pop_back() - { - s.erase(l.back()); - l.pop_back(); - } - - list_size_type size() const - { return l.size(); } - - const T &back() const - { return *l.back(); } - - void resize(list_size_type s); - - bool empty() const - { return l.empty(); } - - protected: - sett s; - listt l; -}; - -template -void set_stack::resize(list_size_type s) -{ - if(l.size()>s) - { - for(unsigned i=l.size()-s; i!=0; i--) - pop_back(); - } - else if(l.size() -class hash_set_stack -{ - protected: - typedef typename hash_multiset_cont sett; - typedef typename sett::iterator set_iterator; - typedef typename sett::const_iterator set_const_iterator; - typedef typename std::list listt; - typedef typename listt::size_type list_size_type; - - public: - typedef set_const_iterator const_iterator; - - const_iterator begin() const - { return s.begin(); } - - const_iterator end() const - { return s.end(); } - - set_const_iterator find(const T &e) const - { return s.find(e); } - - void push_back(const T &e) - { l.push_back(s.insert(e)); } - - void pop_back() - { - s.erase(l.back()); - l.pop_back(); - } - - list_size_type size() const - { return l.size(); } - - const T &back() const - { return *l.back(); } - - void resize(list_size_type s); - - bool empty() const - { return l.empty(); } - - protected: - sett s; - listt l; -}; - -template -void hash_set_stack::resize(list_size_type s) -{ - if(l.size()>s) - { - for(unsigned i=l.size()-s; i!=0; i--) - pop_back(); - } - else if(l.size() names; - - for(symbolst::const_iterator - it=symbols.begin(); - it!=symbols.end(); - it++) - { - const symbolt *symbol; - if(ns.lookup(*it, symbol)) - pretty_map[*it]=*it; - else - { - names.insert(symbol->base_name); - pretty_map[*it]=symbol->base_name; - } - } - - std::map name_components; - - // find collisions - - while(1) - { - std::set collisions; - - for(symbolst::const_iterator it=symbols.begin(); - it!=symbols.end(); it++) - if(names.count(pretty_map[*it])>=2) - collisions.insert(*it); - - if(collisions.empty()) - return; // done - - names.clear(); - - for(std::set::const_iterator it=collisions.begin(); - it!=collisions.end(); it++) - { - unsigned no_components=(++name_components[*it]); - - identifiert id(id2string(*it)); - - if(no_components>=id.components.size()) - pretty_map[*it]=*it; - else - { - while(no_componentssecond; -} -#endif diff --git a/src/util/pretty_names.h b/src/util/pretty_names.h deleted file mode 100644 index f1776c16c1e..00000000000 --- a/src/util/pretty_names.h +++ /dev/null @@ -1,37 +0,0 @@ -/*******************************************************************\ - -Module: Pretty name generation - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_PRETTY_NAMES_H -#define CPROVER_UTIL_PRETTY_NAMES_H - -// THIS FILE WILL GO AWAY - -#include -#include - -#include "irep.h" - -class namespacet; - -#if 0 -class pretty_namest -{ - public: - typedef std::set symbolst; - typedef std::map pretty_mapt; - - pretty_mapt pretty_map; - - void get_pretty_names(const symbolst &symbols, - const namespacet &ns); - - const irep_idt &pretty_name(const irep_idt &identifier) const; -}; -#endif - -#endif // CPROVER_UTIL_PRETTY_NAMES_H diff --git a/src/util/rational_tools.cpp b/src/util/rational_tools.cpp index 08f303c31f9..22b5263a485 100644 --- a/src/util/rational_tools.cpp +++ b/src/util/rational_tools.cpp @@ -6,8 +6,9 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -#include "std_expr.h" +#include "rational.h" #include "std_types.h" + #include "rational_tools.h" /*******************************************************************\ diff --git a/src/util/rational_tools.h b/src/util/rational_tools.h index fecadc17f1a..34dcf8d4932 100644 --- a/src/util/rational_tools.h +++ b/src/util/rational_tools.h @@ -9,7 +9,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_RATIONAL_TOOLS_H #define CPROVER_UTIL_RATIONAL_TOOLS_H -#include "rational.h" +#include "std_expr.h" + +class rationalt; bool to_rational(const exprt &expr, rationalt &rational_value); constant_exprt from_rational(const rationalt &rational_value); diff --git a/src/util/ref_expr_set.h b/src/util/ref_expr_set.h index a607d15baeb..197351399ce 100644 --- a/src/util/ref_expr_set.h +++ b/src/util/ref_expr_set.h @@ -9,18 +9,17 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_REF_EXPR_SET_H #define CPROVER_UTIL_REF_EXPR_SET_H -#include +#include -#include "hash_cont.h" #include "expr.h" #include "reference_counting.h" -extern const hash_set_cont empty_expr_set; +extern const std::unordered_set empty_expr_set; struct ref_expr_set_dt { ref_expr_set_dt() {} - typedef hash_set_cont expr_sett; + typedef std::unordered_set expr_sett; expr_sett expr_set; const static ref_expr_set_dt blank; diff --git a/src/util/rename.cpp b/src/util/rename.cpp index 3b66de68257..b121edb6acb 100644 --- a/src/util/rename.cpp +++ b/src/util/rename.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "rename.h" -#include "i2string.h" #include "symbol.h" #include "expr.h" #include "namespace.h" @@ -51,7 +50,7 @@ void get_new_name(irep_idt &new_name, const namespacet &ns) std::string prefix=id2string(new_name)+"_"; - new_name=prefix+i2string(ns.get_max(prefix)+1); + new_name=prefix+std::to_string(ns.get_max(prefix)+1); } /*******************************************************************\ diff --git a/src/util/rename_symbol.h b/src/util/rename_symbol.h index 0beb85516f8..1e75c92e169 100644 --- a/src/util/rename_symbol.h +++ b/src/util/rename_symbol.h @@ -14,14 +14,18 @@ Author: Daniel Kroening, kroening@kroening.com // false: renamed something // -#include "hash_cont.h" -#include "expr.h" +#include + +#include "irep.h" + +class exprt; +class typet; class rename_symbolt { public: - typedef hash_map_cont expr_mapt; - typedef hash_map_cont type_mapt; + typedef std::unordered_map expr_mapt; + typedef std::unordered_map type_mapt; inline void insert_expr(const irep_idt &old_id, const irep_idt &new_id) diff --git a/src/util/replace_expr.h b/src/util/replace_expr.h index 9a804b1d785..74b2a64374c 100644 --- a/src/util/replace_expr.h +++ b/src/util/replace_expr.h @@ -14,10 +14,9 @@ Author: Daniel Kroening, kroening@kroening.com // false: replaced something // -#include "hash_cont.h" #include "expr.h" -typedef hash_map_cont replace_mapt; +typedef std::unordered_map replace_mapt; bool replace_expr(const exprt &what, const exprt &by, exprt &dest); bool replace_expr(const replace_mapt &what, exprt &dest); diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index b27cd1f0378..8fad66c80ba 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -14,14 +14,13 @@ Author: Daniel Kroening, kroening@kroening.com // false: replaced something // -#include "hash_cont.h" #include "expr.h" class replace_symbolt { public: - typedef hash_map_cont expr_mapt; - typedef hash_map_cont type_mapt; + typedef std::unordered_map expr_mapt; + typedef std::unordered_map type_mapt; inline void insert(const irep_idt &identifier, const exprt &expr) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 865a3e982e0..2894544b8db 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "rational.h" #include "simplify_expr_class.h" #include "simplify_expr.h" #include "mp_arith.h" @@ -47,10 +48,10 @@ struct simplify_expr_cachet friend class simplify_exprt; #if 1 - typedef hash_map_cont< + typedef std::unordered_map< exprt, exprt, irep_full_hash, irep_full_eq> containert; #else - typedef hash_map_cont< + typedef std::unordered_map< exprt, exprt, irep_hash> containert; #endif diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index aa98a85b13b..89df15cf7be 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include +#include #include "simplify_expr_class.h" #include "expr.h" @@ -146,7 +147,7 @@ bool simplify_exprt::simplify_boolean(exprt &expr) { // first gather all the a's with !a - hash_set_cont expr_set; + std::unordered_set expr_set; forall_operands(it, expr) if(it->id()==ID_not && diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index eeaa7e2bcfe..cfaea165f36 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#include #include #include "type.h" diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 98dab123a3f..acc1c0453a7 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "base_type.h" +#include "rational.h" #include "simplify_expr_class.h" #include "expr.h" #include "namespace.h" -#include "namespace_utils.h" #include "config.h" #include "bv_arithmetic.h" #include "std_expr.h" @@ -478,7 +479,7 @@ bool simplify_exprt::simplify_plus(exprt &expr) // search for a and -a // first gather all the a's with -a - typedef hash_map_cont + typedef std::unordered_map expr_mapt; expr_mapt expr_map; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 25e18ceb09d..5efc4d6e70c 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "config.h" #include "namespace.h" #include "pointer_offset_size.h" -#include "i2string.h" #include "std_types.h" #include "std_expr.h" @@ -200,7 +199,7 @@ Function: constant_exprt::integer_constant constant_exprt constant_exprt::integer_constant(unsigned v) { - return constant_exprt(i2string(v), integer_typet()); + return constant_exprt(std::to_string(v), integer_typet()); } /*******************************************************************\ diff --git a/src/util/string2int.cpp b/src/util/string2int.cpp index c5112c41d9b..7e746610118 100644 --- a/src/util/string2int.cpp +++ b/src/util/string2int.cpp @@ -15,7 +15,7 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk /*******************************************************************\ -Function: safe_c_str2number +Function: str2number Inputs: @@ -62,57 +62,6 @@ inline T str2number(const char *str, int base, bool safe) /*******************************************************************\ -Function: safe_c_str2int - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int safe_c_str2int(const char *str, int base) -{ - return str2number(str, base, true); -} - -/*******************************************************************\ - -Function: safe_c_str2unsigned - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -unsigned safe_c_str2unsigned(const char *str, int base) -{ - return str2number(str, base, true); -} - -/*******************************************************************\ - -Function: safe_string2int - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int safe_string2int(const std::string &str, int base) -{ - return str2number(str.c_str(), base, true); -} - -/*******************************************************************\ - Function: safe_string2unsigned Inputs: @@ -147,40 +96,6 @@ std::size_t safe_string2size_t(const std::string &str, int base) /*******************************************************************\ -Function: unsafe_c_str2int - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -int unsafe_c_str2int(const char *str, int base) -{ - return str2number(str, base, false); -} - -/*******************************************************************\ - -Function: unsafe_c_str2unsigned - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -unsigned unsafe_c_str2unsigned(const char *str, int base) -{ - return str2number(str, base, false); -} - -/*******************************************************************\ - Function: unsafe_string2int Inputs: diff --git a/src/util/string2int.h b/src/util/string2int.h index f77aed0274e..1a660eba864 100644 --- a/src/util/string2int.h +++ b/src/util/string2int.h @@ -13,21 +13,13 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk // These check that the string is indeed a valid number, // and fail an assertion otherwise. -int safe_c_str2int(const char *str, int base=10); -unsigned safe_c_str2unsigned(const char *str, int base=10); - -int safe_string2int(const std::string &str, int base=10); +// We use those for data types that C++11's std::stoi etc. do not +// cover. unsigned safe_string2unsigned(const std::string &str, int base=10); std::size_t safe_string2size_t(const std::string &str, int base=10); -// The safe_* functions will eventually go away, and will be replaced -// by C++11 std::stoi, std::stol, std::stoll, std::stoul and so on. - // The below mimick C's atoi/atol: any errors are silently ignored. // They are meant to replace atoi/atol. -int unsafe_c_str2int(const char *str, int base=10); -unsigned unsafe_c_str2unsigned(const char *str, int base=10); - int unsafe_string2int(const std::string &str, int base=10); unsigned unsafe_string2unsigned(const std::string &str, int base=10); std::size_t unsafe_string2size_t(const std::string &str, int base=10); diff --git a/src/util/string_container.h b/src/util/string_container.h index e4dda7d393d..c2ce0b22939 100644 --- a/src/util/string_container.h +++ b/src/util/string_container.h @@ -10,9 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_STRING_CONTAINER_H #include +#include #include -#include "hash_cont.h" #include "string_hash.h" struct string_ptrt @@ -73,7 +73,7 @@ class string_containert protected: // the 'unsigned' ought to be size_t - typedef hash_map_cont hash_tablet; + typedef std::unordered_map hash_tablet; hash_tablet hash_table; unsigned get(const char *s); diff --git a/src/util/symbol.h b/src/util/symbol.h index f10084184f4..3f821421719 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -113,24 +113,6 @@ class symbolt std::ostream &operator<<(std::ostream &out, const symbolt &symbol); -#include - -typedef std::list symbol_listt; - -#define forall_symbol_list(it, expr) \ - for(symbol_listt::const_iterator it=(expr).begin(); \ - it!=(expr).end(); ++it) - -typedef std::list symbolptr_listt; - -#define forall_symbolptr_list(it, list) \ - for(symbolptr_listt::const_iterator it=(list).begin(); \ - it!=(list).end(); ++it) - -#define Forall_symbolptr_list(it, list) \ - for(symbolptr_listt::iterator it=(list).begin(); \ - it!=(list).end(); ++it) - /*! \brief Symbol table entry describing a data type \ingroup gr_symbol_table diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index b9905f215b8..b0fc5b7840b 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -20,8 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include -#include "hash_cont.h" #include "symbol.h" #define forall_symbols(it, expr) \ @@ -51,7 +51,7 @@ typedef std::multimap symbol_module_mapt; class symbol_tablet { public: - typedef hash_map_cont symbolst; + typedef std::unordered_map symbolst; symbolst symbols; symbol_base_mapt symbol_base_map; diff --git a/src/util/tempfile.cpp b/src/util/tempfile.cpp index 3a6dd24e7cd..143b702abf6 100644 --- a/src/util/tempfile.cpp +++ b/src/util/tempfile.cpp @@ -32,7 +32,6 @@ Author: Daniel Kroening #include #endif -#include "i2string.h" #include "tempfile.h" /*******************************************************************\ @@ -122,7 +121,7 @@ std::string get_temporary_file( // the path returned by GetTempPath ends with a backslash std::string t_template= std::string(lpTempPathBuffer)+prefix+ - i2string(getpid())+".XXXXXX"+suffix; + std::to_string(getpid())+".XXXXXX"+suffix; #else std::string dir="/tmp/"; const char *TMPDIR_env=getenv("TMPDIR"); @@ -131,7 +130,7 @@ std::string get_temporary_file( if(*dir.rbegin()!='/') dir+='/'; std::string t_template= - dir+prefix+i2string(getpid())+".XXXXXX"+suffix; + dir+prefix+std::to_string(getpid())+".XXXXXX"+suffix; #endif char *t_ptr=strdup(t_template.c_str()); diff --git a/src/util/type.h b/src/util/type.h index 6e007d261ff..1fa20503f80 100644 --- a/src/util/type.h +++ b/src/util/type.h @@ -9,8 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_TYPE_H #define CPROVER_UTIL_TYPE_H -#include - #include #define SUBTYPE_IN_GETSUB @@ -148,16 +146,6 @@ class type_with_subtypest:public typet #endif }; -typedef std::list type_listt; - -#define forall_type_list(it, type) \ - for(type_listt::const_iterator it=(type).begin(); \ - it!=(type).end(); ++it) - -#define Forall_type_list(it, type) \ - for(type_listt::iterator it=(type).begin(); \ - it!=(type).end(); ++it) - #define forall_subtypes(it, type) \ if((type).has_subtypes()) \ for(typet::subtypest::const_iterator it=(type).subtypes().begin(), \ diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index afa79a8d75c..4296c14666f 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "i2string.h" #include "xml.h" #include "json.h" #include "xml_expr.h" @@ -212,7 +211,7 @@ void ui_message_handlert::print( const char *type=level_string(level); std::string sequence_number_str= - sequence_number>=0?i2string(sequence_number):""; + sequence_number>=0?std::to_string(sequence_number):""; ui_msg(type, tmp_message, sequence_number_str, location); } diff --git a/src/util/xml.cpp b/src/util/xml.cpp index fd8a870ec8d..957424302f3 100644 --- a/src/util/xml.cpp +++ b/src/util/xml.cpp @@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "string2int.h" -#include "i2string.h" #include "xml.h" /*******************************************************************\ @@ -148,7 +147,7 @@ void xmlt::escape(const std::string &s, std::ostream &out) default: // � isn't allowed, but what shall we do? if((ch>=0 && ch<' ') || ch==127) - out << "&#"+i2string((unsigned char)ch)+";"; + out << "&#"+std::to_string((unsigned char)ch)+";"; else out << ch; } @@ -194,7 +193,7 @@ void xmlt::escape_attribute(const std::string &s, std::ostream &out) default: // � isn't allowed, but what shall we do? if((ch>=0 && ch<' ') || ch==127) - out << "&#"+i2string((unsigned char)ch)+";"; + out << "&#"+std::to_string((unsigned char)ch)+";"; else out << ch; } @@ -281,7 +280,7 @@ void xmlt::set_attribute( const std::string &attribute, unsigned value) { - set_attribute(attribute, i2string(value)); + set_attribute(attribute, std::to_string(value)); } /*******************************************************************\ @@ -300,7 +299,7 @@ void xmlt::set_attribute( const std::string &attribute, unsigned long value) { - set_attribute(attribute, i2string(value)); + set_attribute(attribute, std::to_string(value)); } /*******************************************************************\ @@ -319,7 +318,7 @@ void xmlt::set_attribute( const std::string &attribute, unsigned long long value) { - set_attribute(attribute, i2string(value)); + set_attribute(attribute, std::to_string(value)); } /*******************************************************************\ diff --git a/src/xmllang/graphml.cpp b/src/xmllang/graphml.cpp index 1a8530f7ae0..c1ab6760f4f 100644 --- a/src/xmllang/graphml.cpp +++ b/src/xmllang/graphml.cpp @@ -11,7 +11,6 @@ Author: Michael Tautschnig, mt@eecs.qmul.ac.uk #include #include -#include #include "graphml.h" @@ -586,7 +585,7 @@ bool write_graphml(const graphmlt &src, std::ostream &os) { xmlt &entry=node.new_element("data"); entry.set_attribute("key", "threadNumber"); - entry.data=i2string(n.thread_nr); + entry.data=std::to_string(n.thread_nr); } //