diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index aeabc8f7650..f43be1dca9e 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -396,7 +396,7 @@ int janalyzer_parse_optionst::doit() lazy_goto_model.initialize(cmdline.args, options); class_hierarchy = - util_make_unique(lazy_goto_model.symbol_table); + std::make_unique(lazy_goto_model.symbol_table); log.status() << "Generating GOTO Program" << messaget::eom; lazy_goto_model.load_all_functions(); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index dd19585c248..2b7cefc2abd 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1517,7 +1517,7 @@ void java_bytecode_languaget::show_parse(std::ostream &out) std::unique_ptr new_java_bytecode_language() { - return util_make_unique(); + return std::make_unique(); } bool java_bytecode_languaget::from_expr( diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 22189337dc1..a63a0572f1a 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H #include -#include #include #include // IWYU pragma: keep @@ -319,7 +318,9 @@ class java_bytecode_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "java"; } std::string description() const override { return "Java Bytecode"; } diff --git a/jbmc/src/java_bytecode/java_qualifiers.cpp b/jbmc/src/java_bytecode/java_qualifiers.cpp index 37b4b894b08..c462e5471f8 100644 --- a/jbmc/src/java_bytecode/java_qualifiers.cpp +++ b/jbmc/src/java_bytecode/java_qualifiers.cpp @@ -8,8 +8,6 @@ #include #include -#include - #include "expr2java.h" java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other) @@ -24,7 +22,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other) std::unique_ptr java_qualifierst::clone() const { - auto other = util_make_unique(ns); + auto other = std::make_unique(ns); *other = *this; return std::move(other); } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index ef776c63f3c..82d940222d1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -535,7 +534,7 @@ int jbmc_parse_optionst::doit() options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { verifier = - util_make_unique>( + std::make_unique>( options, ui_message_handler, *goto_model_ptr); } else if( @@ -545,13 +544,13 @@ int jbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>( options, ui_message_handler, *goto_model_ptr); } else { - verifier = util_make_unique< + verifier = std::make_unique< stop_on_fail_verifiert>( options, ui_message_handler, *goto_model_ptr); } @@ -560,7 +559,7 @@ int jbmc_parse_optionst::doit() !options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { - verifier = util_make_unique>( options, ui_message_handler, *goto_model_ptr); } @@ -571,13 +570,13 @@ int jbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>( options, ui_message_handler, *goto_model_ptr); } else { - verifier = util_make_unique>( options, ui_message_handler, *goto_model_ptr); } @@ -603,7 +602,7 @@ int jbmc_parse_optionst::get_goto_program( lazy_goto_model.initialize(cmdline.args, options); class_hierarchy = - util_make_unique(lazy_goto_model.symbol_table); + std::make_unique(lazy_goto_model.symbol_table); // Show the class hierarchy if(cmdline.isset("show-class-hierarchy")) @@ -662,7 +661,7 @@ int jbmc_parse_optionst::get_goto_program( } goto_model_ptr = - util_make_unique(std::move(lazy_goto_model)); + std::make_unique(std::move(lazy_goto_model)); } log.status() << config.object_bits_info() << messaget::eom; diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 090784f4759..a4f0bc34e69 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -50,7 +50,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -565,20 +564,20 @@ class ait : public ai_recursive_interproceduralt // constructor ait() : ai_recursive_interproceduralt( - util_make_unique< + std::make_unique< ai_history_factory_default_constructort>(), - util_make_unique>(), - util_make_unique(), + std::make_unique>(), + std::make_unique(), no_logging) { } explicit ait(std::unique_ptr &&df) : ai_recursive_interproceduralt( - util_make_unique< + std::make_unique< ai_history_factory_default_constructort>(), std::move(df), - util_make_unique(), + std::make_unique(), no_logging) { } diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h index 13195ae052e..85d6dcb1dfb 100644 --- a/src/analyses/ai_domain.h +++ b/src/analyses/ai_domain.h @@ -41,7 +41,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANALYSES_AI_DOMAIN_H #include -#include #include #include "ai_history.h" @@ -206,7 +205,7 @@ class ai_domain_factoryt : public ai_domain_factory_baset std::unique_ptr copy(const statet &s) const override { - return util_make_unique(static_cast(s)); + return std::make_unique(static_cast(s)); } bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) @@ -229,7 +228,7 @@ class ai_domain_factory_default_constructort std::unique_ptr make(locationt l) const override { - auto d = util_make_unique(); + auto d = std::make_unique(); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); } @@ -246,7 +245,7 @@ class ai_domain_factory_location_constructort std::unique_ptr make(locationt l) const override { - auto d = util_make_unique(l); + auto d = std::make_unique(l); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); } diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index a95d0064a72..621dbdfeeb8 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -349,7 +349,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt { auto node_id = dg.add_node(); dg.nodes[node_id].PC = l; - auto p = util_make_unique(node_id); + auto p = std::make_unique(node_id); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); @@ -360,7 +360,7 @@ class dep_graph_domain_factoryt : public ai_domain_factoryt }; dependence_grapht::dependence_grapht(const namespacet &_ns) - : ait(util_make_unique(*this)), + : ait(std::make_unique(*this)), ns(_ns), rd(ns) { diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 0c75177dfda..0f81ecaf632 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -15,7 +15,6 @@ Date: April 2010 #include #include #include -#include #include #include #include @@ -528,7 +527,7 @@ void rw_range_sett::add( .first; if(entry->second==nullptr) - entry->second=util_make_unique(); + entry->second = std::make_unique(); static_cast(*entry->second).push_back( {range_start, range_end}); @@ -766,7 +765,7 @@ void rw_guarded_range_set_value_sett::add( .first; if(entry->second==nullptr) - entry->second=util_make_unique(); + entry->second = std::make_unique(); static_cast(*entry->second).insert( {range_start, {range_end, guard.as_expr()}}); diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp index ff90f398e9b..a7cc24007b1 100644 --- a/src/analyses/invariant_propagation.cpp +++ b/src/analyses/invariant_propagation.cpp @@ -25,7 +25,7 @@ class invariant_set_domain_factoryt std::unique_ptr make(locationt l) const override { - auto p = util_make_unique( + auto p = std::make_unique( ip.value_sets, ip.object_store, ip.ns); CHECK_RETURN(p->is_bottom()); @@ -40,7 +40,7 @@ invariant_propagationt::invariant_propagationt( const namespacet &_ns, value_setst &_value_sets) : ait( - util_make_unique(*this)), + std::make_unique(*this)), ns(_ns), value_sets(_value_sets), object_store(_ns) diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h index eb86ff93329..febc741dbae 100644 --- a/src/analyses/local_may_alias.h +++ b/src/analyses/local_may_alias.h @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "locals.h" #include "dirty.h" @@ -120,7 +119,7 @@ class local_may_alias_factoryt goto_functionst::function_mapt::const_iterator f_it2= goto_functions->function_map.find(fkt); CHECK_RETURN(f_it2 != goto_functions->function_map.end()); - return *(fkt_map[fkt]=util_make_unique(f_it2->second)); + return *(fkt_map[fkt] = std::make_unique(f_it2->second)); } local_may_aliast &operator()(goto_programt::const_targett t) diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 0b2ccf42f68..5dc71d4aab4 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -16,7 +16,6 @@ Date: February 2013 #include "reaching_definitions.h" #include // IWYU pragma: keep -#include #include #include @@ -41,7 +40,7 @@ class rd_range_domain_factoryt : public ai_domain_factoryt std::unique_ptr make(locationt) const override { - auto p = util_make_unique(bv_container); + auto p = std::make_unique(bv_container); CHECK_RETURN(p->is_bottom()); return std::unique_ptr(p.release()); } @@ -53,7 +52,7 @@ class rd_range_domain_factoryt : public ai_domain_factoryt reaching_definitions_analysist::reaching_definitions_analysist( const namespacet &_ns) : concurrency_aware_ait( - util_make_unique(this)), + std::make_unique(this)), ns(_ns) { } @@ -734,13 +733,13 @@ const rd_range_domaint::ranges_at_loct &rd_range_domaint::get( void reaching_definitions_analysist::initialize( const goto_functionst &goto_functions) { - auto value_sets_=util_make_unique(ns); + auto value_sets_ = std::make_unique(ns); (*value_sets_)(goto_functions); value_sets=std::move(value_sets_); - is_threaded=util_make_unique(goto_functions); + is_threaded = std::make_unique(goto_functions); - is_dirty=util_make_unique(goto_functions); + is_dirty = std::make_unique(goto_functions); concurrency_aware_ait::initialize(goto_functions); } diff --git a/src/analyses/variable-sensitivity/abstract_value_object.cpp b/src/analyses/variable-sensitivity/abstract_value_object.cpp index b21130cdebf..aa4c94c21c9 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_value_object.cpp @@ -9,7 +9,6 @@ #include #include #include -#include #include #include @@ -76,12 +75,12 @@ bool single_value_index_ranget::advance_to_next() index_range_implementation_ptrt make_empty_index_range() { - return util_make_unique(); + return std::make_unique(); } index_range_implementation_ptrt make_indeterminate_index_range() { - return util_make_unique(); + return std::make_unique(); } class single_value_value_ranget : public value_range_implementationt @@ -115,7 +114,7 @@ class single_value_value_ranget : public value_range_implementationt value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value) { - return util_make_unique(value); + return std::make_unique(value); } static abstract_object_pointert constants_expression_transform( diff --git a/src/analyses/variable-sensitivity/abstract_value_object.h b/src/analyses/variable-sensitivity/abstract_value_object.h index 924fe76595c..1bd2f1dcff9 100644 --- a/src/analyses/variable-sensitivity/abstract_value_object.h +++ b/src/analyses/variable-sensitivity/abstract_value_object.h @@ -229,7 +229,7 @@ class empty_value_ranget : public value_range_implementationt } value_range_implementation_ptrt reset() const override { - return util_make_unique(); + return std::make_unique(); } private: diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 0c59b7c796c..32d46f06f6f 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -34,7 +34,7 @@ class constant_index_ranget : public single_value_index_ranget static index_range_implementation_ptrt make_constant_index_range(const exprt &val) { - return util_make_unique(val); + return std::make_unique(val); } constant_abstract_valuet::constant_abstract_valuet(const exprt &e) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 3931e12beb9..5f3c6affb4f 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -12,7 +12,6 @@ #include #include #include -#include #include #include "abstract_environment.h" @@ -72,7 +71,7 @@ static index_range_implementation_ptrt make_interval_index_range( const constant_interval_exprt &interval, const namespacet &n) { - return util_make_unique(interval, n); + return std::make_unique(interval, n); } static inline bool diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index cd78b90554f..5357fc3046a 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -10,7 +10,6 @@ /// Value Set Abstract Object #include -#include #include #include @@ -62,7 +61,7 @@ class value_set_index_ranget : public index_range_implementationt static index_range_implementation_ptrt make_value_set_index_range(const std::set &vals) { - return util_make_unique(vals); + return std::make_unique(vals); } static value_range_implementation_ptrt @@ -104,7 +103,7 @@ class value_set_value_ranget : public value_range_implementationt static value_range_implementation_ptrt make_value_set_value_range(const abstract_object_sett &vals) { - return util_make_unique(vals); + return std::make_unique(vals); } static abstract_object_sett diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp index df2bbc557ab..80afe243632 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp @@ -617,7 +617,7 @@ class variable_sensitivity_dependence_domain_factoryt { auto node_id = dg.add_node(); dg.nodes[node_id].PC = l; - auto p = util_make_unique( + auto p = std::make_unique( node_id, object_factory, configuration); CHECK_RETURN(p->is_bottom()); @@ -637,12 +637,12 @@ variable_sensitivity_dependence_grapht::variable_sensitivity_dependence_grapht( const vsd_configt &configuration, message_handlert &message_handler) : ai_three_way_merget( - util_make_unique>(), - util_make_unique( + std::make_unique>(), + std::make_unique( *this, object_factory, configuration), - util_make_unique(), + std::make_unique(), message_handler), goto_functions(goto_functions), ns(_ns) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index f2f54706011..707de155078 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -264,7 +264,7 @@ class variable_sensitivity_domain_factoryt std::unique_ptr make(locationt l) const override { - auto d = util_make_unique( + auto d = std::make_unique( object_factory, configuration); CHECK_RETURN(d->is_bottom()); return std::unique_ptr(d.release()); diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp index cf82835ceb8..4dea6f2642e 100644 --- a/src/ansi-c/ansi_c_language.cpp +++ b/src/ansi-c/ansi_c_language.cpp @@ -150,7 +150,7 @@ void ansi_c_languaget::show_parse(std::ostream &out) std::unique_ptr new_ansi_c_language() { - return util_make_unique(); + return std::make_unique(); } bool ansi_c_languaget::from_expr( diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h index db80e687549..5b7435e786f 100644 --- a/src/ansi-c/ansi_c_language.h +++ b/src/ansi-c/ansi_c_language.h @@ -12,8 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include - #include #include "ansi_c_parse_tree.h" @@ -101,7 +99,9 @@ class ansi_c_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "C"; } std::string description() const override { return "ANSI-C 99"; } diff --git a/src/ansi-c/c_qualifiers.cpp b/src/ansi-c/c_qualifiers.cpp index 78d178bc94c..780ec12be5c 100644 --- a/src/ansi-c/c_qualifiers.cpp +++ b/src/ansi-c/c_qualifiers.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_qualifiers.h" -#include #include c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) @@ -26,7 +25,7 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other) std::unique_ptr c_qualifierst::clone() const { - auto other = util_make_unique(); + auto other = std::make_unique(); *other = *this; return std::move(other); } diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 0d936ef0f03..59915865a0b 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -22,7 +22,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -2022,7 +2021,7 @@ void goto_check_ct::goto_check( bool did_something = false; local_bitvector_analysis = - util_make_unique(goto_function, ns); + std::make_unique(goto_function, ns); goto_programt &goto_program = goto_function.body; diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index e310b2a623e..6f090945d35 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -641,13 +640,13 @@ int cbmc_parse_optionst::doit() { if(options.get_bool_option("stop-on-fail")) { - verifier = util_make_unique< + verifier = std::make_unique< stop_on_fail_verifiert>( options, ui_message_handler, goto_model); } else { - verifier = util_make_unique>( options, ui_message_handler, goto_model); } @@ -656,7 +655,7 @@ int cbmc_parse_optionst::doit() options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { verifier = - util_make_unique>( + std::make_unique>( options, ui_message_handler, goto_model); } else if( @@ -666,13 +665,13 @@ int cbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>(options, ui_message_handler, goto_model); } else { verifier = - util_make_unique>( + std::make_unique>( options, ui_message_handler, goto_model); } } @@ -680,7 +679,7 @@ int cbmc_parse_optionst::doit() !options.get_bool_option("stop-on-fail") && options.get_bool_option("paths")) { - verifier = util_make_unique< + verifier = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); } @@ -691,12 +690,12 @@ int cbmc_parse_optionst::doit() if(options.get_bool_option("localize-faults")) { verifier = - util_make_unique>(options, ui_message_handler, goto_model); } else { - verifier = util_make_unique< + verifier = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); } diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp index 2e2119d83c8..7b8880d824b 100644 --- a/src/cpp/cpp_language.cpp +++ b/src/cpp/cpp_language.cpp @@ -197,7 +197,7 @@ void cpp_languaget::show_parse( std::unique_ptr new_cpp_language() { - return util_make_unique(); + return std::make_unique(); } bool cpp_languaget::from_expr( diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h index a2133f9cf95..12e48ecce19 100644 --- a/src/cpp/cpp_language.h +++ b/src/cpp/cpp_language.h @@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include -#include // unique_ptr - #include #include "cpp_parse_tree.h" @@ -81,7 +79,9 @@ class cpp_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { return "cpp"; } std::string description() const override { return "C++"; } diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index 9d9e44e318a..1b110e78dba 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -45,17 +45,17 @@ std::unique_ptr build_analyzer( std::unique_ptr hf = nullptr; if(options.get_bool_option("ahistorical")) { - hf = util_make_unique< + hf = std::make_unique< ai_history_factory_default_constructort>(); } else if(options.get_bool_option("call-stack")) { - hf = util_make_unique( + hf = std::make_unique( options.get_unsigned_int_option("call-stack-recursion-limit")); } else if(options.get_bool_option("local-control-flow-history")) { - hf = util_make_unique( + hf = std::make_unique( options.get_bool_option("local-control-flow-history-forward"), options.get_bool_option("local-control-flow-history-backward"), options.get_unsigned_int_option("local-control-flow-history-limit")); @@ -65,17 +65,17 @@ std::unique_ptr build_analyzer( std::unique_ptr df = nullptr; if(options.get_bool_option("constants")) { - df = util_make_unique< + df = std::make_unique< ai_domain_factory_default_constructort>(); } else if(options.get_bool_option("intervals")) { - df = util_make_unique< + df = std::make_unique< ai_domain_factory_default_constructort>(); } else if(options.get_bool_option("vsd")) { - df = util_make_unique( + df = std::make_unique( vs_object_factory, vsd_config); } // non-null is not fully supported, despite the historical options @@ -86,11 +86,11 @@ std::unique_ptr build_analyzer( std::unique_ptr st = nullptr; if(options.get_bool_option("one-domain-per-history")) { - st = util_make_unique(); + st = std::make_unique(); } else if(options.get_bool_option("one-domain-per-location")) { - st = util_make_unique(); + st = std::make_unique(); } // Only try to build the abstract interpreter if all the parts have been @@ -99,7 +99,7 @@ std::unique_ptr build_analyzer( { if(options.get_bool_option("recursive-interprocedural")) { - return util_make_unique( + return std::make_unique( std::move(hf), std::move(df), std::move(st), mh); } else if(options.get_bool_option("three-way-merge")) @@ -107,7 +107,7 @@ std::unique_ptr build_analyzer( // Only works with VSD if(options.get_bool_option("vsd")) { - return util_make_unique( + return std::make_unique( std::move(hf), std::move(df), std::move(st), mh); } } @@ -118,33 +118,33 @@ std::unique_ptr build_analyzer( if(options.get_bool_option("constants")) { // constant_propagator_ait derives from ait - return util_make_unique( + return std::make_unique( goto_model.goto_functions); } else if(options.get_bool_option("dependence-graph")) { - return util_make_unique(ns); + return std::make_unique(ns); } else if(options.get_bool_option("dependence-graph-vs")) { - return util_make_unique( + return std::make_unique( goto_model.goto_functions, ns, vs_object_factory, vsd_config, mh); } else if(options.get_bool_option("vsd")) { - auto df = util_make_unique( + auto df = std::make_unique( vs_object_factory, vsd_config); - return util_make_unique>(std::move(df)); + return std::make_unique>(std::move(df)); } else if(options.get_bool_option("intervals")) { - return util_make_unique>(); + return std::make_unique>(); } #if 0 // Not actually implemented, despite the option... else if(options.get_bool_option("non-null")) { - return util_make_unique >(); + return std::make_unique >(); } #endif } @@ -156,7 +156,7 @@ std::unique_ptr build_analyzer( // 'non-revertable' and it has merge shared if(options.get_bool_option("dependence-graph")) { - return util_make_unique(ns); + return std::make_unique(ns); } #endif } diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp index c99a6cfb423..b434a4d3a38 100644 --- a/src/goto-checker/bmc_util.cpp +++ b/src/goto-checker/bmc_util.cpp @@ -27,7 +27,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include -#include #include #include "goto_symex_property_decider.h" @@ -165,11 +164,11 @@ get_memory_model(const optionst &options, const namespacet &ns) const std::string mm = options.get_option("mm"); if(mm.empty() || mm == "sc") - return util_make_unique(ns); + return std::make_unique(ns); else if(mm == "tso") - return util_make_unique(ns); + return std::make_unique(ns); else if(mm == "pso") - return util_make_unique(ns); + return std::make_unique(ns); else { throw "invalid memory model '" + mm + "': use one of sc, tso, pso"; diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 13f4ce14acd..7b6e0b2078e 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -62,7 +62,7 @@ operator()(propertiest &properties) { update_properties(properties, result.updated_properties, path.equation); - property_decider = util_make_unique( + property_decider = std::make_unique( options, ui_message_handler, path.equation, ns); const auto solver_runtime = diff --git a/src/goto-checker/solver_factory.cpp b/src/goto-checker/solver_factory.cpp index 0dc0dffa550..c44842474a8 100644 --- a/src/goto-checker/solver_factory.cpp +++ b/src/goto-checker/solver_factory.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include #include -#include #include #include #include @@ -192,14 +191,14 @@ template static std::unique_ptr make_satcheck_prop(message_handlert &message_handler, const optionst &options) { - auto satcheck = util_make_unique(message_handler); + auto satcheck = std::make_unique(message_handler); if(options.is_set("write-solver-stats-to")) { if( auto hardness_collector = dynamic_cast(&*satcheck)) { std::unique_ptr solver_hardness = - util_make_unique(); + std::make_unique(); solver_hardness->set_outfile(options.get_option("write-solver-stats-to")); hardness_collector->solver_hardness = std::move(solver_hardness); } @@ -345,7 +344,7 @@ std::unique_ptr solver_factoryt::get_default() bool get_array_constraints = options.get_bool_option("show-array-constraints"); - auto bv_pointers = util_make_unique( + auto bv_pointers = std::make_unique( ns, *sat_solver, message_handler, get_array_constraints); if(options.get_option("arrays-uf") == "never") @@ -355,7 +354,7 @@ std::unique_ptr solver_factoryt::get_default() set_decision_procedure_time_limit(*bv_pointers); - return util_make_unique( + return std::make_unique( std::move(bv_pointers), std::move(sat_solver)); } @@ -364,14 +363,14 @@ std::unique_ptr solver_factoryt::get_dimacs() no_beautification(); no_incremental_check(); - auto prop = util_make_unique(message_handler); + auto prop = std::make_unique(message_handler); std::string filename = options.get_option("outfile"); auto bv_dimacs = - util_make_unique(ns, *prop, message_handler, filename); + std::make_unique(ns, *prop, message_handler, filename); - return util_make_unique(std::move(bv_dimacs), std::move(prop)); + return std::make_unique(std::move(bv_dimacs), std::move(prop)); } std::unique_ptr solver_factoryt::get_external_sat() @@ -381,11 +380,11 @@ std::unique_ptr solver_factoryt::get_external_sat() std::string external_sat_solver = options.get_option("external-sat-solver"); auto prop = - util_make_unique(message_handler, external_sat_solver); + std::make_unique(message_handler, external_sat_solver); - auto bv_pointers = util_make_unique(ns, *prop, message_handler); + auto bv_pointers = std::make_unique(ns, *prop, message_handler); - return util_make_unique(std::move(bv_pointers), std::move(prop)); + return std::make_unique(std::move(bv_pointers), std::move(prop)); } std::unique_ptr solver_factoryt::get_bv_refinement() @@ -406,9 +405,9 @@ std::unique_ptr solver_factoryt::get_bv_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto decision_procedure = util_make_unique(info); + auto decision_procedure = std::make_unique(info); set_decision_procedure_time_limit(*decision_procedure); - return util_make_unique( + return std::make_unique( std::move(decision_procedure), std::move(prop)); } @@ -431,9 +430,9 @@ solver_factoryt::get_string_refinement() info.refine_arithmetic = options.get_bool_option("refine-arithmetic"); info.message_handler = &message_handler; - auto decision_procedure = util_make_unique(info); + auto decision_procedure = std::make_unique(info); set_decision_procedure_time_limit(*decision_procedure); - return util_make_unique( + return std::make_unique( std::move(decision_procedure), std::move(prop)); } @@ -445,7 +444,7 @@ std::unique_ptr open_outfile_and_check( if(filename.empty()) return nullptr; - auto out = util_make_unique(widen_if_needed(filename)); + auto out = std::make_unique(widen_if_needed(filename)); if(!*out) { @@ -483,7 +482,7 @@ solver_factoryt::get_incremental_smt2(std::string solver_command) on_std_out ? nullptr : open_outfile_and_check(outfile_arg, message_handler, "--outfile"); - solver_process = util_make_unique( + solver_process = std::make_unique( message_handler, on_std_out ? std::cout : *outfile, std::move(outfile)); } else @@ -492,15 +491,15 @@ solver_factoryt::get_incremental_smt2(std::string solver_command) // If no out_filename is provided `open_outfile_and_check` will return // `nullptr`, and the solver will work normally without any logging. - solver_process = util_make_unique( + solver_process = std::make_unique( std::move(solver_command), message_handler, open_outfile_and_check( out_filename, message_handler, "--dump-smt-formula")); } - return util_make_unique( - util_make_unique( + return std::make_unique( + std::make_unique( ns, std::move(solver_process), message_handler)); } @@ -521,7 +520,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) "provide a filename with --outfile"); } - auto smt2_dec = util_make_unique( + auto smt2_dec = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -533,11 +532,11 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_dec->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_dec); - return util_make_unique(std::move(smt2_dec)); + return std::make_unique(std::move(smt2_dec)); } else if(filename == "-") { - auto smt2_conv = util_make_unique( + auto smt2_conv = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -549,13 +548,13 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_conv->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_conv); - return util_make_unique(std::move(smt2_conv)); + return std::make_unique(std::move(smt2_conv)); } else { auto out = open_outfile_and_check(filename, message_handler, "--outfile"); - auto smt2_conv = util_make_unique( + auto smt2_conv = std::make_unique( ns, "cbmc", std::string("Generated by CBMC ") + CBMC_VERSION, @@ -567,7 +566,7 @@ solver_factoryt::get_smt2(smt2_dect::solvert solver) smt2_conv->use_FPA_theory = true; set_decision_procedure_time_limit(*smt2_conv); - return util_make_unique(std::move(smt2_conv), std::move(out)); + return std::make_unique(std::move(smt2_conv), std::move(out)); } } diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index f4100354a3a..d32e51bf6d5 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -11,7 +11,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include #include #include @@ -95,7 +94,7 @@ struct function_call_harness_generatort::implt function_call_harness_generatort::function_call_harness_generatort( ui_message_handlert &message_handler) - : goto_harness_generatort{}, p_impl(util_make_unique()) + : goto_harness_generatort{}, p_impl(std::make_unique()) { p_impl->message_handler = &message_handler; } @@ -254,7 +253,7 @@ void function_call_harness_generatort::implt::generate( map_function_parameters_to_function_argument_names(); recursive_initialization_config.pointers_to_treat_as_cstrings = function_arguments_to_treat_as_cstrings; - recursive_initialization = util_make_unique( + recursive_initialization = std::make_unique( recursive_initialization_config, goto_model); generate_nondet_globals(function_body); diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index 56741e3e1d6..117e5661064 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -13,7 +13,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include #include @@ -258,12 +257,12 @@ goto_harness_generator_factoryt goto_harness_parse_optionst::make_factory() { auto factory = goto_harness_generator_factoryt{}; factory.register_generator("call-function", [this]() { - return util_make_unique( + return std::make_unique( ui_message_handler); }); factory.register_generator("initialize-with-memory-snapshot", [this]() { - return util_make_unique( + return std::make_unique( ui_message_handler); }); diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h index 83a4963746e..cea48a83d76 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h @@ -14,8 +14,6 @@ Author: Matt Lewis #include -#include - #include #include @@ -49,7 +47,7 @@ class enumerating_loop_accelerationt goto_functions, guard_manager), path_limit(_path_limit), - path_enumerator(util_make_unique( + path_enumerator(std::make_unique( message_handler, symbol_table, goto_functions, diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index cdc37eca0ef..36c44ad6a97 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -14,7 +14,6 @@ Author: Matt Lewis #include -#include #include #include @@ -73,7 +72,7 @@ class scratch_programt:public goto_programt path_storage(), options(get_default_options()), symex(mh, symbol_table, equation, options, path_storage, guard_manager), - satcheck(util_make_unique(mh)), + satcheck(std::make_unique(mh)), satchecker(ns, *satcheck, mh), z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3, mh), checker(&z3) // checker(&satchecker) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 1447191158c..96fb6020e22 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -14,7 +14,6 @@ Date: May 2016 #include "cover.h" #include -#include #include #include @@ -65,44 +64,40 @@ void cover_instrumenterst::add_from_criterion( switch(criterion) { case coverage_criteriont::LOCATION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::BRANCH: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::DECISION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::CONDITION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::PATH: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::MCDC: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::ASSERTION: - instrumenters.push_back( - util_make_unique( - symbol_table, goal_filters)); + instrumenters.push_back(std::make_unique( + symbol_table, goal_filters)); break; case coverage_criteriont::COVER: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); break; case coverage_criteriont::ASSUME: instrumenters.push_back( - util_make_unique(symbol_table, goal_filters)); + std::make_unique(symbol_table, goal_filters)); } } @@ -194,9 +189,9 @@ cover_configt get_cover_config( std::unique_ptr &goal_filters = cover_config.goal_filters; cover_instrumenterst &instrumenters = cover_config.cover_instrumenters; - function_filters.add(util_make_unique()); + function_filters.add(std::make_unique()); - goal_filters->add(util_make_unique()); + goal_filters->add(std::make_unique()); optionst::value_listt criteria_strings = options.get_list_option("cover"); @@ -227,11 +222,11 @@ cover_configt get_cover_config( if(!cover_include_pattern.empty()) { function_filters.add( - util_make_unique(cover_include_pattern)); + std::make_unique(cover_include_pattern)); } if(options.get_bool_option("no-trivial-tests")) - function_filters.add(util_make_unique()); + function_filters.add(std::make_unique()); cover_config.traces_must_terminate = options.get_bool_option("cover-traces-must-terminate"); @@ -265,13 +260,13 @@ cover_configt get_cover_config( { const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id); cover_config.function_filters.add( - util_make_unique(main_symbol.name)); + std::make_unique(main_symbol.name)); } else if(cover_only == "file") { const symbolt &main_symbol = symbol_table.lookup_ref(main_function_id); cover_config.function_filters.add( - util_make_unique(main_symbol.location.get_file())); + std::make_unique(main_symbol.location.get_file())); } else if(!cover_only.empty()) { diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 4d5026d3a9a..8cd756bc25d 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -16,7 +16,6 @@ Date: May 2016 #include "cover_filter.h" #include "cover_instrument.h" -#include "util/make_unique.h" class cmdlinet; class goto_modelt; @@ -64,7 +63,7 @@ struct cover_configt function_filterst function_filters; // cover instruments point to goal_filters, so they must be stored on the heap std::unique_ptr goal_filters = - util_make_unique(); + std::make_unique(); cover_instrumenterst cover_instrumenters; cover_instrumenter_baset::assertion_factoryt make_assertion = goto_programt::make_assertion; diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 5098922a65a..3687fb65187 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -16,7 +16,6 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include @@ -381,7 +380,7 @@ std::unique_ptr generate_function_bodies_factory( { if(options.empty() || options == "nondet-return") { - return util_make_unique( + return std::make_unique( std::vector{}, std::regex{}, object_factory_parameters, @@ -390,17 +389,17 @@ std::unique_ptr generate_function_bodies_factory( if(options == "assume-false") { - return util_make_unique(); + return std::make_unique(); } if(options == "assert-false") { - return util_make_unique(); + return std::make_unique(); } if(options == "assert-false-assume-false") { - return util_make_unique< + return std::make_unique< assert_false_then_assume_false_generate_function_bodiest>(); } @@ -477,13 +476,13 @@ std::unique_ptr generate_function_bodies_factory( } } if(param_numbers.empty()) - return util_make_unique( + return std::make_unique( std::move(globals_to_havoc), std::move(params_regex), object_factory_parameters, message_handler); else - return util_make_unique( + return std::make_unique( std::move(globals_to_havoc), std::move(param_numbers), object_factory_parameters, diff --git a/src/goto-symex/path_storage.cpp b/src/goto-symex/path_storage.cpp index 39134334753..3197de7b4cb 100644 --- a/src/goto-symex/path_storage.cpp +++ b/src/goto-symex/path_storage.cpp @@ -12,7 +12,6 @@ Author: Kareem Khazem #include #include -#include nondet_symbol_exprt symex_nondet_generatort:: operator()(typet type, source_locationt location) @@ -97,7 +96,7 @@ static const std::map< " last-in, first-out order. Explores\n" " the program tree depth-first.\n", []() { // NOLINT(whitespace/braces) - return util_make_unique(); + return std::make_unique(); }}}, {"fifo", {" fifo next instruction is pushed before\n" @@ -105,7 +104,7 @@ static const std::map< " first-in, first-out order. Explores\n" " the program tree breadth-first.\n", []() { // NOLINT(whitespace/braces) - return util_make_unique(); + return std::make_unique(); }}}}); std::string show_path_strategies() diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index a9c11fb982f..bc1d420f71b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -21,7 +21,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -417,7 +416,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( auto *storage = &path_storage; // create and prepare the state - auto state = util_make_unique( + auto state = std::make_unique( symex_targett::sourcet(entry_point_id, start_function->body), symex_config.max_field_sensitivity_array_size, symex_config.simplify_opt, diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 97a0058ea9a..4b1090f07db 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -591,7 +591,7 @@ optionalt cegis_verifiert::verify() preprocess_goto_model(); std::unique_ptr< all_properties_verifier_with_trace_storaget> - checker = util_make_unique< + checker = std::make_unique< all_properties_verifier_with_trace_storaget>( options, ui_message_handler, goto_model); diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp index 58caa64c018..1ad144c3ce1 100644 --- a/src/jsil/jsil_language.cpp +++ b/src/jsil/jsil_language.cpp @@ -101,7 +101,7 @@ void jsil_languaget::show_parse(std::ostream &out) std::unique_ptr new_jsil_language() { - return util_make_unique(); + return std::make_unique(); } bool jsil_languaget::from_expr( diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h index 7138620118b..4d99beff857 100644 --- a/src/jsil/jsil_language.h +++ b/src/jsil/jsil_language.h @@ -14,8 +14,6 @@ Author: Michael Tautschnig, tautschn@amazon.com #include -#include - #include #include "jsil_parse_tree.h" @@ -53,7 +51,9 @@ class jsil_languaget:public languaget const namespacet &ns) override; std::unique_ptr new_language() override - { return util_make_unique(); } + { + return std::make_unique(); + } std::string id() const override { diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h index cea1ceefb89..097daecfcab 100644 --- a/src/json-symtab-language/json_symtab_language.h +++ b/src/json-symtab-language/json_symtab_language.h @@ -12,7 +12,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com #define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H #include -#include #include #include @@ -55,7 +54,7 @@ class json_symtab_languaget : public languaget std::unique_ptr new_language() override { - return util_make_unique(); + return std::make_unique(); } bool generate_support_functions(symbol_table_baset &symbol_table) override @@ -75,7 +74,7 @@ class json_symtab_languaget : public languaget inline std::unique_ptr new_json_symtab_language() { - return util_make_unique(); + return std::make_unique(); } #endif diff --git a/src/libcprover-cpp/api.cpp b/src/libcprover-cpp/api.cpp index aeb3fd2d842..652478d57f9 100644 --- a/src/libcprover-cpp/api.cpp +++ b/src/libcprover-cpp/api.cpp @@ -36,7 +36,7 @@ extern configt config; std::unique_ptr api_sessiont::get_api_version() const { - return util_make_unique(std::string{CBMC_VERSION}); + return std::make_unique(std::string{CBMC_VERSION}); } struct api_session_implementationt @@ -51,10 +51,10 @@ api_sessiont::api_sessiont() : api_sessiont{api_optionst::create()} } api_sessiont::api_sessiont(const api_optionst &options) - : implementation{util_make_unique()} + : implementation{std::make_unique()} { implementation->message_handler = - util_make_unique(null_message_handlert{}); + std::make_unique(null_message_handlert{}); implementation->options = options.to_engine_options(); // Needed to initialise the language options correctly cmdlinet cmdline; @@ -130,13 +130,13 @@ void api_sessiont::set_message_callback( api_call_back_contextt context) { implementation->message_handler = - util_make_unique(callback, context); + std::make_unique(callback, context); } void api_sessiont::load_model_from_files( const std::vector &files) const { - implementation->model = util_make_unique(initialize_goto_model( + implementation->model = std::make_unique(initialize_goto_model( files, *implementation->message_handler, *implementation->options)); } @@ -161,7 +161,7 @@ void api_sessiont::read_goto_binary(std::string &file) const if(read_opt_val.has_value()) { implementation->model = - util_make_unique(std::move(read_opt_val.value())); + std::make_unique(std::move(read_opt_val.value())); } else { @@ -228,7 +228,7 @@ std::unique_ptr api_sessiont::run_verifier() const auto properties = verifier.get_properties(); result.set_properties(properties); - return util_make_unique(result); + return std::make_unique(result); } void api_sessiont::drop_unused_functions() const diff --git a/src/libcprover-cpp/api_options.cpp b/src/libcprover-cpp/api_options.cpp index d11e01785ac..c4d1839ddec 100644 --- a/src/libcprover-cpp/api_options.cpp +++ b/src/libcprover-cpp/api_options.cpp @@ -3,7 +3,6 @@ #include "api_options.h" #include -#include #include #include @@ -16,7 +15,7 @@ api_optionst api_optionst::create() static std::unique_ptr make_internal_default_options() { - std::unique_ptr options = util_make_unique(); + std::unique_ptr options = std::make_unique(); cmdlinet command_line; PARSE_OPTIONS_GOTO_CHECK(command_line, (*options)); parse_solver_options(command_line, *options); diff --git a/src/libcprover-cpp/verification_result.cpp b/src/libcprover-cpp/verification_result.cpp index f7d801f733a..fd18f7ef4a2 100644 --- a/src/libcprover-cpp/verification_result.cpp +++ b/src/libcprover-cpp/verification_result.cpp @@ -8,7 +8,6 @@ #include #include -#include #include @@ -61,7 +60,7 @@ verification_resultt::verification_result_implt::get_properties() // Verification_result verification_resultt::verification_resultt() - : _impl(util_make_unique()) + : _impl(std::make_unique()) { } @@ -70,7 +69,7 @@ verification_resultt::~verification_resultt() } verification_resultt::verification_resultt(const verification_resultt &other) - : _impl(util_make_unique(*other._impl)) + : _impl(std::make_unique(*other._impl)) { } diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h index d917471be3d..4003ff47f05 100644 --- a/src/pointer-analysis/value_set_analysis.h +++ b/src/pointer-analysis/value_set_analysis.h @@ -33,7 +33,7 @@ class value_set_analysis_templatet : public value_setst, public ait typedef typename baset::locationt locationt; explicit value_set_analysis_templatet(const namespacet &_ns) - : baset(util_make_unique>()), + : baset(std::make_unique>()), ns(_ns) { } diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp index 14bda00a080..d49b1a4d424 100644 --- a/src/solvers/sat/satcheck_glucose.cpp +++ b/src/solvers/sat/satcheck_glucose.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -254,7 +253,7 @@ void satcheck_glucose_baset::set_assignment(literalt a, bool value) template satcheck_glucose_baset::satcheck_glucose_baset( message_handlert &message_handler) - : cnf_solvert(message_handler), solver(util_make_unique()) + : cnf_solvert(message_handler), solver(std::make_unique()) { } diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp index 2c9799cc700..dc26882ad4b 100644 --- a/src/solvers/sat/satcheck_minisat2.cpp +++ b/src/solvers/sat/satcheck_minisat2.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include @@ -325,7 +324,7 @@ template satcheck_minisat2_baset::satcheck_minisat2_baset( message_handlert &message_handler) : cnf_solvert(message_handler), - solver(util_make_unique()), + solver(std::make_unique()), time_limit_seconds(0) { } diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 48ebcfa1a60..3a77517173c 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -6,7 +6,6 @@ #include #include #include -#include #include #include #include @@ -19,12 +18,12 @@ #include struct_encodingt::struct_encodingt(const namespacet &ns) - : boolbv_width{util_make_unique(ns)}, ns{ns} + : boolbv_width{std::make_unique(ns)}, ns{ns} { } struct_encodingt::struct_encodingt(const struct_encodingt &other) - : boolbv_width{util_make_unique(*other.boolbv_width)}, + : boolbv_width{std::make_unique(*other.boolbv_width)}, ns{other.ns} { } diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp index bb7aeab4d9a..2a0ab220886 100644 --- a/src/solvers/strings/string_dependencies.cpp +++ b/src/solvers/strings/string_dependencies.cpp @@ -12,7 +12,6 @@ Author: Diffblue Ltd. #include #include #include -#include #include /// Applies `f` on all strings contained in `e` that are not if-expressions. @@ -34,38 +33,38 @@ static std::unique_ptr to_string_builtin_function( const irep_idt &id = name.get_identifier(); if(id == ID_cprover_string_insert_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_concat_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_concat_char_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_format_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_of_int_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_char_set_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_to_lower_case_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); if(id == ID_cprover_string_to_upper_case_func) - return util_make_unique( + return std::make_unique( return_code, fun_app.arguments(), array_pool); - return util_make_unique( + return std::make_unique( return_code, fun_app, array_pool); } @@ -85,7 +84,7 @@ string_dependenciest::node_at(const array_string_exprt &e) const { const auto &it = node_index_pool.find(e); if(it != node_index_pool.end()) - return util_make_unique(string_nodes.at(it->second)); + return std::make_unique(string_nodes.at(it->second)); return {}; } diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp index f9d7fe9be6b..28087cdb0b8 100644 --- a/src/statement-list/statement_list_language.cpp +++ b/src/statement-list/statement_list_language.cpp @@ -19,7 +19,6 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com #include #include #include -#include #include void statement_list_languaget::set_language_options(const optionst &options) @@ -144,12 +143,12 @@ std::set statement_list_languaget::extensions() const std::unique_ptr new_statement_list_language() { - return util_make_unique(); + return std::make_unique(); } std::unique_ptr statement_list_languaget::new_language() { - return util_make_unique(); + return std::make_unique(); } std::string statement_list_languaget::id() const diff --git a/src/util/make_unique.h b/src/util/make_unique.h deleted file mode 100644 index 0f4ba41ac3e..00000000000 --- a/src/util/make_unique.h +++ /dev/null @@ -1,24 +0,0 @@ -/*******************************************************************\ - -Module: Really simple unique_ptr utilities - -Author: Reuben Thomas, reuben.thomas@diffblue.com - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_MAKE_UNIQUE_H -#define CPROVER_UTIL_MAKE_UNIQUE_H - -#include // unique_ptr - -// This is a stand-in for std::make_unique, which isn't part of the standard -// library until C++14. When we move to C++14, we should do a find-and-replace -// on this to use std::make_unique instead. - -template -std::unique_ptr util_make_unique(Ts &&... ts) -{ - return std::unique_ptr(new T(std::forward(ts)...)); -} - -#endif diff --git a/src/util/piped_process.cpp b/src/util/piped_process.cpp index f5b028ae2f6..a9427d7671e 100644 --- a/src/util/piped_process.cpp +++ b/src/util/piped_process.cpp @@ -79,7 +79,6 @@ # include "run.h" // for Windows arg quoting # include "unicode.h" // for widen function # include // library for _tcscpy function -# include # include #else # include // library for fcntl function @@ -213,7 +212,7 @@ piped_processt::piped_processt( } // Create the child process STARTUPINFOW start_info; - proc_info = util_make_unique(); + proc_info = std::make_unique(); ZeroMemory(proc_info.get(), sizeof(PROCESS_INFORMATION)); ZeroMemory(&start_info, sizeof(STARTUPINFOW)); start_info.cb = sizeof(STARTUPINFOW); diff --git a/src/util/range.h b/src/util/range.h index d884e7635fe..0f09e9b9e61 100644 --- a/src/util/range.h +++ b/src/util/range.h @@ -14,12 +14,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_UTIL_RANGE_H #define CPROVER_UTIL_RANGE_H +#include + #include +#include #include -#include -#include - /// Iterator which applies some given function \c f after each increment and /// returns its result on dereference. template @@ -349,7 +349,7 @@ struct zip_iteratort !same_size || ((first_begin == first_end) == (second_begin == second_end))); if(first_begin != first_end) - current = util_make_unique(*first_begin, *second_begin); + current = std::make_unique(*first_begin, *second_begin); } private: diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index fe7eb5f26fd..4caf809bb55 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -35,7 +35,6 @@ Author: Daniel Poetzl #include "as_const.h" #include "invariant.h" -#include "make_unique.h" #include "small_shared_n_way_ptr.h" #include "small_shared_ptr.h" diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp index 13204451ead..69302626dc7 100644 --- a/src/util/ui_message.cpp +++ b/src/util/ui_message.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "json.h" #include "json_irep.h" #include "json_stream.h" -#include "make_unique.h" #include "structured_data.h" #include "xml.h" #include "xml_irep.h" @@ -86,7 +85,7 @@ ui_message_handlert::ui_message_handlert( if(get_ui() == uit::PLAIN) { console_message_handler = - util_make_unique(always_flush); + std::make_unique(always_flush); message_handler = &*console_message_handler; } } diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 05f9694b07b..57ffbc1fe8b 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -5,7 +5,6 @@ #include #include #include -#include #include #include #include @@ -120,7 +119,7 @@ struct decision_procedure_test_environmentt final smt_is_dynamic_objectt is_dynamic_object_function; smt2_incremental_decision_proceduret procedure{ ns, - util_make_unique( + std::make_unique( [&](const smt_commandt &smt_command) { this->send(smt_command); }, [&]() { return this->receive_response(); }), message_handler};