forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
With the move to C++ 17 we can use std::make_unique instead.
- Loading branch information
1 parent
a8de0b7
commit c17285c
Showing
58 changed files
with
188 additions
and
253 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected] | |
#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_LANGUAGE_H | ||
|
||
#include <util/json.h> | ||
#include <util/make_unique.h> | ||
#include <util/prefix_filter.h> | ||
#include <util/symbol.h> // IWYU pragma: keep | ||
|
||
|
@@ -319,7 +318,9 @@ class java_bytecode_languaget:public languaget | |
const namespacet &ns) override; | ||
|
||
std::unique_ptr<languaget> new_language() override | ||
{ return util_make_unique<java_bytecode_languaget>(); } | ||
{ | ||
return std::make_unique<java_bytecode_languaget>(); | ||
} | ||
|
||
std::string id() const override { return "java"; } | ||
std::string description() const override { return "Java Bytecode"; } | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected] | |
#include <util/exit_codes.h> | ||
#include <util/help_formatter.h> | ||
#include <util/invariant.h> | ||
#include <util/make_unique.h> | ||
#include <util/version.h> | ||
#include <util/xml.h> | ||
|
||
|
@@ -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<stop_on_fail_verifiert<java_single_path_symex_checkert>>( | ||
std::make_unique<stop_on_fail_verifiert<java_single_path_symex_checkert>>( | ||
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<stop_on_fail_verifier_with_fault_localizationt< | ||
std::make_unique<stop_on_fail_verifier_with_fault_localizationt< | ||
java_multi_path_symex_checkert>>( | ||
options, ui_message_handler, *goto_model_ptr); | ||
} | ||
else | ||
{ | ||
verifier = util_make_unique< | ||
verifier = std::make_unique< | ||
stop_on_fail_verifiert<java_multi_path_symex_checkert>>( | ||
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<all_properties_verifier_with_trace_storaget< | ||
verifier = std::make_unique<all_properties_verifier_with_trace_storaget< | ||
java_single_path_symex_checkert>>( | ||
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<all_properties_verifier_with_fault_localizationt< | ||
std::make_unique<all_properties_verifier_with_fault_localizationt< | ||
java_multi_path_symex_checkert>>( | ||
options, ui_message_handler, *goto_model_ptr); | ||
} | ||
else | ||
{ | ||
verifier = util_make_unique<all_properties_verifier_with_trace_storaget< | ||
verifier = std::make_unique<all_properties_verifier_with_trace_storaget< | ||
java_multi_path_symex_checkert>>( | ||
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<class_hierarchyt>(lazy_goto_model.symbol_table); | ||
std::make_unique<class_hierarchyt>(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<lazy_goto_modelt>(std::move(lazy_goto_model)); | ||
std::make_unique<lazy_goto_modelt>(std::move(lazy_goto_model)); | ||
} | ||
|
||
log.status() << config.object_bits_info() << messaget::eom; | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -50,7 +50,6 @@ Author: Daniel Kroening, [email protected] | |
|
||
#include <util/deprecate.h> | ||
#include <util/json.h> | ||
#include <util/make_unique.h> | ||
#include <util/message.h> | ||
#include <util/xml.h> | ||
|
||
|
@@ -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<ahistoricalt>>(), | ||
util_make_unique<ai_domain_factory_default_constructort<domainT>>(), | ||
util_make_unique<location_sensitive_storaget>(), | ||
std::make_unique<ai_domain_factory_default_constructort<domainT>>(), | ||
std::make_unique<location_sensitive_storaget>(), | ||
no_logging) | ||
{ | ||
} | ||
|
||
explicit ait(std::unique_ptr<ai_domain_factory_baset> &&df) | ||
: ai_recursive_interproceduralt( | ||
util_make_unique< | ||
std::make_unique< | ||
ai_history_factory_default_constructort<ahistoricalt>>(), | ||
std::move(df), | ||
util_make_unique<location_sensitive_storaget>(), | ||
std::make_unique<location_sensitive_storaget>(), | ||
no_logging) | ||
{ | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -41,7 +41,6 @@ Author: Daniel Kroening, [email protected] | |
#define CPROVER_ANALYSES_AI_DOMAIN_H | ||
|
||
#include <util/json.h> | ||
#include <util/make_unique.h> | ||
#include <util/xml.h> | ||
|
||
#include "ai_history.h" | ||
|
@@ -206,7 +205,7 @@ class ai_domain_factoryt : public ai_domain_factory_baset | |
|
||
std::unique_ptr<statet> copy(const statet &s) const override | ||
{ | ||
return util_make_unique<domainT>(static_cast<const domainT &>(s)); | ||
return std::make_unique<domainT>(static_cast<const domainT &>(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<statet> make(locationt l) const override | ||
{ | ||
auto d = util_make_unique<domainT>(); | ||
auto d = std::make_unique<domainT>(); | ||
CHECK_RETURN(d->is_bottom()); | ||
return std::unique_ptr<statet>(d.release()); | ||
} | ||
|
@@ -246,7 +245,7 @@ class ai_domain_factory_location_constructort | |
|
||
std::unique_ptr<statet> make(locationt l) const override | ||
{ | ||
auto d = util_make_unique<domainT>(l); | ||
auto d = std::make_unique<domainT>(l); | ||
CHECK_RETURN(d->is_bottom()); | ||
return std::unique_ptr<statet>(d.release()); | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected] | |
#include <stack> | ||
|
||
#include <util/union_find.h> | ||
#include <util/make_unique.h> | ||
|
||
#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<local_may_aliast>(f_it2->second)); | ||
return *(fkt_map[fkt] = std::make_unique<local_may_aliast>(f_it2->second)); | ||
} | ||
|
||
local_may_aliast &operator()(goto_programt::const_targett t) | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.