diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index a6c1bf227fbe..0ea8126e6a46 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -203,12 +203,7 @@ class shift_exprt; class rw_range_sett { public: - #ifdef USE_DSTRING typedef std::map> objectst; - #else - typedef std::unordered_map< - irep_idt, std::unique_ptr, string_hash> objectst; - #endif virtual ~rw_range_sett(); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index fb8e0a78374a..faa8c46224ad 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -274,11 +274,7 @@ class rd_range_domaint:public ai_domain_baset sparse_bitvector_analysist *const bv_container; typedef std::set values_innert; - #ifdef USE_DSTRING typedef std::map valuest; - #else - typedef std::unordered_map valuest; - #endif /// It is an ordered map from program variable names to `ID`s of /// `reaching_definitiont` instances stored in map pointed to by /// `bv_container`. The map is not empty only if `has_value` is `UNKNOWN`. @@ -286,11 +282,7 @@ class rd_range_domaint:public ai_domain_baset /// instruction. valuest values; - #ifdef USE_DSTRING typedef std::map export_cachet; - #else - typedef std::unordered_map export_cachet; - #endif /// It is a helper data structure. It consists of data already stored in /// `values` and `bv_container`. It is basically (an ordered) map from (a /// subset of) variables in `values` to iterators to GOTO instructions where diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index d15753b8fa17..60495c653743 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -20,9 +20,6 @@ Author: Daniel Kroening #include #include #include -#ifndef USE_DSTRING -# include -#endif #include #include @@ -78,12 +75,7 @@ std::string graphml_witnesst::convert_assign_rec( const irep_idt &identifier, const code_assignt &assign) { -#ifdef USE_DSTRING const auto cit = cache.find({identifier.get_no(), &assign.read()}); -#else - const auto cit = - cache.find({get_string_container()[id2string(identifier)], &assign.read()}); -#endif if(cit != cache.end()) return cit->second; @@ -219,12 +211,7 @@ std::string graphml_witnesst::convert_assign_rec( result = lhs + " = " + expr_to_string(ns, identifier, clean_rhs) + ";"; } -#ifdef USE_DSTRING cache.insert({{identifier.get_no(), &assign.read()}, result}); -#else - cache.insert( - {{get_string_container()[id2string(identifier)], &assign.read()}, result}); -#endif return result; } diff --git a/src/libcprover-cpp/verification_result.h b/src/libcprover-cpp/verification_result.h index 778299315168..6176ef8486d6 100644 --- a/src/libcprover-cpp/verification_result.h +++ b/src/libcprover-cpp/verification_result.h @@ -12,16 +12,8 @@ #include #include -#ifndef USE_STD_STRING -# define USE_DSTRING -#endif - -#ifdef USE_DSTRING class dstringt; typedef dstringt irep_idt; -#else -typedef std::string irep_idt; -#endif struct property_infot; using propertiest = std::map; diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 8b3ad907ddec..d07e01ead438 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -191,19 +191,11 @@ class value_set_fit typedef std::unordered_set dynamic_object_id_sett; - #ifdef USE_DSTRING typedef std::map valuest; typedef std::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 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 std::vector get_value_set(const exprt &expr, const namespacet &ns) const; diff --git a/src/util/README.md b/src/util/README.md index 1c01fa7d7256..4da105111498 100644 --- a/src/util/README.md +++ b/src/util/README.md @@ -72,9 +72,9 @@ standard data structures as in irept. \subsection irep_idt_section Strings: dstringt, the string_container and the ID_* -Within cbmc, strings are represented using \ref irep_idt. By default this is -typedefed to \ref dstringt. For debugging purposes you can set `USE_STD_STRING` -to change this typedef to `std::string`. You can also easily convert an +Within cbmc, strings are represented using \ref irep_idt, which is +typedefed to \ref dstringt. +You can also easily convert an [irep_idt](\ref irep_idt) to a `std::string` using the [id2string](\ref id2string) function, or to a `char*` using the [c_str()](\ref dstringt::c_str) member function. diff --git a/src/util/dstring.h b/src/util/dstring.h index 973711699e92..38926cb754ea 100644 --- a/src/util/dstring.h +++ b/src/util/dstring.h @@ -29,8 +29,7 @@ struct diagnostics_helpert; /// copies of the same string you only have to store the whole string once, /// which saves space. /// -/// `irep_idt` is typedef-ed to \ref dstringt in irep.h unless `USE_STD_STRING` -/// is set. +/// `irep_idt` is typedef-ed to \ref dstringt in irep.h. /// /// /// Note: Marked final to disable inheritance. No virtual destructor, so diff --git a/src/util/irep.cpp b/src/util/irep.cpp index 650e8bc768fb..36e103ea8ff6 100644 --- a/src/util/irep.cpp +++ b/src/util/irep.cpp @@ -76,20 +76,12 @@ long long irept::get_long_long(const irep_idt &name) const void irept::set(const irep_idt &name, const long long value) { -#ifdef USE_DSTRING add(name).id(to_dstring(value)); -#else - add(name).id(std::to_string(value)); -#endif } void irept::set_size_t(const irep_idt &name, const std::size_t value) { -#ifdef USE_DSTRING add(name).id(to_dstring(value)); -#else - add(name).id(std::to_string(value)); -#endif } void irept::remove(const irep_idt &name) diff --git a/src/util/irep.h b/src/util/irep.h index eb91b9f73ef5..97fea5e9c4a0 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -33,24 +33,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#ifdef USE_DSTRING typedef dstringt irep_idt; // NOLINTNEXTLINE(readability/identifiers) typedef dstring_hash irep_id_hash; -#else -#include "string_hash.h" -typedef std::string irep_idt; -// NOLINTNEXTLINE(readability/identifiers) -typedef string_hash irep_id_hash; -#endif inline const std::string &id2string(const irep_idt &d) { - #ifdef USE_DSTRING return as_string(d); - #else - return d; - #endif } #ifdef IREP_DEBUG @@ -76,9 +65,8 @@ struct ref_count_ift /// A node with data in a tree, it contains: /// -/// * \ref irept::dt::data : A string (Unless `USE_STD_STRING` is set, this is -/// actually a \ref dstringt and thus an integer which is a reference into a -/// string table.) +/// * \ref irept::dt::data : A \ref dstringt and thus an integer which is a +/// reference into a string table.) /// /// * \ref irept::dt::named_sub : A map from `irep_idt` (a string) to \ref /// irept. This is used for named children, i.e. subexpressions, parameters, diff --git a/src/util/irep_ids.cpp b/src/util/irep_ids.cpp index bb933862ed76..26fcd44d7df4 100644 --- a/src/util/irep_ids.cpp +++ b/src/util/irep_ids.cpp @@ -25,8 +25,6 @@ const char *irep_ids_table[]= nullptr, }; -#ifdef USE_DSTRING - enum class idt:unsigned { #define IREP_ID_ONE(the_id) id_##the_id, @@ -42,13 +40,6 @@ enum class idt:unsigned const dstringt ID_##the_id=dstringt::make_from_table_index( \ static_cast(idt::id_##the_id)); -#else - -#define IREP_ID_ONE(the_id) const std::string ID_##the_id(#the_id); -# define IREP_ID_TWO(the_id, str) const std::string ID_##the_id(# str); - -#endif - #include "irep_ids.def" // NOLINT(build/include) string_containert::string_containert() diff --git a/src/util/irep_ids.h b/src/util/irep_ids.h index b96ff929f25d..b8ee3957006c 100644 --- a/src/util/irep_ids.h +++ b/src/util/irep_ids.h @@ -12,15 +12,7 @@ Author: Reuben Thomas, reuben.thomas@me.com #ifndef CPROVER_UTIL_IREP_IDS_H #define CPROVER_UTIL_IREP_IDS_H -#ifndef USE_STD_STRING -#define USE_DSTRING -#endif - -#ifdef USE_DSTRING #include "dstring.h" -#else -#include -#endif /// \file /// The irep_ids are generated using a technique called @@ -34,18 +26,9 @@ Author: Reuben Thomas, reuben.thomas@me.com /// into a const extern irep_idt with the variable name `ID_param` and the /// string value `"contents"`. -#ifdef USE_DSTRING - #define IREP_ID_ONE(the_id) extern const dstringt ID_##the_id; #define IREP_ID_TWO(the_id, str) extern const dstringt ID_##the_id; -#else - -#define IREP_ID_ONE(the_id) extern const std::string ID_##the_id; -#define IREP_ID_TWO(the_id, str) extern const std::string ID_##the_id; - -#endif - #include "irep_ids.def" #endif diff --git a/src/util/irep_serialization.cpp b/src/util/irep_serialization.cpp index e959e8d99f1d..20f37d8a194d 100644 --- a/src/util/irep_serialization.cpp +++ b/src/util/irep_serialization.cpp @@ -212,11 +212,7 @@ void irep_serializationt::write_string_ref( std::ostream &out, const irep_idt &s) { -#ifdef USE_DSTRING size_t id = s.get_no(); -#else - size_t id = get_string_container()[s]; -#endif if(id>=ireps_container.string_map.size()) ireps_container.string_map.resize(id+1, false); diff --git a/src/util/json.h b/src/util/json.h index dbb0b706f683..2ef36d85f07a 100644 --- a/src/util/json.h +++ b/src/util/json.h @@ -274,12 +274,10 @@ class json_stringt:public jsont { } -#ifdef USE_DSTRING explicit json_stringt(const irep_idt &_value) : jsont(kindt::J_STRING, id2string(_value)) { } -#endif /// Constructon from string literal. explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value) diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp index da50c0b85ad6..66f92ffd63c8 100644 --- a/unit/util/irep.cpp +++ b/unit/util/irep.cpp @@ -22,13 +22,8 @@ SCENARIO("irept_memory", "[core][utils][irept]") const std::size_t ref_count_size = 0; #endif -#ifdef USE_DSTRING const std::size_t data_size = sizeof(dstringt); REQUIRE(sizeof(dstringt) == sizeof(unsigned)); -#else - const std::size_t data_size = sizeof(std::string); - REQUIRE(sizeof(std::string) == sizeof(void *)); -#endif const std::size_t sub_size = sizeof(std::vector); #ifndef _GLIBCXX_DEBUG