diff --git a/.clang-format-ignore b/.clang-format-ignore index bf05754242fa..7d2a397c6b32 100644 --- a/.clang-format-ignore +++ b/.clang-format-ignore @@ -1,4 +1,3 @@ jbmc/src/miniz/miniz.cpp src/cprover/wcwidth.c -src/nonstd/optional.hpp unit/catch/catch.hpp diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 0b3eee5c96ce..ad856986c4a1 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -445,7 +445,7 @@ int janalyzer_parse_optionst::perform_analysis( } else { - optionalt json_file; + std::optional json_file; if(cmdline.isset("json")) json_file = cmdline.get_value("json"); bool result = taint_analysis( diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index ccb0445f8648..f7593c2a23e5 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -677,7 +677,7 @@ used. Under eager loading \ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, lazy_class_to_declared_symbols_mapt &, message_handlert &) is called once for each method listed in method_bytecode (described above). This then calls -\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, optionalt, lazy_class_to_declared_symbols_mapt &, message_handlert &); +\ref java_bytecode_languaget::convert_single_method(const irep_idt &, symbol_table_baset &, std::optional, lazy_class_to_declared_symbols_mapt &, message_handlert &); without a ci_lazy_methods_neededt object, which calls \ref java_bytecode_convert_method, passing in the method parse tree. This in diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp index 223f5a5187e6..f9e7a0758077 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.cpp +++ b/jbmc/src/java_bytecode/assignments_from_json.cpp @@ -44,7 +44,7 @@ struct object_creation_infot /// Where runtime types differ from compile-time types, we need to mark the /// runtime types as needed by lazy methods. - optionalt &needed_lazy_methods; + std::optional &needed_lazy_methods; /// Map to keep track of reference-equal objects. Each entry has an ID (such /// that any two reference-equal objects have the same ID) and the expression @@ -117,7 +117,7 @@ static bool is_enum_with_type_equal_to_declaring_type( /// A runtime type that is different from the objects compile-time type should /// be specified in `json` in this way. /// Type values are of the format "my.package.name.ClassName". -static optionalt get_type(const jsont &json) +static std::optional get_type(const jsont &json) { if(!json.is_object()) return {}; @@ -267,9 +267,9 @@ static jsont get_untyped_string(const jsont &json) /// \param symbol_table: used to look up the type given its name. /// \return runtime type of the object, if specified by at least one of the /// parameters. -static optionalt runtime_type( +static std::optional runtime_type( const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, const symbol_table_baset &symbol_table) { const auto type_from_json = get_type(json); @@ -304,9 +304,9 @@ static optionalt runtime_type( /// field, this takes priority over \p type_from_array. /// \param type_from_array: may contain a type name from a containing array. /// \return if the type of an array was given, the type of its elements. -static optionalt element_type_from_array_type( +static std::optional element_type_from_array_type( const jsont &json, - const optionalt &type_from_array) + const std::optional &type_from_array) { if(const auto json_array_type = get_type(json)) { @@ -332,7 +332,7 @@ static optionalt element_type_from_array_type( code_with_references_listt assign_from_json_rec( const exprt &expr, const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info); /// One of the base cases (primitive case) of the recursion. @@ -392,7 +392,7 @@ static code_frontend_assignt assign_null(const exprt &expr) static code_with_references_listt assign_array_data_component_from_json( const exprt &expr, const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info) { const auto &java_class_type = followed_class_type(expr, info.symbol_table); @@ -411,7 +411,7 @@ static code_with_references_listt assign_array_data_component_from_json( code_frontend_assignt{array_init_data, data_member_expr, info.loc}); size_t index = 0; - const optionalt inferred_element_type = + const std::optional inferred_element_type = element_type_from_array_type(json, type_from_array); const json_arrayt json_array = get_untyped_array(json, element_type); for(auto it = json_array.begin(); it < json_array.end(); it++, index++) @@ -457,7 +457,7 @@ static std::pair assign_det_length_array_from_json( const exprt &expr, const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info) { PRECONDITION(is_java_array_type(expr.type())); @@ -486,7 +486,7 @@ static code_with_references_listt assign_nondet_length_array_from_json( const exprt &array, const jsont &json, const exprt &given_length_expr, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info) { PRECONDITION(is_java_array_type(array.type())); @@ -793,7 +793,7 @@ static get_or_create_reference_resultt get_or_create_reference( static code_with_references_listt assign_reference_from_json( const exprt &expr, const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info) { const std::string &id = has_enum_type(expr, info.symbol_table) @@ -849,7 +849,7 @@ static code_with_references_listt assign_reference_from_json( code_with_references_listt assign_from_json_rec( const exprt &expr, const jsont &json, - const optionalt &type_from_array, + const std::optional &type_from_array, object_creation_infot &info) { code_with_references_listt result; @@ -915,7 +915,7 @@ code_with_references_listt assign_from_json( const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt &needed_lazy_methods, + std::optional &needed_lazy_methods, size_t max_user_array_length, std::unordered_map &references) { diff --git a/jbmc/src/java_bytecode/assignments_from_json.h b/jbmc/src/java_bytecode/assignments_from_json.h index 160ba4590f09..328fbb5c9b41 100644 --- a/jbmc/src/java_bytecode/assignments_from_json.h +++ b/jbmc/src/java_bytecode/assignments_from_json.h @@ -100,7 +100,7 @@ code_with_references_listt assign_from_json( const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt &needed_lazy_methods, + std::optional &needed_lazy_methods, size_t max_user_array_length, std::unordered_map &references); diff --git a/jbmc/src/java_bytecode/ci_lazy_methods.h b/jbmc/src/java_bytecode/ci_lazy_methods.h index d96174aec399..f37e153589eb 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods.h +++ b/jbmc/src/java_bytecode/ci_lazy_methods.h @@ -41,7 +41,8 @@ class method_bytecodet const java_bytecode_parse_treet::methodt &method; }; - typedef optionalt> + typedef std::optional< + std::reference_wrapper> opt_reft; private: diff --git a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp index 72964181f4d7..11d5c7dac59e 100644 --- a/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp +++ b/jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp @@ -53,7 +53,7 @@ void ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists( const irep_idt &class_id) { resolve_inherited_componentt resolve_inherited_component{symbol_table}; - optionalt + std::optional cprover_nondet_initialize = resolve_inherited_component( class_id, "cproverNondetInitialize:()V", true); diff --git a/jbmc/src/java_bytecode/code_with_references.h b/jbmc/src/java_bytecode/code_with_references.h index ba775f88ada9..6f38b69f0936 100644 --- a/jbmc/src/java_bytecode/code_with_references.h +++ b/jbmc/src/java_bytecode/code_with_references.h @@ -30,7 +30,7 @@ struct object_creation_referencet /// This should only be set once the actual elements of the array have been /// seen, not the first time an `@ref` have been seen, only when `@id` is /// seen. - optionalt array_length; + std::optional array_length; }; /// Base class for code which can contain references which can get replaced diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp index 39033edf2adf..5444a6f11f75 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp @@ -51,7 +51,7 @@ void generic_parameter_specialization_mapt::pop(std::size_t container_index) container_to_specializations.at(container_index).pop(); } -optionalt +std::optional generic_parameter_specialization_mapt::pop(const irep_idt ¶meter_name) { const auto types_it = param_to_container.find(parameter_name); diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map.h index 914dca2758b0..2a954e11e662 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map.h @@ -53,8 +53,8 @@ class generic_parameter_specialization_mapt /// a given type parameter /// \param parameter_name: The name of the type parameter /// \returns: The specialization for the given type parameter, if there was - /// one before the pop, or an empty optionalt if the stack was empty - optionalt pop(const irep_idt ¶meter_name); + /// one before the pop, or an empty std::optional if the stack was empty + std::optional pop(const irep_idt ¶meter_name); /// A wrapper for a generic_parameter_specialization_mapt and a namespacet /// that can be output to a stream diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h index f8f9f8dd8d85..bd1eaa79cc84 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -17,7 +17,7 @@ class generic_parameter_specialization_map_keyst /// Generic parameter specialization map to modify generic_parameter_specialization_mapt &generic_parameter_specialization_map; /// Key of the container to pop on destruction - optionalt container_id; + std::optional container_id; public: /// Initialize a generic-parameter-specialization-map entry owner operating diff --git a/jbmc/src/java_bytecode/jar_file.cpp b/jbmc/src/java_bytecode/jar_file.cpp index e4f29bece5cc..0cab95892160 100644 --- a/jbmc/src/java_bytecode/jar_file.cpp +++ b/jbmc/src/java_bytecode/jar_file.cpp @@ -54,7 +54,7 @@ jar_filet &jar_filet::operator=(jar_filet &&other) return *this; } -optionalt jar_filet::get_entry(const std::string &name) +std::optional jar_filet::get_entry(const std::string &name) { const auto entry=m_name_to_index.find(name); if(entry==m_name_to_index.end()) diff --git a/jbmc/src/java_bytecode/jar_file.h b/jbmc/src/java_bytecode/jar_file.h index bf6a1d02a0b3..aa7c1602b3cb 100644 --- a/jbmc/src/java_bytecode/jar_file.h +++ b/jbmc/src/java_bytecode/jar_file.h @@ -13,8 +13,6 @@ Author: Diffblue Ltd #include #include -#include - #include "mz_zip_archive.h" /// Class representing a .jar archive. Uses miniz to decompress and index @@ -42,7 +40,7 @@ class jar_filet final /// Get contents of a file in the jar archive. /// Returns nullopt if file doesn't exist. /// \param filename: Name of the file in the archive - optionalt get_entry(const std::string &filename); + std::optional get_entry(const std::string &filename); /// Get contents of the Manifest file in the jar archive as a key-value map /// (both as strings) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index d14a070e5068..f600348b9435 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -186,8 +186,8 @@ class java_bytecode_convert_classt /// \param signature: Signature of the class /// \return Reference of the generic superclass, or empty if the superclass /// is not generic -static optionalt -extract_generic_superclass_reference(const optionalt &signature) +static std::optional extract_generic_superclass_reference( + const std::optional &signature) { if(signature.has_value()) { @@ -226,8 +226,8 @@ extract_generic_superclass_reference(const optionalt &signature) /// \param interface_name: The interface name /// \return Reference of the generic interface, or empty if the interface /// is not generic -static optionalt extract_generic_interface_reference( - const optionalt &signature, +static std::optional extract_generic_interface_reference( + const std::optional &signature, const std::string &interface_name) { if(signature.has_value()) @@ -355,7 +355,7 @@ void java_bytecode_convert_classt::convert( // including the generic info in its signature // e.g., signature for class 'A' that extends // 'Generic' is 'LGeneric;' - const optionalt &superclass_ref = + const std::optional &superclass_ref = extract_generic_superclass_reference(c.signature); if(superclass_ref.has_value()) { @@ -397,7 +397,7 @@ void java_bytecode_convert_classt::convert( // including the generic info in its signature // e.g., signature for class 'A implements GenericInterface' is // 'Ljava/lang/Object;LGenericInterface;' - const optionalt interface_ref = + const std::optional interface_ref = extract_generic_interface_reference(c.signature, id2string(interface)); if(interface_ref.has_value()) { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 2416188aa0dc..758bcdf6ec84 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -228,7 +228,7 @@ exprt java_bytecode_convert_methodt::variable( /// \return the constructed member type java_method_typet member_type_lazy( const std::string &descriptor, - const optionalt &signature, + const std::optional &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler) @@ -534,7 +534,7 @@ void create_parameter_symbols( void java_bytecode_convert_methodt::convert( const symbolt &class_symbol, const methodt &m, - const optionalt &method_context) + const std::optional &method_context) { // Construct the fully qualified method name // (e.g. "my.package.ClassName.myMethodName:(II)I") and query the symbol table @@ -1263,7 +1263,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) } } - optionalt catch_instruction; + std::optional catch_instruction; if(catch_type!=typet()) { @@ -3083,7 +3083,7 @@ code_blockt java_bytecode_convert_methodt::convert_astore( return block; } -optionalt java_bytecode_convert_methodt::convert_invoke_dynamic( +std::optional java_bytecode_convert_methodt::convert_invoke_dynamic( const source_locationt &location, std::size_t instruction_address, const exprt &arg0, @@ -3282,11 +3282,11 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, - const optionalt &method_context, + const std::optional &method_context, bool assert_no_exceptions_thrown) { diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.h b/jbmc/src/java_bytecode/java_bytecode_convert_method.h index e9a0fe01742b..8ad5d25ad966 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.h @@ -31,11 +31,11 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, - const optionalt &method_context, + const std::optional &method_context, bool assert_no_exceptions_thrown); void create_method_stub_symbol( diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 011b0ff205ca..2d12b5377bd6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -40,7 +40,7 @@ class java_bytecode_convert_methodt message_handlert &_message_handler, size_t _max_array_length, bool throw_assertion_error, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, java_string_library_preprocesst &_string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support, @@ -69,7 +69,7 @@ class java_bytecode_convert_methodt void operator()( const symbolt &class_symbol, const methodt &method, - const optionalt &method_context) + const std::optional &method_context) { convert(class_symbol, method, method_context); } @@ -84,7 +84,7 @@ class java_bytecode_convert_methodt const bool throw_assertion_error; const bool assert_no_exceptions_thrown; const bool threading_support; - optionalt needed_lazy_methods; + std::optional needed_lazy_methods; /// Fully qualified name of the method under translation. /// Initialized by `convert`. @@ -319,7 +319,7 @@ class java_bytecode_convert_methodt void convert( const symbolt &class_symbol, const methodt &, - const optionalt &method_context); + const std::optional &method_context); code_blockt convert_parameter_annotations( const methodt &method, @@ -368,7 +368,7 @@ class java_bytecode_convert_methodt std::vector::const_iterator> &ret_instructions) const; - optionalt convert_invoke_dynamic( + std::optional convert_invoke_dynamic( const source_locationt &location, std::size_t instruction_address, const exprt &arg0, diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp index 9c908a29a722..a37d6688be95 100644 --- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp @@ -71,7 +71,7 @@ class java_bytecode_instrumentt void instrument_code(codet &code); void add_expr_instrumentation(code_blockt &block, const exprt &expr); void prepend_instrumentation(codet &code, code_blockt &instrumentation); - optionalt instrument_expr(const exprt &expr); + std::optional instrument_expr(const exprt &expr); }; const std::vector exception_needed_classes = { @@ -218,7 +218,7 @@ code_ifthenelset java_bytecode_instrumentt::check_class_cast( pointer_typet voidptr = pointer_type(java_void_type()); exprt null_check_op = typecast_exprt::conditional_cast(tested_expr, voidptr); - optionalt check_code; + std::optional check_code; if(throw_runtime_exceptions) { check_code= @@ -309,7 +309,7 @@ void java_bytecode_instrumentt::add_expr_instrumentation( code_blockt &block, const exprt &expr) { - if(optionalt expr_instrumentation = instrument_expr(expr)) + if(std::optional expr_instrumentation = instrument_expr(expr)) { if(expr_instrumentation->get_statement() == ID_block) block.append(to_code_block(*expr_instrumentation)); @@ -447,13 +447,14 @@ void java_bytecode_instrumentt::instrument_code(codet &code) /// either assertions or runtime exceptions. /// \param expr: the expression for which we compute instrumentation /// \return The instrumentation for \p expr if required -optionalt java_bytecode_instrumentt::instrument_expr(const exprt &expr) +std::optional +java_bytecode_instrumentt::instrument_expr(const exprt &expr) { code_blockt result; // First check our operands: for(const auto &op : expr.operands()) { - if(optionalt op_result = instrument_expr(op)) + if(std::optional op_result = instrument_expr(op)) result.add(std::move(*op_result)); } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index ae1acc79f91d..32d870c04946 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -1238,7 +1238,7 @@ void java_bytecode_languaget::convert_lazy_method( /// be called for each function call in `function_body`. static void notify_static_method_calls( const codet &function_body, - optionalt needed_lazy_methods) + std::optional needed_lazy_methods) { if(needed_lazy_methods) { @@ -1295,7 +1295,7 @@ static void notify_static_method_calls( bool java_bytecode_languaget::convert_single_method( const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &message_handler) { @@ -1354,7 +1354,7 @@ bool java_bytecode_languaget::convert_single_method( bool java_bytecode_languaget::convert_single_method_code( const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &message_handler) { diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 9bf89d5b0250..b2f7c95cbe35 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -229,7 +229,7 @@ struct java_bytecode_language_optionst /// JSON which contains initial values of static fields (right /// after the static initializer of the class was run). This is read from the /// file specified by the --static-values command-line option. - optionalt static_values_json; + std::optional static_values_json; /// List of classes to never load std::unordered_set no_load_classes; @@ -243,7 +243,7 @@ struct java_bytecode_language_optionst /// symbol (corresponding to the body of the method) will be replaced with the /// same kind of "return nondet null or instance of return type" body that we /// use for stubbed methods. The original method body will never be loaded. - optionalt method_context; + std::optional method_context; /// Should we lift clinit calls in function bodies to the top? For example, /// turning `if(x) A.clinit() else B.clinit()` into @@ -251,7 +251,7 @@ struct java_bytecode_language_optionst bool should_lift_clinit_calls; /// If set then a JAR file has been given via the -jar option. - optionalt main_jar; + std::optional main_jar; }; #define JAVA_CLASS_MODEL_SUFFIX "@class_model" @@ -349,27 +349,27 @@ class java_bytecode_languaget:public languaget convert_single_method( function_id, symbol_table, - optionalt(), + std::optional(), class_to_declared_symbols, message_handler); } bool convert_single_method( const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &); bool convert_single_method_code( const irep_idt &function_id, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, lazy_class_to_declared_symbols_mapt &class_to_declared_symbols, message_handlert &); bool do_ci_lazy_method_conversion(symbol_table_baset &, message_handlert &); const select_pointer_typet &get_pointer_type_selector() const; - optionalt language_options; + std::optional language_options; irep_idt main_class; std::vector main_jar_classes; java_class_loadert java_class_loader; diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp index cb593a66dbec..3aa3449e4c62 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp @@ -90,8 +90,8 @@ void java_bytecode_parse_treet::annotationt::element_value_pairt::output( /// \param annotation_type_name: An irep_idt representing the name of the /// annotation class, e.g. java::java.lang.SuppressWarnings /// \return The first annotation with the given name in annotations if one -/// exists, an empty optionalt otherwise. -optionalt +/// exists, an empty std::optional otherwise. +std::optional java_bytecode_parse_treet::find_annotation( const annotationst &annotations, const irep_idt &annotation_type_name) diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h index 5d649009c1ad..0af9819055c6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h +++ b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include "bytecode_info.h" @@ -48,7 +47,7 @@ struct java_bytecode_parse_treet typedef std::vector annotationst; - static optionalt find_annotation( + static std::optional find_annotation( const annotationst &annotations, const irep_idt &annotation_type_name); @@ -64,7 +63,7 @@ struct java_bytecode_parse_treet struct membert { std::string descriptor; - optionalt signature; + std::optional signature; irep_idt name; bool is_public, is_protected, is_private, is_static, is_final; annotationst annotations; @@ -127,7 +126,7 @@ struct java_bytecode_parse_treet { irep_idt name; std::string descriptor; - optionalt signature; + std::optional signature; std::size_t index; std::size_t start_pc; std::size_t length; @@ -228,7 +227,7 @@ struct java_bytecode_parse_treet struct lambda_method_handlet { java_class_typet::method_handle_kindt handle_type; - optionalt method_descriptor; + std::optional method_descriptor; /// Construct a lambda method handle with parameters \p params. lambda_method_handlet( @@ -273,7 +272,7 @@ struct java_bytecode_parse_treet typedef std::list implementst; implementst implements; - optionalt signature; + std::optional signature; typedef std::list fieldst; typedef std::list methodst; fieldst fields; diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index c99928326099..b7e02ddd8596 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -109,7 +109,7 @@ class java_bytecode_parsert final : public parsert void get_annotation_class_refs(const std::vector &annotations); void get_annotation_value_class_refs(const exprt &value); void parse_local_variable_type_table(methodt &method); - optionalt + std::optional parse_method_handle(const class method_handle_infot &entry); void read_bootstrapmethods_entry(); @@ -1803,7 +1803,7 @@ void java_bytecode_parsert::rmethod() rmethod_attribute(method); } -optionalt java_bytecode_parse( +std::optional java_bytecode_parse( std::istream &istream, const irep_idt &class_name, message_handlert &message_handler, @@ -1825,7 +1825,7 @@ optionalt java_bytecode_parse( return std::move(java_bytecode_parser.parse_tree); } -optionalt java_bytecode_parse( +std::optional java_bytecode_parse( const std::string &file, const irep_idt &class_name, message_handlert &message_handler, @@ -1914,7 +1914,7 @@ static java_class_typet::method_handle_kindt get_method_handle_type( /// \param entry: the constant pool entry of the methodhandle_info structure /// \return the method_handle type of the methodhandle_structure, /// either for a recognized bootstrap method or for a lambda function -optionalt +std::optional java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry) { const std::function pool_entry_lambda = @@ -2071,7 +2071,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry() } log.debug() << "INFO: parse lambda handle" << messaget::eom; - optionalt lambda_method_handle = + std::optional lambda_method_handle = parse_method_handle(method_handle_infot{method_handle_argument}); if(!lambda_method_handle.has_value()) diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.h b/jbmc/src/java_bytecode/java_bytecode_parser.h index af456ffba3d3..99c4e013b3df 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.h +++ b/jbmc/src/java_bytecode/java_bytecode_parser.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include struct java_bytecode_parse_treet; @@ -23,8 +22,8 @@ struct java_bytecode_parse_treet; /// \param msg: handles log messages /// \param skip_instructions: if true, the loaded class's methods will all be /// empty. Saves time and memory for consumers that only want signature info. -/// \return parse tree, or empty optionalt on failure -optionalt java_bytecode_parse( +/// \return parse tree, or empty std::optional on failure +std::optional java_bytecode_parse( const std::string &file, const irep_idt &class_name, class message_handlert &msg, @@ -36,8 +35,8 @@ optionalt java_bytecode_parse( /// \param msg: handles log messages /// \param skip_instructions: if true, the loaded class's methods will all be /// empty. Saves time and memory for consumers that only want signature info. -/// \return parse tree, or empty optionalt on failure -optionalt java_bytecode_parse( +/// \return parse tree, or empty std::optional on failure +std::optional java_bytecode_parse( std::istream &stream, const irep_idt &class_name, class message_handlert &msg, diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 11eb97cba65f..19b0c698d319 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -228,7 +228,7 @@ std::vector java_class_loadert::load_entire_jar( return *classes; } -optionalt> java_class_loadert::read_jar_file( +std::optional> java_class_loadert::read_jar_file( const std::string &jar_path, message_handlert &message_handler) { diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index 1c7c7c14df63..163cc1df220d 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -105,7 +105,7 @@ class java_class_loadert : public java_class_loader_baset /// Map from class names to the bytecode parse trees parse_tree_with_overridest_mapt class_map; - optionalt> + std::optional> read_jar_file(const std::string &jar_path, message_handlert &); }; diff --git a/jbmc/src/java_bytecode/java_class_loader_base.cpp b/jbmc/src/java_bytecode/java_class_loader_base.cpp index 5a998bc4d636..49c56cf27fbd 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.cpp +++ b/jbmc/src/java_bytecode/java_class_loader_base.cpp @@ -132,7 +132,7 @@ java_class_loader_baset::class_name_to_os_file(const irep_idt &class_name) } /// attempt to load a class from a classpath_entry -optionalt java_class_loader_baset::load_class( +std::optional java_class_loader_baset::load_class( const irep_idt &class_name, const classpath_entryt &cp_entry, message_handlert &message_handler) @@ -154,7 +154,7 @@ optionalt java_class_loader_baset::load_class( /// \param jar_file: path of the jar file /// \param message_handler: message handler /// \return optional value of parse tree, empty if class cannot be loaded -optionalt +std::optional java_class_loader_baset::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, @@ -189,7 +189,7 @@ java_class_loader_baset::get_class_from_jar( /// \param path: directory to load from /// \param message_handler: message handler /// \return optional value of parse tree, empty if class cannot be loaded -optionalt +std::optional java_class_loader_baset::get_class_from_directory( const irep_idt &class_name, const std::string &path, diff --git a/jbmc/src/java_bytecode/java_class_loader_base.h b/jbmc/src/java_bytecode/java_class_loader_base.h index 967b19d2bbc6..5ae4874a6bc9 100644 --- a/jbmc/src/java_bytecode/java_class_loader_base.h +++ b/jbmc/src/java_bytecode/java_class_loader_base.h @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_BASE_H #include -#include #include "jar_pool.h" @@ -58,19 +57,19 @@ class java_class_loader_baset std::list classpath_entries; /// attempt to load a class from a classpath_entry - optionalt load_class( + std::optional load_class( const irep_idt &class_name, const classpath_entryt &, message_handlert &); /// attempt to load a class from a given jar file - optionalt get_class_from_jar( + std::optional get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, message_handlert &); /// attempt to load a class from a given directory - optionalt get_class_from_directory( + std::optional get_class_from_directory( const irep_idt &class_name, const std::string &path, message_handlert &); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 86c463480bc5..fa074554c8e5 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -32,7 +32,7 @@ Author: Daniel Kroening, kroening@kroening.com #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V" -static optionalt record_return_value( +static std::optional record_return_value( const symbolt &function, const symbol_table_baset &symbol_table); @@ -493,7 +493,7 @@ static code_blockt java_record_outputs( return init_code; } -static optionalt record_return_value( +static std::optional record_return_value( const symbolt &function, const symbol_table_baset &symbol_table) { diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 87faebded0e1..b824caefcbc9 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -100,7 +100,7 @@ class java_object_factoryt bool is_sub, bool skip_classid, lifetimet lifetime, - const optionalt &override_type, + const std::optional &override_type, size_t depth, update_in_placet, const source_locationt &location); @@ -910,7 +910,7 @@ void java_object_factoryt::gen_nondet_struct_init( // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ resolve_inherited_componentt resolve_inherited_component{symbol_table}; - optionalt + std::optional cprover_nondet_initialize = resolve_inherited_component( "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true); @@ -1002,7 +1002,7 @@ void java_object_factoryt::gen_nondet_init( bool is_sub, bool skip_classid, lifetimet lifetime, - const optionalt &override_type, + const std::optional &override_type, size_t depth, update_in_placet update_in_place, const source_locationt &location) diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index e107ea9e4d5d..fad44b659581 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -782,7 +782,7 @@ class_to_declared_symbols(const symbol_table_baset &symbol_table) for(const auto &symbol_pair : symbol_table) { const symbolt &symbol = symbol_pair.second; - if(optionalt declaring = declaring_class(symbol)) + if(std::optional declaring = declaring_class(symbol)) result.emplace(*declaring, symbol); } return result; @@ -792,7 +792,7 @@ code_blockt get_user_specified_clinit_body( const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, size_t max_user_array_length, std::unordered_map &references, const std::unordered_multimap diff --git a/jbmc/src/java_bytecode/java_static_initializers.h b/jbmc/src/java_bytecode/java_static_initializers.h index 1f0dba5c955a..3e2286bc3b94 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.h +++ b/jbmc/src/java_bytecode/java_static_initializers.h @@ -86,7 +86,7 @@ code_blockt get_user_specified_clinit_body( const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, - optionalt needed_lazy_methods, + std::optional needed_lazy_methods, size_t max_user_array_length, std::unordered_map &references, const std::unordered_multimap diff --git a/jbmc/src/java_bytecode/java_trace_validation.cpp b/jbmc/src/java_bytecode/java_trace_validation.cpp index 519d57f5fa75..2680c4c12760 100644 --- a/jbmc/src/java_bytecode/java_trace_validation.cpp +++ b/jbmc/src/java_bytecode/java_trace_validation.cpp @@ -36,7 +36,7 @@ static bool may_be_lvalue(const exprt &expr) can_cast_expr(expr); } -optionalt get_inner_symbol_expr(exprt expr) +std::optional get_inner_symbol_expr(exprt expr) { while(expr.has_operands()) { diff --git a/jbmc/src/java_bytecode/java_trace_validation.h b/jbmc/src/java_bytecode/java_trace_validation.h index 7b0b5b8935bf..0f4cef9450f5 100644 --- a/jbmc/src/java_bytecode/java_trace_validation.h +++ b/jbmc/src/java_bytecode/java_trace_validation.h @@ -9,9 +9,10 @@ Author: Jeannie Moulton #ifndef CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H #define CPROVER_JAVA_BYTECODE_JAVA_TRACE_VALIDATION_H -#include #include +#include + class goto_tracet; class namespacet; class exprt; @@ -49,7 +50,7 @@ bool check_symbol_structure(const exprt &expr); /// Recursively extracts the first operand of an expression until it reaches a /// symbol and returns it, or returns an empty optional -optionalt get_inner_symbol_expr(exprt expr); +std::optional get_inner_symbol_expr(exprt expr); /// \return true iff the expression is a member expression (or nested member /// expression) of a valid symbol diff --git a/jbmc/src/java_bytecode/java_types.cpp b/jbmc/src/java_bytecode/java_types.cpp index 6793d6cb5ff0..b5d7557a204a 100644 --- a/jbmc/src/java_bytecode/java_types.cpp +++ b/jbmc/src/java_bytecode/java_types.cpp @@ -558,7 +558,7 @@ java_reference_typet java_reference_array_type(const struct_tag_typet &subtype) /// \param class_name_prefix: name of class to append to generic type /// variables/parameters /// \return internal type representation for GOTO programs -optionalt java_type_from_string( +std::optional java_type_from_string( const std::string &src, const std::string &class_name_prefix) { @@ -1072,7 +1072,7 @@ java_generic_struct_tag_typet::java_generic_struct_tag_typet( /// in the vector of generic types. /// \param type: The parameter type we are looking for. /// \return The index of the type in the vector of generic types. -optionalt java_generic_struct_tag_typet::generic_type_index( +std::optional java_generic_struct_tag_typet::generic_type_index( const java_generic_parametert &type) const { const auto &type_variable = type.get_name(); diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 5c38043c7014..b1e2c1a4306a 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include class java_annotationt : public irept @@ -672,7 +671,7 @@ exprt get_array_dimension_field(const exprt &pointer); exprt get_array_element_type_field(const exprt &pointer); typet java_type_from_char(char t); -optionalt java_type_from_string( +std::optional java_type_from_string( const std::string &, const std::string &class_name_prefix = ""); char java_char_from_type(const typet &type); @@ -880,7 +879,7 @@ class java_generic_struct_tag_typet : public struct_tag_typet return (generic_typest &)(add(ID_generic_types).get_sub()); } - optionalt + std::optional generic_type_index(const java_generic_parametert &type) const; }; @@ -1138,9 +1137,9 @@ class unsupported_java_class_signature_exceptiont:public std::logic_error } }; -inline optionalt java_type_from_string_with_exception( +inline std::optional java_type_from_string_with_exception( const std::string &descriptor, - const optionalt &signature, + const std::optional &signature, const std::string &class_name) { try @@ -1157,7 +1156,7 @@ inline optionalt java_type_from_string_with_exception( /// \param gen_types: The subtypes array. /// \param identifier: The string identifier of the type of the component. /// \return Optional with the size if the identifier was found. -inline const optionalt java_generics_get_index_for_subtype( +inline const std::optional java_generics_get_index_for_subtype( const std::vector &gen_types, const irep_idt &identifier) { diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 7f16b087364d..dcd5cc868498 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -445,7 +445,7 @@ std::string pretty_print_java_type(const std::string &fqn_java_type) /// ancestors including interfaces, rather than just parents. /// \return the concrete component referred to if any is found, or an invalid /// resolve_inherited_componentt::inherited_componentt otherwise. -optionalt +std::optional get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, @@ -566,10 +566,10 @@ symbolt &fresh_java_symbol( type, name_prefix, basename_prefix, source_location, ID_java, symbol_table); } -optionalt declaring_class(const symbolt &symbol) +std::optional declaring_class(const symbolt &symbol) { const irep_idt &class_id = symbol.type.get(ID_C_class); - return class_id.empty() ? optionalt{} : class_id; + return class_id.empty() ? std::optional{} : class_id; } void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class) @@ -577,7 +577,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class) symbol.type.set(ID_C_class, declaring_class); } -[[nodiscard]] optionalt +[[nodiscard]] std::optional class_name_from_method_name(const std::string &method_name) { const auto signature_index = method_name.rfind(":"); diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 1e23021188e9..c07e2a716aa9 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -153,7 +153,7 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip); std::string pretty_print_java_type(const std::string &fqn_java_type); -optionalt +std::optional get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, @@ -175,7 +175,7 @@ symbolt &fresh_java_symbol( /// symbol is not declared by a class then an empty optional is returned. This /// is used for method symbols and static field symbols to link them back to the /// class which declared them. -optionalt declaring_class(const symbolt &symbol); +std::optional declaring_class(const symbolt &symbol); /// Sets the identifier of the class which declared a given \p symbol to \p /// declaring_class. @@ -184,7 +184,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class); /// Get JVM type name of the class in which \p method_name is defined. /// Returns an empty optional if the class name cannot be retrieved, /// e.g. method_name is an internal function. -[[nodiscard]] optionalt +[[nodiscard]] std::optional class_name_from_method_name(const std::string &method_name); #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index 17975e12ff65..559acb80b044 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -51,7 +51,7 @@ irep_idt lambda_synthetic_class_name( /// methods) of the class where the lambda is called /// \param index: Index of the lambda method handle in the vector /// \return Symbol of the lambda method if the method handle has a known type -static optionalt +static std::optional get_lambda_method_handle( const symbol_table_baset &symbol_table, const java_class_typet::java_lambda_method_handlest &lambda_method_handles, @@ -73,7 +73,7 @@ get_lambda_method_handle( return {}; } -static optionalt +static std::optional lambda_method_handle( const symbol_table_baset &symbol_table, const irep_idt &method_identifier, @@ -605,7 +605,7 @@ static symbol_exprt instantiate_new_object( /// If \p maybe_boxed_type is a boxed primitive return its unboxing method; /// otherwise return empty. -static optionalt +static std::optional get_unboxing_method(const pointer_typet &maybe_boxed_type) { const irep_idt &boxed_type_id = @@ -613,7 +613,7 @@ get_unboxing_method(const pointer_typet &maybe_boxed_type) const java_boxed_type_infot *boxed_type_info = get_boxed_type_info_by_name(boxed_type_id); return boxed_type_info ? boxed_type_info->unboxing_function_name - : optionalt{}; + : std::optional{}; } /// Produce a class_method_descriptor_exprt or symbol_exprt for diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index 154d3133d976..c6bceb4fd723 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -42,7 +42,7 @@ pointer_typet select_pointer_typet::specialize_generics( generic_parameter_specialization_map; while(true) { - const optionalt specialization = + const std::optional specialization = spec_map_copy.pop(parameter_name); if(!specialization) { diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index a7264b9dd5b0..80a11dc1b522 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -135,7 +135,7 @@ class jbmc_parse_optionst : public parse_options_baset /// See java_bytecode_languaget::method_context. /// The two fields are initialized in exactly the same way. /// TODO Refactor this so it only needs to be computed once, in one place. - optionalt method_context; + std::optional method_context; }; #endif // CPROVER_JBMC_JBMC_PARSE_OPTIONS_H diff --git a/jbmc/src/jdiff/java_syntactic_diff.cpp b/jbmc/src/jdiff/java_syntactic_diff.cpp index 8b4f6473b938..0a9d429a7d83 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.cpp +++ b/jbmc/src/jdiff/java_syntactic_diff.cpp @@ -36,7 +36,7 @@ bool java_syntactic_difft::operator()() CHECK_RETURN(fun1 != nullptr); const symbolt *fun2 = goto_model2.symbol_table.lookup(gf_entry.first); CHECK_RETURN(fun2 != nullptr); - const optionalt class_name = declaring_class(*fun1); + const std::optional class_name = declaring_class(*fun1); bool function_access_changed = fun1->type.get(ID_access) != fun2->type.get(ID_access); bool class_access_changed = false; diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index fbae94a8d81a..81248f7b8e8a 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -71,7 +71,7 @@ require_goto_statements::pointer_assignment_locationt require_goto_statements::find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &component_name, const symbol_table_baset &symbol_table) { @@ -383,10 +383,10 @@ get_ultimate_source_symbol( /// `require_struct_component_assignment`. const irep_idt &require_goto_statements::require_struct_component_assignment( const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &component_name, const irep_idt &component_type_name, - const optionalt &typecast_name, + const std::optional &typecast_name, const std::vector &entry_point_instructions, const symbol_table_baset &symbol_table) { @@ -445,7 +445,7 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( const irep_idt & require_goto_statements::require_struct_array_component_assignment( const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &array_component_name, const irep_idt &array_type_name, const std::vector &entry_point_instructions, diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.h b/jbmc/unit/java-testing-utils/require_goto_statements.h index 33f3dd744a78..ebd78d9d7e4d 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.h +++ b/jbmc/unit/java-testing-utils/require_goto_statements.h @@ -23,7 +23,7 @@ namespace require_goto_statements { struct pointer_assignment_locationt { - optionalt null_assignment; + std::optional null_assignment; std::vector non_null_assignments; }; @@ -47,7 +47,7 @@ class no_decl_found_exceptiont : public std::exception pointer_assignment_locationt find_struct_component_assignments( const std::vector &statements, const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &component_name, const symbol_table_baset &symbol_table); @@ -74,16 +74,16 @@ const code_declt &require_declaration_of_name( const irep_idt &require_struct_component_assignment( const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &component_name, const irep_idt &component_type_name, - const optionalt &typecast_name, + const std::optional &typecast_name, const std::vector &entry_point_instructions, const symbol_table_baset &symbol_table); const irep_idt &require_struct_array_component_assignment( const irep_idt &structure_name, - const optionalt &superclass_name, + const std::optional &superclass_name, const irep_idt &array_component_name, const irep_idt &array_type_name, const std::vector &entry_point_instructions, diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index c76486757652..4559d4348c5e 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -17,7 +17,7 @@ Author: Diffblue Ltd. /// \return A cast to pointer_typet version of type pointer_typet require_type::require_pointer( const typet &type, - const optionalt &subtype) + const std::optional &subtype) { REQUIRE(type.id() == ID_pointer); const pointer_typet &pointer = to_pointer_type(type); @@ -243,7 +243,7 @@ java_generic_parametert require_type::require_java_generic_parameter( /// \return The value passed in the first argument const typet &require_type::require_java_non_generic_type( const typet &type, - const optionalt &expect_subtype) + const std::optional &expect_subtype) { REQUIRE(!is_java_generic_parameter(type)); REQUIRE(!is_java_generic_type(type)); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index d9e5135bc138..513593fb7ccf 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -22,7 +22,7 @@ Author: Diffblue Ltd. namespace require_type { pointer_typet -require_pointer(const typet &type, const optionalt &subtype); +require_pointer(const typet &type, const std::optional &subtype); const struct_tag_typet & require_struct_tag(const typet &type, const irep_idt &identifier = ""); @@ -78,7 +78,7 @@ java_generic_parametert require_java_generic_parameter( const typet &require_java_non_generic_type( const typet &type, - const optionalt &expect_subtype); + const std::optional &expect_subtype); class_typet require_complete_class(const typet &class_type); diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp index 41e422dea175..50710153209f 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp @@ -28,7 +28,7 @@ SCENARIO( GIVEN( "A class with a static lambda variables from " + compiler + " compiler.") { - optionalt parse_tree = java_bytecode_parse( + std::optional parse_tree = java_bytecode_parse( "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + compiler + "_classes/StaticLambdas.class", "StaticLambdas", @@ -351,11 +351,12 @@ SCENARIO( [](const std::string &compiler) { // NOLINT(whitespace/braces) GIVEN("A method with local lambdas from " + compiler + " compiler.") { - optionalt parse_tree = java_bytecode_parse( - "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + - compiler + "_classes/LocalLambdas.class", - "LocalLambdas", - null_message_handler); + std::optional parse_tree = + java_bytecode_parse( + "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + + compiler + "_classes/LocalLambdas.class", + "LocalLambdas", + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); @@ -672,11 +673,12 @@ SCENARIO( "A class that has lambdas as member variables from " + compiler + " compiler.") { - optionalt parse_tree = java_bytecode_parse( - "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + - compiler + "_classes/MemberLambdas.class", - "MemberLambdas", - null_message_handler); + std::optional parse_tree = + java_bytecode_parse( + "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + + compiler + "_classes/MemberLambdas.class", + "MemberLambdas", + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); @@ -1019,11 +1021,12 @@ SCENARIO( "variables from " + compiler + " compiler.") { - optionalt parse_tree = java_bytecode_parse( - "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + - compiler + "_classes/OuterMemberLambdas$Inner.class", - "OuterMemberLambdas$Inner", - null_message_handler); + std::optional parse_tree = + java_bytecode_parse( + "./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/" + + compiler + "_classes/OuterMemberLambdas$Inner.class", + "OuterMemberLambdas$Inner", + null_message_handler); WHEN("Parsing that class") { REQUIRE(parse_tree); diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp index 55afffa9084c..15598ef8e7b9 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp @@ -91,7 +91,7 @@ SCENARIO( const reference_typet test_class_type = reference_type(struct_tag_typet{"java::TestClass"}); - optionalt option{}; + std::optional option{}; const code_with_references_listt code = assign_from_json( symbol_exprt{"symbol_to_assign", test_class_type}, json, @@ -180,7 +180,7 @@ SCENARIO( const reference_typet test_class_type = reference_type(struct_tag_typet{"java::TestClass"}); - optionalt option{}; + std::optional option{}; const code_with_references_listt code = assign_from_json( symbol_exprt{"symbol_to_assign", test_class_type}, json, @@ -303,7 +303,7 @@ SCENARIO( const reference_typet test_class_type = reference_type(struct_tag_typet{"java::TestClass"}); - optionalt option{}; + std::optional option{}; const code_with_references_listt code = assign_from_json( symbol_exprt{"symbol_to_assign", test_class_type}, json, @@ -467,7 +467,7 @@ SCENARIO( const reference_typet test_class_type = reference_type(struct_tag_typet{"java::TestClass"}); - optionalt option{}; + std::optional option{}; const code_with_references_listt code = assign_from_json( symbol_exprt{"symbol_to_assign", test_class_type}, json, diff --git a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp index 40b9ffef565f..44464c46b2d2 100644 --- a/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/strings/string_refinement/dependency_graph.cpp @@ -82,13 +82,13 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]") symbol_generatort generator; array_poolt array_pool(generator); - optionalt new_equation1 = + std::optional new_equation1 = add_node(dependencies, equation1, array_pool, generator); REQUIRE(new_equation1.has_value()); - optionalt new_equation2 = + std::optional new_equation2 = add_node(dependencies, equation2, array_pool, generator); REQUIRE(new_equation2.has_value()); - optionalt new_equation3 = + std::optional new_equation3 = add_node(dependencies, equation3, array_pool, generator); REQUIRE(new_equation3.has_value()); diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp index 93278523c02f..543e68302a44 100644 --- a/src/analyses/call_graph.cpp +++ b/src/analyses/call_graph.cpp @@ -296,12 +296,12 @@ void call_grapht::output_xml(std::ostream &out) const } } -optionalt call_grapht::directed_grapht::get_node_index( - const irep_idt &function) const +std::optional +call_grapht::directed_grapht::get_node_index(const irep_idt &function) const { auto findit=nodes_by_name.find(function); if(findit==nodes_by_name.end()) - return optionalt(); + return std::optional(); else return findit->second; } diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h index 8abdbc13bf94..630f277f306e 100644 --- a/src/analyses/call_graph.h +++ b/src/analyses/call_graph.h @@ -147,7 +147,7 @@ class call_grapht /// Find the graph node by function name /// \param function: function to find /// \return none if function is not in this graph, or some index otherwise. - optionalt get_node_index(const irep_idt &function) const; + std::optional get_node_index(const irep_idt &function) const; /// Type of the node name -> node index map. typedef std::unordered_map nodes_by_namet; diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index a7fe27f985f5..a67816bce45c 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -32,8 +32,8 @@ struct goto_null_checkt /// \param expr: expression to check /// \return a `goto_null_checkt` indicating what expression is tested and /// whether the check applies on the taken or not-taken branch, or an empty -/// optionalt if this isn't a null check. -static optionalt get_null_checked_expr(const exprt &expr) +/// std::optional if this isn't a null check. +static std::optional get_null_checked_expr(const exprt &expr) { exprt normalized_expr = expr; // If true, then a null check is made when test `expr` passes; if false, diff --git a/src/analyses/sese_regions.cpp b/src/analyses/sese_regions.cpp index 727e0819ea3f..240d56678453 100644 --- a/src/analyses/sese_regions.cpp +++ b/src/analyses/sese_regions.cpp @@ -146,7 +146,7 @@ void sese_region_analysist::compute_sese_regions( // but our current dominator analysis doesn't make it easy to determine an // immediate dominator. - // Ideally I would use `optionalt` here, but it triggers a + // Ideally I would use `std::optional` here, but it triggers a // GCC-5 bug. std::size_t closest_exit_index = dominators.cfg.size(); for(const auto &possible_exit : instruction_postdoms) diff --git a/src/analyses/sese_regions.h b/src/analyses/sese_regions.h index 563bd0add05c..52e882d1a67c 100644 --- a/src/analyses/sese_regions.h +++ b/src/analyses/sese_regions.h @@ -12,13 +12,11 @@ Author: Diffblue Ltd. #ifndef CPROVER_ANALYSES_SESE_REGIONS_H #define CPROVER_ANALYSES_SESE_REGIONS_H -#include - class sese_region_analysist { public: void operator()(const goto_programt &goto_program); - optionalt + std::optional get_region_exit(goto_programt::const_targett entry) const { auto find_result = sese_regions.find(entry); diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 5f3c6affb4f7..51f738c51091 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -117,7 +117,8 @@ interval_from_x_ge_value(const exprt &value) static inline mp_integer force_value_from_expr(const exprt &value) { PRECONDITION(constant_interval_exprt::is_int(value.type())); - optionalt maybe_integer_value = numeric_cast(value); + std::optional maybe_integer_value = + numeric_cast(value); INVARIANT(maybe_integer_value.has_value(), "Input has to have a value"); return maybe_integer_value.value(); } diff --git a/src/analyses/variable-sensitivity/liveness_context.h b/src/analyses/variable-sensitivity/liveness_context.h index c15808cd98a4..ff32786d6482 100644 --- a/src/analyses/variable-sensitivity/liveness_context.h +++ b/src/analyses/variable-sensitivity/liveness_context.h @@ -83,7 +83,7 @@ class liveness_contextt : public write_location_contextt abstract_object_pointert reset_location_on_merge(const liveness_context_ptrt &merged) const; - optionalt assign_location; + std::optional assign_location; context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override; diff --git a/src/ansi-c/c_expr.cpp b/src/ansi-c/c_expr.cpp index 92cec4044f2f..a763f0fb5507 100644 --- a/src/ansi-c/c_expr.cpp +++ b/src/ansi-c/c_expr.cpp @@ -15,7 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com shuffle_vector_exprt::shuffle_vector_exprt( exprt vector1, - optionalt vector2, + std::optional vector2, exprt::operandst indices) : multi_ary_exprt( ID_shuffle_vector, diff --git a/src/ansi-c/c_expr.h b/src/ansi-c/c_expr.h index 55b820cc60ff..13a7ceca4eb3 100644 --- a/src/ansi-c/c_expr.h +++ b/src/ansi-c/c_expr.h @@ -21,7 +21,7 @@ class shuffle_vector_exprt : public multi_ary_exprt public: shuffle_vector_exprt( exprt vector1, - optionalt vector2, + std::optional vector2, exprt::operandst indices); const vector_typet &type() const diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index fe7ea79939d6..10547403f5a2 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -775,7 +775,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type) } } -optionalt +std::optional c_typecastt::check_address_can_be_taken(const typet &type) { if(type.id() == ID_c_bit_field) diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h index 3416677a515f..9585d99b7cb0 100644 --- a/src/ansi-c/c_typecast.h +++ b/src/ansi-c/c_typecast.h @@ -10,9 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_C_TYPECAST_H #define CPROVER_ANSI_C_C_TYPECAST_H -#include - #include +#include #include class exprt; @@ -69,7 +68,7 @@ class c_typecastt /// \return empty when address can be taken, /// error message otherwise - static optionalt check_address_can_be_taken(const typet &); + static std::optional check_address_can_be_taken(const typet &); protected: const namespacet &ns; diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index d413f0dcf8cc..bbe4948376e0 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -228,14 +228,14 @@ class c_typecheck_baset: const irep_idt &arith_op); exprt typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr); - virtual optionalt typecheck_gcc_polymorphic_builtin( + virtual std::optional typecheck_gcc_polymorphic_builtin( const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location); virtual code_blockt instantiate_gcc_polymorphic_builtin( const irep_idt &identifier, const symbol_exprt &function_symbol); - virtual optionalt + virtual std::optional typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr); virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr); diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index 40bb18332f60..162daad11d81 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -490,7 +490,8 @@ static symbol_exprt typecheck_atomic_fetch_op( return result; } -optionalt c_typecheck_baset::typecheck_gcc_polymorphic_builtin( +std::optional +c_typecheck_baset::typecheck_gcc_polymorphic_builtin( const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location) @@ -1420,7 +1421,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector( const exprt &arg0 = arguments[0]; const vector_typet &input_vec_type = to_vector_type(arg0.type()); - optionalt arg1; + std::optional arg1; if(arguments.size() == 3) { if(arguments[1].type() != input_vec_type) diff --git a/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp b/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp index 4e1915a68734..26667aca9dfb 100644 --- a/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp +++ b/src/ansi-c/c_typecheck_shadow_memory_builtin.cpp @@ -223,7 +223,7 @@ static symbol_exprt typecheck_set_field( /// Typecheck the function if it is a shadow_memory builtin and return a symbol /// for it. Otherwise return empty. -optionalt c_typecheck_baset::typecheck_shadow_memory_builtin( +std::optional c_typecheck_baset::typecheck_shadow_memory_builtin( const side_effect_expr_function_callt &expr) { const exprt &f_op = expr.function(); diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index dcf84fcfdde6..1175ed6b04b5 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1719,7 +1719,7 @@ std::string expr2ct::convert_object_descriptor( return result; } -static optionalt +static std::optional build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) { const typet &type = static_cast(expr.find(ID_C_c_sizeof_type)); @@ -1728,7 +1728,7 @@ build_sizeof_expr(const constant_exprt &expr, const namespacet &ns) return {}; const auto type_size_expr = size_of_expr(type, ns); - optionalt type_size; + std::optional type_size; if(type_size_expr.has_value()) type_size = numeric_cast(*type_size_expr); auto val = numeric_cast(expr); @@ -4066,7 +4066,7 @@ std::string expr2ct::convert_with_precedence( return convert_norep(src, precedence); } -optionalt expr2ct::convert_function(const exprt &src) +std::optional expr2ct::convert_function(const exprt &src) { static const std::map function_names = { {"buffer_size", "BUFFER_SIZE"}, diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 07d73975a3f2..6ede63b7c2bc 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -185,7 +185,7 @@ class expr2ct /// Returns a string if \p src is a function with a known conversion, else /// returns nullopt. - optionalt convert_function(const exprt &src); + std::optional convert_function(const exprt &src); std::string convert_function(const exprt &src, const std::string &symbol); std::string convert_complex( diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 59915865a0be..a05a9953b171 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -213,7 +213,7 @@ class goto_check_ct /// checking bool requires_pointer_primitive_check(const exprt &expr); - optionalt + std::optional get_pointer_is_null_condition(const exprt &address, const exprt &size); conditionst get_pointer_points_to_valid_memory_conditions( const exprt &address, @@ -322,7 +322,7 @@ class goto_check_ct } check_statust; /// optional (named-check, status) pair - using named_check_statust = optionalt>; + using named_check_statust = std::optional>; /// Matches a named-check string of the form /// @@ -2343,7 +2343,7 @@ goto_check_ct::get_pointer_points_to_valid_memory_conditions( return conditions; } -optionalt +std::optional goto_check_ct::get_pointer_is_null_condition( const exprt &address, const exprt &size) diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index a7b4f21d4e07..d7996e6d8315 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -101,7 +101,7 @@ mp_integer alignment(const typet &type, const namespacet &ns) return result; } -static optionalt +static std::optional underlying_width(const c_bit_field_typet &type, const namespacet &ns) { const typet &underlying_type = type.underlying_type(); diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 09e022073cd6..205ec052dd84 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -19,7 +19,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu /// \param object: non-typechecked object /// \param operands: non-typechecked operands /// \return typechecked code -optionalt cpp_typecheckt::cpp_constructor( +std::optional cpp_typecheckt::cpp_constructor( const source_locationt &source_location, const exprt &object, const exprt::operandst &operands) diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index d7f895f8bd1d..5f2ee3dbe16d 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -16,7 +16,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu #include /// \return typechecked code -optionalt cpp_typecheckt::cpp_destructor( +std::optional cpp_typecheckt::cpp_destructor( const source_locationt &source_location, const exprt &object) { diff --git a/src/cpp/cpp_typecheck.h b/src/cpp/cpp_typecheck.h index 7c625f4ba6df..814b3d8c13e3 100644 --- a/src/cpp/cpp_typecheck.h +++ b/src/cpp/cpp_typecheck.h @@ -98,7 +98,7 @@ class cpp_typecheckt:public c_typecheck_baset bool cpp_is_pod(const typet &type) const; - optionalt cpp_constructor( + std::optional cpp_constructor( const source_locationt &source_location, const exprt &object, const exprt::operandst &operands); @@ -430,7 +430,7 @@ class cpp_typecheckt:public c_typecheck_baset const struct_typet &this_struct_type(); - optionalt + std::optional cpp_destructor(const source_locationt &source_location, const exprt &object); // expressions diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp index 4e866b9fdd17..c16a92a6d12b 100644 --- a/src/cpp/parse.cpp +++ b/src/cpp/parse.cpp @@ -231,7 +231,7 @@ class Parser // NOLINT(readability/identifiers) bool rNullDeclaration(cpp_declarationt &); bool rTypedef(cpp_declarationt &); bool rTypedefUsing(cpp_declarationt &); - optionalt rTypedefStatement(); + std::optional rTypedefStatement(); bool rTypeSpecifier(typet &, bool); bool isTypeSpecifier(); bool rLinkageSpec(cpp_linkage_spect &); @@ -341,20 +341,20 @@ class Parser // NOLINT(readability/identifiers) bool maybeTemplateArgs(); bool rFunctionBody(cpp_declaratort &); - optionalt rCompoundStatement(); - optionalt rStatement(); - optionalt rIfStatement(); - optionalt rSwitchStatement(); - optionalt rWhileStatement(); - optionalt rDoStatement(); - optionalt rForStatement(); - optionalt rTryStatement(); - - optionalt rExprStatement(); - optionalt rDeclarationStatement(); - optionalt + std::optional rCompoundStatement(); + std::optional rStatement(); + std::optional rIfStatement(); + std::optional rSwitchStatement(); + std::optional rWhileStatement(); + std::optional rDoStatement(); + std::optional rForStatement(); + std::optional rTryStatement(); + + std::optional rExprStatement(); + std::optional rDeclarationStatement(); + std::optional rIntegralDeclStatement(cpp_storage_spect &, typet &, typet &); - optionalt rOtherDeclStatement(cpp_storage_spect &, typet &); + std::optional rOtherDeclStatement(cpp_storage_spect &, typet &); bool MaybeTypeNameOrClassTemplate(cpp_tokent &); void SkipTo(int token); @@ -363,13 +363,13 @@ class Parser // NOLINT(readability/identifiers) bool rString(cpp_tokent &tk); // GCC extensions - optionalt rGCCAsmStatement(); + std::optional rGCCAsmStatement(); // MSC extensions - optionalt rMSC_tryStatement(); - optionalt rMSC_leaveStatement(); - optionalt rMSCAsmStatement(); - optionalt rMSC_if_existsStatement(); + std::optional rMSC_tryStatement(); + std::optional rMSC_leaveStatement(); + std::optional rMSCAsmStatement(); + std::optional rMSC_if_existsStatement(); bool rTypePredicate(exprt &); bool rMSCuuidof(exprt &); bool rMSC_if_existsExpr(exprt &); @@ -680,7 +680,7 @@ bool Parser::rTypedefUsing(cpp_declarationt &declaration) return true; } -optionalt Parser::rTypedefStatement() +std::optional Parser::rTypedefStatement() { cpp_declarationt declaration; if(!rTypedef(declaration)) @@ -6573,7 +6573,7 @@ bool Parser::rMSC_if_existsExpr(exprt &expr) return true; } -optionalt Parser::rMSC_if_existsStatement() +std::optional Parser::rMSC_if_existsStatement() { cpp_tokent tk1; @@ -7235,7 +7235,7 @@ bool Parser::rFunctionBody(cpp_declaratort &declarator) compound.statement : '{' (statement)* '}' */ -optionalt Parser::rCompoundStatement() +std::optional Parser::rCompoundStatement() { cpp_tokent ob, cb; @@ -7296,7 +7296,7 @@ optionalt Parser::rCompoundStatement() | USING { NAMESPACE } identifier ';' | STATIC_ASSERT ( expression ',' expression ) ';' */ -optionalt Parser::rStatement() +std::optional Parser::rStatement() { cpp_tokent tk1, tk2, tk3; int k; @@ -7548,7 +7548,7 @@ optionalt Parser::rStatement() if.statement : IF '(' comma.expression ')' statement { ELSE statement } */ -optionalt Parser::rIfStatement() +std::optional Parser::rIfStatement() { cpp_tokent tk1, tk2, tk3, tk4; @@ -7595,7 +7595,7 @@ optionalt Parser::rIfStatement() switch.statement : SWITCH '(' comma.expression ')' statement */ -optionalt Parser::rSwitchStatement() +std::optional Parser::rSwitchStatement() { cpp_tokent tk1, tk2, tk3; @@ -7626,7 +7626,7 @@ optionalt Parser::rSwitchStatement() while.statement : WHILE '(' comma.expression ')' statement */ -optionalt Parser::rWhileStatement() +std::optional Parser::rWhileStatement() { cpp_tokent tk1, tk2, tk3; @@ -7657,7 +7657,7 @@ optionalt Parser::rWhileStatement() do.statement : DO statement WHILE '(' comma.expression ')' ';' */ -optionalt Parser::rDoStatement() +std::optional Parser::rDoStatement() { cpp_tokent tk0, tk1, tk2, tk3, tk4; @@ -7694,7 +7694,7 @@ optionalt Parser::rDoStatement() : FOR '(' expr.statement {comma.expression} ';' {comma.expression} ')' statement */ -optionalt Parser::rForStatement() +std::optional Parser::rForStatement() { cpp_tokent tk1, tk2, tk3, tk4; @@ -7751,7 +7751,7 @@ optionalt Parser::rForStatement() exception.handler : CATCH '(' (arg.declaration | Ellipsis) ')' compound.statement */ -optionalt Parser::rTryStatement() +std::optional Parser::rTryStatement() { cpp_tokent try_token; @@ -7777,7 +7777,7 @@ optionalt Parser::rTryStatement() if(lex.get_token(op_token)!='(') return {}; - optionalt catch_op; + std::optional catch_op; if(lex.LookAhead(0)==TOK_ELLIPSIS) { @@ -7827,7 +7827,7 @@ optionalt Parser::rTryStatement() return std::move(statement); } -optionalt Parser::rMSC_tryStatement() +std::optional Parser::rMSC_tryStatement() { // These are for 'structured exception handling', // and are a relic from Visual C. @@ -7889,7 +7889,7 @@ optionalt Parser::rMSC_tryStatement() return {}; } -optionalt Parser::rMSC_leaveStatement() +std::optional Parser::rMSC_leaveStatement() { // These are for 'structured exception handling', // and are a relic from Visual C. @@ -7905,7 +7905,7 @@ optionalt Parser::rMSC_leaveStatement() return std::move(statement); } -optionalt Parser::rGCCAsmStatement() +std::optional Parser::rGCCAsmStatement() { cpp_tokent tk; @@ -8004,7 +8004,7 @@ optionalt Parser::rGCCAsmStatement() return std::move(statement); } -optionalt Parser::rMSCAsmStatement() +std::optional Parser::rMSCAsmStatement() { cpp_tokent tk; @@ -8080,7 +8080,7 @@ optionalt Parser::rMSCAsmStatement() | openc++.postfix.expr | openc++.primary.exp */ -optionalt Parser::rExprStatement() +std::optional Parser::rExprStatement() { cpp_tokent tk; @@ -8191,7 +8191,7 @@ bool Parser::rCondition(exprt &statement) Note: if you modify this function, take a look at rDeclaration(), too. */ -optionalt Parser::rDeclarationStatement() +std::optional Parser::rDeclarationStatement() { cpp_storage_spect storage_spec; typet cv_q, integral; @@ -8261,7 +8261,7 @@ optionalt Parser::rDeclarationStatement() integral.decl.statement : decl.head integral.or.class.spec {cv.qualify} {declarators} ';' */ -optionalt Parser::rIntegralDeclStatement( +std::optional Parser::rIntegralDeclStatement( cpp_storage_spect &storage_spec, typet &integral, typet &cv_q) @@ -8304,7 +8304,7 @@ optionalt Parser::rIntegralDeclStatement( other.decl.statement :decl.head name {cv.qualify} declarators ';' */ -optionalt +std::optional Parser::rOtherDeclStatement(cpp_storage_spect &storage_spec, typet &cv_q) { typet type_name; diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index 1fe3acf7d442..6dc8a74b7497 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -161,7 +161,7 @@ bv_pointers_widet::bv_pointers_widet( { } -optionalt bv_pointers_widet::convert_address_of_rec(const exprt &expr) +std::optional bv_pointers_widet::convert_address_of_rec(const exprt &expr) { if(expr.id() == ID_symbol) { diff --git a/src/cprover/bv_pointers_wide.h b/src/cprover/bv_pointers_wide.h index 02f65e138971..1c1f0be60fb0 100644 --- a/src/cprover/bv_pointers_wide.h +++ b/src/cprover/bv_pointers_wide.h @@ -64,7 +64,7 @@ class bv_pointers_widet : public boolbvt exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override; - [[nodiscard]] optionalt convert_address_of_rec(const exprt &); + [[nodiscard]] std::optional convert_address_of_rec(const exprt &); [[nodiscard]] bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &); diff --git a/src/cprover/counterexample_found.cpp b/src/cprover/counterexample_found.cpp index ff488f82f6ac..40142d6a28b5 100644 --- a/src/cprover/counterexample_found.cpp +++ b/src/cprover/counterexample_found.cpp @@ -170,7 +170,7 @@ propertyt::tracet counterexample( return trace; } -optionalt counterexample_found( +std::optional counterexample_found( const std::vector &frames, const workt &work, const std::unordered_set &address_taken, diff --git a/src/cprover/counterexample_found.h b/src/cprover/counterexample_found.h index bd848f0ad2a3..5a7fe9e2d372 100644 --- a/src/cprover/counterexample_found.h +++ b/src/cprover/counterexample_found.h @@ -16,7 +16,7 @@ Author: Daniel Kroening, dkr@amazon.com #include -optionalt counterexample_found( +std::optional counterexample_found( const std::vector &, const workt &, const std::unordered_set &address_taken, diff --git a/src/cprover/cprover_parse_options.cpp b/src/cprover/cprover_parse_options.cpp index 977ac1186c7c..1bd9203bdb89 100644 --- a/src/cprover/cprover_parse_options.cpp +++ b/src/cprover/cprover_parse_options.cpp @@ -215,10 +215,10 @@ int cprover_parse_optionst::main() return CPROVER_EXIT_SUCCESS; } - // gcc produces a spurious warning for optionalt if initialised - // with ternary operator. Initialising with an immediately invoked lamda - // avoids this. - const auto contract = [&]() -> optionalt { + // gcc produces a spurious warning for std::optional if + // initialised with ternary operator. Initialising with an immediately + // invoked lambda avoids this. + const auto contract = [&]() -> std::optional { if(cmdline.isset("contract")) return {cmdline.get_value("contract")}; else diff --git a/src/cprover/inductiveness.h b/src/cprover/inductiveness.h index 3368d9fbbf7e..369966e27961 100644 --- a/src/cprover/inductiveness.h +++ b/src/cprover/inductiveness.h @@ -45,7 +45,7 @@ class inductiveness_resultt return result; } - optionalt work; + std::optional work; private: explicit inductiveness_resultt(outcomet __outcome) : outcome(__outcome) diff --git a/src/cprover/instrument_contracts.cpp b/src/cprover/instrument_contracts.cpp index ff6e71a6834c..b68b49681dd3 100644 --- a/src/cprover/instrument_contracts.cpp +++ b/src/cprover/instrument_contracts.cpp @@ -24,7 +24,7 @@ Author: Daniel Kroening, dkr@amazon.com #define MAX_TEXT 20 -optionalt +std::optional get_contract(const irep_idt &function_identifier, const namespacet &ns) { // contracts are in a separate symbol, with prefix "contract::" @@ -343,7 +343,7 @@ void instrument_contract_checks( { for(auto &instruction : body.instructions) instruction.transform( - [&old_prefix, &old_exprs](exprt expr) -> optionalt { + [&old_prefix, &old_exprs](exprt expr) -> std::optional { return replace_old(expr, old_prefix, old_exprs); }); } diff --git a/src/cprover/instrument_contracts.h b/src/cprover/instrument_contracts.h index f33f17c1c021..29b740ed14d3 100644 --- a/src/cprover/instrument_contracts.h +++ b/src/cprover/instrument_contracts.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_CPROVER_INSTRUMENT_CONTRACTS_H #include -#include class code_with_contract_typet; class goto_modelt; @@ -21,7 +20,7 @@ class namespacet; void instrument_contracts(goto_modelt &); -optionalt +std::optional get_contract(const irep_idt &function_identifier, const namespacet &); #endif // CPROVER_CPOVER_INSTRUMENT_CONTRACTS_H diff --git a/src/cprover/may_alias.cpp b/src/cprover/may_alias.cpp index 2dd005535f8e..b3cc69fb84dd 100644 --- a/src/cprover/may_alias.cpp +++ b/src/cprover/may_alias.cpp @@ -92,7 +92,7 @@ bool prefix_of(const typet &a, const typet &b, const namespacet &ns) return a_struct.is_prefix_of(b_struct) || b_struct.is_prefix_of(a_struct); } -static optionalt find_object(const exprt &expr) +static std::optional find_object(const exprt &expr) { if(expr.id() == ID_object_address) return to_object_address_expr(expr); @@ -145,7 +145,7 @@ static exprt drop_pointer_typecasts(exprt src) return src; } -optionalt +std::optional same_address(const exprt &a, const exprt &b, const namespacet &ns) { static const auto true_expr = true_exprt(); @@ -219,7 +219,7 @@ same_address(const exprt &a, const exprt &b, const namespacet &ns) return {}; } -optionalt may_alias( +std::optional may_alias( const exprt &a, const exprt &b, const std::unordered_set &address_taken, diff --git a/src/cprover/may_alias.h b/src/cprover/may_alias.h index feeee1c89c0a..11e8b29c4ac1 100644 --- a/src/cprover/may_alias.h +++ b/src/cprover/may_alias.h @@ -21,7 +21,7 @@ class namespacet; bool is_object_field_element(const exprt &); // check whether the given two addresses may be aliases -optionalt may_alias( +std::optional may_alias( const exprt &, const exprt &, const std::unordered_set &address_taken, diff --git a/src/cprover/report_traces.cpp b/src/cprover/report_traces.cpp index 9a96fd648dcb..09833323dbeb 100644 --- a/src/cprover/report_traces.cpp +++ b/src/cprover/report_traces.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, dkr@amazon.com #include -optionalt address_to_lvalue(exprt src) +std::optional address_to_lvalue(exprt src) { if(src.id() == ID_object_address) return to_object_address_expr(src).object_expr(); diff --git a/src/cprover/sentinel_dll.cpp b/src/cprover/sentinel_dll.cpp index 071e811bb0e8..1ae2eea45b2a 100644 --- a/src/cprover/sentinel_dll.cpp +++ b/src/cprover/sentinel_dll.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "state.h" -optionalt sentinel_dll_member( +std::optional sentinel_dll_member( const exprt &state, const exprt &node, bool next, // vs. prev @@ -69,13 +69,13 @@ optionalt sentinel_dll_member( return evaluate_exprt(state, field_address, component.type()); } -optionalt +std::optional sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &ns) { return sentinel_dll_member(state, node, true, ns); } -optionalt +std::optional sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &ns) { return sentinel_dll_member(state, node, false, ns); diff --git a/src/cprover/sentinel_dll.h b/src/cprover/sentinel_dll.h index 88331c6720da..8e5af2f8faf3 100644 --- a/src/cprover/sentinel_dll.h +++ b/src/cprover/sentinel_dll.h @@ -101,10 +101,10 @@ inline state_is_sentinel_dll_exprt &to_state_is_sentinel_dll_expr(exprt &expr) return ret; } -optionalt +std::optional sentinel_dll_next(const exprt &state, const exprt &node, const namespacet &); -optionalt +std::optional sentinel_dll_prev(const exprt &state, const exprt &node, const namespacet &); #endif // CPROVER_CPROVER_SENTINEL_DLL_H diff --git a/src/cprover/state_encoding.cpp b/src/cprover/state_encoding.cpp index 2ea684d7fae6..56ef744c049b 100644 --- a/src/cprover/state_encoding.cpp +++ b/src/cprover/state_encoding.cpp @@ -1116,7 +1116,7 @@ void state_encodingt::encode( void state_encoding( const goto_modelt &goto_model, bool program_is_inlined, - optionalt contract, + std::optional contract, encoding_targett &dest) { if(program_is_inlined) @@ -1179,7 +1179,7 @@ void state_encoding( const goto_modelt &goto_model, state_encoding_formatt state_encoding_format, bool program_is_inlined, - optionalt contract, + std::optional contract, std::ostream &out) { switch(state_encoding_format) @@ -1236,7 +1236,7 @@ void variable_encoding( solver_resultt state_encoding_solver( const goto_modelt &goto_model, bool program_is_inlined, - optionalt contract, + std::optional contract, const solver_optionst &solver_options) { const namespacet ns(goto_model.symbol_table); diff --git a/src/cprover/state_encoding.h b/src/cprover/state_encoding.h index 96ce2ba07420..aa74196b8056 100644 --- a/src/cprover/state_encoding.h +++ b/src/cprover/state_encoding.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_CPROVER_STATE_ENCODING_H #include -#include #include "solver.h" @@ -31,13 +30,13 @@ void state_encoding( const goto_modelt &, state_encoding_formatt, bool program_is_inlined, - optionalt contract, + std::optional contract, std::ostream &out); solver_resultt state_encoding_solver( const goto_modelt &, bool program_is_inlined, - optionalt contract, + std::optional contract, const solver_optionst &); void variable_encoding( diff --git a/src/crangler/c_defines.h b/src/crangler/c_defines.h index 3dc34ba435a0..eb241ec45329 100644 --- a/src/crangler/c_defines.h +++ b/src/crangler/c_defines.h @@ -12,8 +12,7 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef CPROVER_CRANGLER_C_DEFINES_H #define CPROVER_CRANGLER_C_DEFINES_H -#include - +#include #include #include #include @@ -25,7 +24,7 @@ class c_definest public: struct definet { - optionalt> parameters; + std::optional> parameters; std::string value; }; diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp index 7d716b745a43..2bb5f6b75a2f 100644 --- a/src/crangler/c_wrangler.cpp +++ b/src/crangler/c_wrangler.cpp @@ -80,7 +80,7 @@ struct c_wranglert std::vector function_contract; std::vector loop_contract; std::vector assertions; - optionalt stub; + std::optional stub; bool remove_static = false; }; diff --git a/src/crangler/mini_c_parser.cpp b/src/crangler/mini_c_parser.cpp index dba474d1210d..ce573ed166b2 100644 --- a/src/crangler/mini_c_parser.cpp +++ b/src/crangler/mini_c_parser.cpp @@ -114,7 +114,7 @@ bool c_declarationt::has_body() const return !initializer.empty() && initializer.front() == '{'; } -optionalt c_declarationt::declared_identifier() const +std::optional c_declarationt::declared_identifier() const { for(auto &t : declarator) if(is_identifier(t)) diff --git a/src/crangler/mini_c_parser.h b/src/crangler/mini_c_parser.h index ab3930aae33c..7453ec498afc 100644 --- a/src/crangler/mini_c_parser.h +++ b/src/crangler/mini_c_parser.h @@ -12,11 +12,10 @@ Author: Daniel Kroening, dkr@amazon.com #ifndef CPROVER_CRANGLER_MINI_C_PARSER_H #define CPROVER_CRANGLER_MINI_C_PARSER_H -#include - #include "ctoken.h" #include +#include #include struct c_declarationt @@ -32,7 +31,7 @@ struct c_declarationt void print(std::ostream &) const; bool is_function() const; bool has_body() const; - optionalt declared_identifier() const; + std::optional declared_identifier() const; }; using c_translation_unitt = std::vector; diff --git a/src/goto-analyzer/show_on_source.cpp b/src/goto-analyzer/show_on_source.cpp index c6dc644b0434..98f6d3889f92 100644 --- a/src/goto-analyzer/show_on_source.cpp +++ b/src/goto-analyzer/show_on_source.cpp @@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com /// get the name of the file referred to at a location loc, /// if any -static optionalt +static std::optional show_location(const ai_baset &ai, ai_baset::locationt loc) { const auto abstract_state = ai.abstract_state_before(loc); diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 45dd7b243dff..55726c91e2b8 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -42,7 +42,7 @@ class taint_analysist const symbol_tablet &, goto_functionst &, bool show_full, - const optionalt &json_file_name); + const std::optional &json_file_name); protected: messaget log; @@ -226,7 +226,7 @@ bool taint_analysist::operator()( const symbol_tablet &symbol_table, goto_functionst &goto_functions, bool show_full, - const optionalt &json_file_name) + const std::optional &json_file_name) { try { @@ -421,7 +421,7 @@ bool taint_analysis( const std::string &taint_file_name, message_handlert &message_handler, bool show_full, - const optionalt &json_file_name) + const std::optional &json_file_name) { taint_analysist taint_analysis(message_handler); return taint_analysis( diff --git a/src/goto-analyzer/taint_analysis.h b/src/goto-analyzer/taint_analysis.h index 841136a04135..6afb08995667 100644 --- a/src/goto-analyzer/taint_analysis.h +++ b/src/goto-analyzer/taint_analysis.h @@ -12,10 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H #define CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H +#include #include -#include - class goto_modelt; class message_handlert; @@ -24,6 +23,6 @@ bool taint_analysis( const std::string &taint_file_name, message_handlert &, bool show_full, - const optionalt &json_output_file_name = {}); + const std::optional &json_output_file_name = {}); #endif // CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 6ff7822bed79..7afcf5c32239 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -100,7 +100,7 @@ static void add_to_xml( return; } -static optionalt +static std::optional file_name_string_opt(const source_locationt &source_location) { if(source_location.get_file().empty()) @@ -249,7 +249,7 @@ bool static_unreachable_instructions( return false; } -static optionalt +static std::optional line_string_opt(const source_locationt &source_location) { const irep_idt &line = source_location.get_line(); diff --git a/src/goto-cc/armcc_cmdline.cpp b/src/goto-cc/armcc_cmdline.cpp index b5c2cae696a5..6b55671caa55 100644 --- a/src/goto-cc/armcc_cmdline.cpp +++ b/src/goto-cc/armcc_cmdline.cpp @@ -269,7 +269,7 @@ static const std::vector options_with_arg }; // clang-format on -optionalt +std::optional prefix_in_list(const std::string &option, const std::vector &list) { const auto found = @@ -293,7 +293,7 @@ bool armcc_cmdlinet::parse(int argc, const char **argv) } // it starts with - and it isn't "-" - optionalt prefix; + std::optional prefix; if(in_list(argv[i], options_no_arg)) { diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp index 3d76ace45792..730cfba7956f 100644 --- a/src/goto-cc/compile.cpp +++ b/src/goto-cc/compile.cpp @@ -307,7 +307,7 @@ bool compilet::find_library(const std::string &name) /// parses object files and links them /// \return true on error, false otherwise -bool compilet::link(optionalt &&symbol_table) +bool compilet::link(std::optional &&symbol_table) { // "compile" hitherto uncompiled functions log.statistics() << "Compiling functions" << messaget::eom; @@ -361,7 +361,7 @@ bool compilet::link(optionalt &&symbol_table) /// Parses source files and writes object files, or keeps the symbols in the /// symbol_table if not compiling/assembling only. /// \return Symbol table, if parsing and type checking succeeded, else empty -optionalt compilet::compile() +std::optional compilet::compile() { symbol_tablet symbol_table; @@ -606,7 +606,8 @@ bool compilet::write_bin_object_file( /// Parses and type checks a source file located at \p file_name. /// \return A symbol table if, and only if, parsing and type checking succeeded. -optionalt compilet::parse_source(const std::string &file_name) +std::optional +compilet::parse_source(const std::string &file_name) { language_filest language_files; diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h index f8480649a48c..3eb20174f0e3 100644 --- a/src/goto-cc/compile.h +++ b/src/goto-cc/compile.h @@ -64,10 +64,10 @@ class compilet bool parse(const std::string &filename, language_filest &); bool parse_stdin(languaget &); bool doit(); - optionalt compile(); - bool link(optionalt &&symbol_table); + std::optional compile(); + bool link(std::optional &&symbol_table); - optionalt parse_source(const std::string &); + std::optional parse_source(const std::string &); /// Writes the goto functions of \p src_goto_model to a binary format object /// file. diff --git a/src/goto-cc/goto_cc_cmdline.cpp b/src/goto-cc/goto_cc_cmdline.cpp index 722bc87148ab..8d997a466d0a 100644 --- a/src/goto-cc/goto_cc_cmdline.cpp +++ b/src/goto-cc/goto_cc_cmdline.cpp @@ -48,7 +48,7 @@ bool goto_cc_cmdlinet::in_list(const char *option, const char **list) std::size_t goto_cc_cmdlinet::get_optnr(const std::string &opt_string) { - optionalt optnr; + std::optional optnr; cmdlinet::optiont option; if(has_prefix(opt_string, "--")) // starts with -- ? diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp index fd43edccb857..fe4edcf12959 100644 --- a/src/goto-cc/ms_cl_cmdline.cpp +++ b/src/goto-cc/ms_cl_cmdline.cpp @@ -425,7 +425,7 @@ void ms_cl_cmdlinet::process_cl_option(const std::string &s) if(std::string(s, 1, std::string::npos)==ms_cl_flags[j]) { cmdlinet::optiont option; - optionalt optnr; + std::optional optnr; if(s.size()==2) { @@ -461,7 +461,7 @@ void ms_cl_cmdlinet::process_cl_option(const std::string &s) { cmdlinet::optiont option; - optionalt optnr; + std::optional optnr; if(ms_cl_prefix.size()==1) { diff --git a/src/goto-cc/ms_link_cmdline.cpp b/src/goto-cc/ms_link_cmdline.cpp index 5e63c9b13d1e..ddf5ae3d8c1b 100644 --- a/src/goto-cc/ms_link_cmdline.cpp +++ b/src/goto-cc/ms_link_cmdline.cpp @@ -335,7 +335,7 @@ void ms_link_cmdlinet::process_link_option(const std::string &s) to_upper_string(std::string(s, 1, std::string::npos)) == ms_link_option || to_upper_string(std::string(s, 1, ms_link_option.size() + 1)) == ms_link_option + ':') { - optionalt optnr = getoptnr(ms_link_option); + std::optional optnr = getoptnr(ms_link_option); if(!optnr.has_value()) { diff --git a/src/goto-harness/memory_snapshot_harness_generator.h b/src/goto-harness/memory_snapshot_harness_generator.h index ccfd3d7abf20..52a51fc25603 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.h +++ b/src/goto-harness/memory_snapshot_harness_generator.h @@ -9,8 +9,6 @@ Author: Daniel Poetzl #ifndef CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H #define CPROVER_GOTO_HARNESS_MEMORY_SNAPSHOT_HARNESS_GENERATOR_H -#include - #include #include "goto_harness_generator.h" @@ -55,7 +53,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort struct entry_goto_locationt { irep_idt function_name; - optionalt location_number; + std::optional location_number; entry_goto_locationt() = delete; explicit entry_goto_locationt(irep_idt function_name) @@ -317,7 +315,7 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort searchable_input[item.first] = item.second; } auto associate_key_with_t = - [&searchable_input](const Key &key) -> optionalt { + [&searchable_input](const Key &key) -> std::optional { if(searchable_input.count(key) != 0) return valuet(key, searchable_input[key]); else diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 28e86da5832e..79bc6bfedc0f 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -246,8 +246,8 @@ code_blockt build_null_pointer(const symbol_exprt &result_symbol) code_blockt recursive_initializationt::build_constructor_body( const exprt &depth_symbol, const symbol_exprt &result_symbol, - const optionalt &size_symbol, - const optionalt &lhs_name, + const std::optional &size_symbol, + const std::optional &lhs_name, const bool is_nullable) { PRECONDITION(result_symbol.type().id() == ID_pointer); @@ -297,8 +297,8 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) // or in case a `size` is associated with the `expr` // // void type_constructor_T(int depth_T, T *result_T, int *size); - optionalt size_var; - optionalt expr_name; + std::optional size_var; + std::optional expr_name; bool is_nullable = false; bool has_size_param = false; if(expr.id() == ID_symbol) @@ -335,7 +335,7 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) fun_params.push_back(result_parameter); auto &symbol_table = goto_model.symbol_table; - optionalt size_symbol_expr; + std::optional size_symbol_expr; if(expr_name.has_value() && should_be_treated_as_array(*expr_name)) { typet size_var_type; @@ -397,7 +397,7 @@ bool recursive_initializationt::should_be_treated_as_array( initialization_config.pointers_to_treat_as_arrays.end(); } -optionalt +std::optional recursive_initializationt::find_equal_cluster(const irep_idt &name) const { for(equal_cluster_idt index = 0; @@ -418,7 +418,7 @@ bool recursive_initializationt::is_array_size_parameter( initialization_config.variables_that_hold_array_sizes.end(); } -optionalt recursive_initializationt::get_associated_size_variable( +std::optional recursive_initializationt::get_associated_size_variable( const irep_idt &array_name) const { return optional_lookup( @@ -680,7 +680,7 @@ code_blockt recursive_initializationt::build_pointer_constructor( depth, ID_ge, get_symbol_expr(max_depth_var_name)}; exprt::operandst should_not_recurse{depth_gt_max_depth}; - optionalt has_seen; + std::optional has_seen; if(can_cast_type(to_pointer_type(type).base_type())) has_seen = get_fresh_global_symexpr( "has_seen_" + type2id(to_pointer_type(type).base_type())); @@ -820,7 +820,7 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( const exprt &depth, const symbol_exprt &result, const exprt &size, - const optionalt &lhs_name) + const std::optional &lhs_name) { PRECONDITION(result.type().id() == ID_pointer); const typet &dynamic_array_type = to_pointer_type(result.type()).base_type(); diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index bf7ed32036fd..04a30a19700b 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -14,7 +14,6 @@ Author: Diffblue Ltd. #include #include -#include #include #include #include @@ -123,7 +122,7 @@ class recursive_initializationt irep_idt max_depth_var_name; irep_idt min_depth_var_name; type_constructor_namest type_constructor_names; - std::vector> common_arguments_origins; + std::vector> common_arguments_origins; /// Get the malloc function as symbol exprt, /// and inserts it into the goto-model if it doesn't @@ -131,9 +130,10 @@ class recursive_initializationt symbol_exprt get_malloc_function(); bool should_be_treated_as_array(const irep_idt &pointer_name) const; - optionalt find_equal_cluster(const irep_idt &name) const; + std::optional + find_equal_cluster(const irep_idt &name) const; bool is_array_size_parameter(const irep_idt &cmdline_arg) const; - optionalt + std::optional get_associated_size_variable(const irep_idt &array_name) const; bool should_be_treated_as_cstring(const irep_idt &pointer_name) const; @@ -201,8 +201,8 @@ class recursive_initializationt code_blockt build_constructor_body( const exprt &depth_symbol, const symbol_exprt &result_symbol, - const optionalt &size_symbol, - const optionalt &lhs_name, + const std::optional &size_symbol, + const std::optional &lhs_name, const bool is_nullable); /// Check if a constructor for the type of \p expr already exists and create @@ -260,7 +260,7 @@ class recursive_initializationt const exprt &depth, const symbol_exprt &result, const exprt &size, - const optionalt &lhs_name); + const std::optional &lhs_name); /// Select the specified struct-member to be non-deterministically /// initialized. diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index 6bbf16a92ccf..954be5565e66 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -640,7 +640,7 @@ void disjunctive_polynomial_accelerationt::assert_for_values( exprt &target) { // First figure out what the appropriate type for this expression is. - optionalt expr_type; + std::optional expr_type; for(std::map::iterator it=values.begin(); it!=values.end(); diff --git a/src/goto-instrument/accelerate/polynomial.cpp b/src/goto-instrument/accelerate/polynomial.cpp index 789ae0b5b416..e9f4f910b048 100644 --- a/src/goto-instrument/accelerate/polynomial.cpp +++ b/src/goto-instrument/accelerate/polynomial.cpp @@ -22,7 +22,7 @@ Author: Matt Lewis exprt polynomialt::to_expr() { exprt ret=nil_exprt(); - optionalt itype; + std::optional itype; // Figure out the appropriate type to do all the intermediate calculations // in. diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 801821b76744..41a88788c582 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -497,7 +497,7 @@ void polynomial_acceleratort::assert_for_values( overflow_instrumentert &overflow) { // First figure out what the appropriate type for this expression is. - optionalt expr_type; + std::optional expr_type; for(std::map::iterator it=values.begin(); it!=values.end(); diff --git a/src/goto-instrument/concurrency.cpp b/src/goto-instrument/concurrency.cpp index 877b49b3651d..90daf39c4a08 100644 --- a/src/goto-instrument/concurrency.cpp +++ b/src/goto-instrument/concurrency.cpp @@ -58,14 +58,14 @@ class concurrency_instrumentationt { public: typet type; - optionalt array_symbol, w_index_symbol; + std::optional array_symbol, w_index_symbol; }; class thread_local_vart { public: typet type; - optionalt array_symbol; + std::optional array_symbol; }; typedef std::map shared_varst; diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index a140797eabc8..8b9e9ee23e88 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -625,7 +625,7 @@ void code_contractst::apply_function_contract( exprt::operandst instantiation_values; // keep track of the call's return expression to make it nondet later - optionalt call_ret_opt = {}; + std::optional call_ret_opt = {}; // if true, the call return variable variable was created during replacement bool call_ret_is_fresh_var = false; @@ -1272,7 +1272,7 @@ void code_contractst::add_contract_check( source_location.set_function(wrapper_function); // decl ret - optionalt return_stmt; + std::optional return_stmt; if(code_type.return_type() != empty_typet()) { symbol_exprt r = get_fresh_aux_symbol( diff --git a/src/goto-instrument/contracts/contracts_wrangler.cpp b/src/goto-instrument/contracts/contracts_wrangler.cpp index 62c040006a97..b3aab30e54c2 100644 --- a/src/goto-instrument/contracts/contracts_wrangler.cpp +++ b/src/goto-instrument/contracts/contracts_wrangler.cpp @@ -158,7 +158,7 @@ void contracts_wranglert::mangle( << log.eom; // Extract the assigns from parse_tree. - optionalt assigns_expr; + std::optional assigns_expr; if(!loop_contracts.assigns.empty()) { assigns_expr = static_cast(ansi_c_parser.parse_tree.items.front() diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp index db97996db2bc..4adf164a2037 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.cpp @@ -16,7 +16,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include #include @@ -117,7 +116,7 @@ void dfcc( const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt &to_check, + const std::optional &to_check, const bool allow_recursive_calls, const std::set &to_replace, const bool apply_loop_contracts, @@ -134,7 +133,7 @@ void dfcc( goto_model, harness_id, to_check.has_value() ? parse_function_contract_pair(to_check.value()) - : optionalt>{}, + : std::optional>{}, allow_recursive_calls, to_replace_map, apply_loop_contracts, @@ -147,7 +146,7 @@ void dfcc( const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt> &to_check, + const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, const bool apply_loop_contracts, @@ -172,7 +171,7 @@ dfcct::dfcct( const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt> &to_check, + const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, const dfcc_loop_contract_modet loop_contract_mode, diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc.h b/src/goto-instrument/contracts/dynamic-frames/dfcc.h index 88499b41e44f..247c70cf1272 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc.h @@ -106,7 +106,7 @@ void dfcc( const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt &to_check, + const std::optional &to_check, const bool allow_recursive_calls, const std::set &to_replace, const bool apply_loop_contracts, @@ -139,7 +139,7 @@ void dfcc( const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt> &to_check, + const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, const bool apply_loop_contracts, @@ -167,7 +167,7 @@ class dfcct const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, - const optionalt> &to_check, + const std::optional> &to_check, const bool allow_recursive_calls, const std::map &to_replace, const dfcc_loop_contract_modet loop_contract_mode, @@ -204,7 +204,7 @@ class dfcct const optionst &options; goto_modelt &goto_model; const irep_idt &harness_id; - const optionalt> &to_check; + const std::optional> &to_check; const bool allow_recursive_calls; const std::map &to_replace; const dfcc_loop_contract_modet loop_contract_mode; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp index 7eb14538971c..69073bbc1928 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp @@ -120,7 +120,7 @@ void dfcc_loop_infot::output(std::ostream &out) const out << "}\n"; } -optionalt +std::optional dfcc_loop_infot::find_head(goto_programt &goto_program) const { for(auto target = goto_program.instructions.begin(); @@ -135,10 +135,10 @@ dfcc_loop_infot::find_head(goto_programt &goto_program) const return {}; } -optionalt +std::optional dfcc_loop_infot::find_latch(goto_programt &goto_program) const { - optionalt result = std::nullopt; + std::optional result = std::nullopt; for(auto target = goto_program.instructions.begin(); target != goto_program.instructions.end(); target++) @@ -152,7 +152,7 @@ dfcc_loop_infot::find_latch(goto_programt &goto_program) const return result; } -static optionalt check_has_contract_rec( +static std::optional check_has_contract_rec( const dfcc_loop_nesting_grapht &loop_nesting_graph, const std::size_t loop_idx, const bool must_have_contract) @@ -174,7 +174,7 @@ static optionalt check_has_contract_rec( /// Traverses the loop nesting graph from top level loops and checks if all /// loops nested in loops that have contracts also have contracts. /// Return the head of the first offending loop if it exists, nothing otherwise. -static optionalt check_inner_loops_have_contracts( +static std::optional check_inner_loops_have_contracts( const dfcc_loop_nesting_grapht &loop_nesting_graph) { for(std::size_t idx = 0; idx < loop_nesting_graph.size(); idx++) @@ -710,7 +710,7 @@ dfcc_cfg_infot::get_loop_info(const std::size_t loop_id) const } // find the identifier or the immediately enclosing loop in topological order -const optionalt +const std::optional dfcc_cfg_infot::get_outer_loop_identifier(const std::size_t loop_id) const { PRECONDITION(is_valid_loop_id(loop_id)); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h index 03b0e776fbba..3cbd23551a66 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.h @@ -92,7 +92,7 @@ class dfcc_loop_infot /// instrumented in any other manner that might not maintain or copy the /// source location tags properly then nothing of the argument above is /// expected to hold anymore and you then use this method at your own risk. - optionalt + std::optional find_head(goto_programt &goto_program) const; // Finds the last instruction tagged as loop latch and having the same loop @@ -104,7 +104,7 @@ class dfcc_loop_infot // in the program and turning loops into non-loops. For an explanation of why // this would work please read the documentation of find head, and mentally // replace `head` by `latch` and `start` by `end` in the explanation. - optionalt + std::optional find_latch(goto_programt &goto_program) const; /// Loop identifier assigned by DFCC to this loop. @@ -272,7 +272,7 @@ class dfcc_cfg_infot /// Finds the DFCC id of the loop that contains the given loop, returns /// nullopt when the loop has no outer loop. - const optionalt + const std::optional get_outer_loop_identifier(const std::size_t loop_id) const; /// True iff a DECL ident must be tracked in the write set of the loop diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h index 09cf3cd01439..1bd4ab125bd1 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.h @@ -18,7 +18,6 @@ Date: February 2023 #include #include -#include #include #include "dfcc_contract_mode.h" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h index f274aa5f8f07..963dc5fdf60a 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h @@ -18,7 +18,6 @@ Date: August 2022 #include #include -#include #include #include "dfcc_contract_mode.h" diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp index c3add8fb8ed6..245f45bcfb3c 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp @@ -110,7 +110,7 @@ void dfcc_contract_handlert::add_contract_instructions( const symbolt &dfcc_contract_handlert::get_pure_contract_symbol( const irep_idt &contract_id, - const optionalt function_id_opt) + const std::optional function_id_opt) { auto pure_contract_id = "contract::" + id2string(contract_id); const symbolt *pure_contract_symbol = nullptr; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h index 51020c9547e7..0f77b8838764 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.h @@ -17,7 +17,6 @@ Date: August 2022 #include #include -#include #include #include "dfcc_contract_functions.h" @@ -111,7 +110,7 @@ class dfcc_contract_handlert /// PRECONDITION is triggered. const symbolt &get_pure_contract_symbol( const irep_idt &contract_id, - const optionalt function_id_opt = {}); + const std::optional function_id_opt = {}); protected: goto_modelt &goto_model; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp index ec5a7e8d0826..1f885938aca3 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.cpp @@ -752,7 +752,7 @@ void dfcc_instrumentt::instrument_lhs( /// Checks if lhs is the `dead_object`, and if the rhs /// is an `if_exprt(nondet, ptr, dead_object)` expression. /// Returns `ptr` if the pattern was matched, nullptr otherwise. -optionalt +std::optional dfcc_instrumentt::is_dead_object_update(const exprt &lhs, const exprt &rhs) { if( diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h index a65aaece8c03..4dd9aeec8811 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument.h @@ -286,7 +286,8 @@ class dfcc_instrumentt /// is an `if_exprt(nondet, ptr, dead_object)` expression. /// Returns a pointer to the `ptr` expression if the pattern was matched, /// returns `nullptr` otherwise. - optionalt is_dead_object_update(const exprt &lhs, const exprt &rhs); + std::optional + is_dead_object_update(const exprt &lhs, const exprt &rhs); /// Instrument the \p lhs of an `ASSIGN lhs := rhs` instruction by /// adding an inclusion check of \p lhs in \p write_set. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp index c4c5e8902bc3..4dcb8c9316d4 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.cpp @@ -203,7 +203,7 @@ dfcc_funt dfcc_libraryt::get_hook(const irep_idt &function_id) const } // Returns the havoc function to use for a given front-end function -optionalt +std::optional dfcc_libraryt::get_havoc_hook(const irep_idt &function_id) const { auto found = havoc_hook.find(function_id); @@ -362,7 +362,7 @@ void dfcc_libraryt::load(std::set &to_instrument) goto_model.goto_functions.function_map.at(it.second.name).make_hidden(); } -optionalt dfcc_libraryt::get_dfcc_fun(const irep_idt &id) const +std::optional dfcc_libraryt::get_dfcc_fun(const irep_idt &id) const { auto found = dfcc_name_to_fun.find(id); if(found != dfcc_name_to_fun.end()) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h index 615d88785d41..aa49b9fe5368 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_library.h @@ -14,7 +14,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include -#include #include @@ -223,7 +222,7 @@ class dfcc_libraryt void load(std::set &to_instrument); /// Returns the dfcc_funt that corresponds to the given id if any. - optionalt get_dfcc_fun(const irep_idt &id) const; + std::optional get_dfcc_fun(const irep_idt &id) const; /// Returns the name of the given dfcc_funt. const irep_idt &get_dfcc_fun_name(dfcc_funt fun) const; @@ -264,7 +263,7 @@ class dfcc_libraryt /// Returns the library instrumentation hook for the given built-in. /// function_id must be one of `__CPROVER_assignable`, /// `__CPROVER_object_whole`, `__CPROVER_object_from`, `__CPROVER_object_upto` - optionalt get_havoc_hook(const irep_idt &function_id) const; + std::optional get_havoc_hook(const irep_idt &function_id) const; /// \brief Returns the "__dfcc_instrumented_functions" symbol or creates it if /// it does not exist already. diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp index 3669ab3c1837..2a1429234c35 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_lift_memory_predicates.cpp @@ -180,7 +180,7 @@ std::set dfcc_lift_memory_predicatest::lift_predicates( } // returns an optional rank -static optionalt is_param_expr( +static std::optional is_param_expr( const exprt &expr, const std::map ¶meter_rank) { @@ -331,7 +331,7 @@ void dfcc_lift_memory_predicatest::lift_parameters_and_update_body( // rewrite all occurrences of lifted parameters instruction.transform([&replace_lifted_params](exprt expr) { const bool changed = !replace_lifted_params.replace(expr); - return changed ? optionalt{expr} : std::nullopt; + return changed ? std::optional{expr} : std::nullopt; }); // add address-of to all arguments expressions passed in lifted position to diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp index a9ba9ad9c1bb..6f1be29ad7d9 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.cpp @@ -23,7 +23,7 @@ void dfcc_set_loop_id( target->source_location_nonconst().set(ID_loop_id, loop_id); } -optionalt +std::optional dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target) { if(target->source_location().get(ID_loop_id).empty()) diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h index ab28a2c0d939..98d33d5d34fa 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_loop_tags.h @@ -24,7 +24,7 @@ bool dfcc_has_loop_id( const goto_programt::instructiont::const_targett &target, std::size_t loop_id); -optionalt +std::optional dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target); void dfcc_set_loop_head(goto_programt::instructiont::targett &target); diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp index 8a74801b1699..642aa1056046 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_swap_and_wrap.cpp @@ -16,7 +16,6 @@ Author: Remi Delmas, delmarsd@amazon.com #include #include #include -#include #include #include #include diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp index 703515a5ead9..4df01f607505 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.cpp @@ -301,7 +301,7 @@ const symbolt &dfcc_utilst::clone_and_rename_function( goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, - optionalt new_return_type = {}) + std::optional new_return_type = {}) { std::function trans_fun = [&](const irep_idt &old_name) { return new_function_id; }; diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h index 2b0bec8dbcbd..7923947bd4f2 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_utils.h @@ -104,7 +104,7 @@ struct dfcc_utilst goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, - optionalt new_return_type); + std::optional new_return_type); /// Given a function to wrap `foo` and a new name `wrapped_foo` /// diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h index 09ff311dbfa5..945999f9bfda 100644 --- a/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h +++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_wrapper_program.h @@ -17,7 +17,6 @@ Author: Remi Delmas, delmasrd@amazon.com #include #include -#include #include #include "dfcc_contract_functions.h" @@ -139,7 +138,7 @@ class dfcc_wrapper_programt const source_locationt wrapper_sl; /// Symbol for the return value of the wrapped function - optionalt return_value_opt; + std::optional return_value_opt; /// Symbol for the write set object derived from the contract const symbol_exprt contract_write_set; diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp index c290a1c3ce93..36af6b169642 100644 --- a/src/goto-instrument/cover_basic_blocks.cpp +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -13,7 +13,7 @@ Author: Peter Schrammel #include -optionalt cover_basic_blockst::continuation_of_block( +std::optional cover_basic_blockst::continuation_of_block( const goto_programt::const_targett &instruction, cover_basic_blockst::block_mapt &block_map) { @@ -103,7 +103,7 @@ std::size_t cover_basic_blockst::block_of(goto_programt::const_targett t) const return it->second; } -optionalt +std::optional cover_basic_blockst::instruction_of(const std::size_t block_nr) const { INVARIANT(block_nr < block_infos.size(), "block number out of range"); @@ -214,7 +214,7 @@ cover_basic_blocks_javat::block_of(goto_programt::const_targett t) const return it->second; } -optionalt +std::optional cover_basic_blocks_javat::instruction_of(const std::size_t block_nr) const { PRECONDITION(block_nr < block_infos.size()); diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h index 5fe8b5b97677..8c9bd2c2a894 100644 --- a/src/goto-instrument/cover_basic_blocks.h +++ b/src/goto-instrument/cover_basic_blocks.h @@ -12,8 +12,6 @@ Author: Daniel Kroening #ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H #define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H -#include - #include #include "source_lines.h" @@ -32,7 +30,7 @@ class cover_blocks_baset /// \param block_nr: a block number /// \return the instruction selected for /// instrumentation representative of the given block - virtual optionalt + virtual std::optional instruction_of(std::size_t block_nr) const = 0; /// \param block_nr: a block number @@ -77,7 +75,7 @@ class cover_basic_blockst final : public cover_blocks_baset /// \param block_nr: a block number /// \return the instruction selected for /// instrumentation representative of the given block - optionalt + std::optional instruction_of(std::size_t block_nr) const override; /// \param block_nr: a block number @@ -112,7 +110,7 @@ class cover_basic_blockst final : public cover_blocks_baset struct block_infot { /// the program location to instrument for this block - optionalt representative_inst; + std::optional representative_inst; /// the source location representative for this block /// (we need a separate copy of source locations because we attach @@ -135,7 +133,7 @@ class cover_basic_blockst final : public cover_blocks_baset /// If this block is a continuation of a previous block through unconditional /// forward gotos, return this blocks number. - static optionalt continuation_of_block( + static std::optional continuation_of_block( const goto_programt::const_targett &instruction, block_mapt &block_map); }; @@ -161,7 +159,7 @@ class cover_basic_blocks_javat final : public cover_blocks_baset /// \param block_number: a block number /// \return first instruction of the given block - optionalt + std::optional instruction_of(std::size_t block_number) const override; /// \param block_number: a block number diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 0b867faff8ea..e1bc37c9509f 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -728,7 +728,7 @@ void dump_ct::cleanup_decl( goto_programt tmp; tmp.add(goto_programt::make_decl(decl.symbol())); - if(optionalt value = decl.initial_value()) + if(std::optional value = decl.initial_value()) { decl.set_initial_value({}); tmp.add(goto_programt::make_assignment(decl.symbol(), std::move(*value))); @@ -1536,7 +1536,7 @@ void dump_ct::cleanup_expr(exprt &expr) } } - optionalt clean_init; + std::optional clean_init; if( ns.follow(bu.type()).id() == ID_union && bu.source_location().get_function().empty()) diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index 3687fb651873..be24ed70d30a 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -355,8 +355,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest private: const std::vector globals_to_havoc; - optionalt parameters_to_havoc; - optionalt> param_numbers_to_havoc; + std::optional parameters_to_havoc; + std::optional> param_numbers_to_havoc; const c_object_factory_parameterst &object_factory_parameters; mutable messaget message; }; diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 55721374ce63..534294d484d4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1214,8 +1214,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() options, goto_model, harness_id, - to_enforce.empty() ? optionalt{} - : optionalt{to_enforce.front()}, + to_enforce.empty() ? std::optional{} + : std::optional{to_enforce.front()}, allow_recursive_calls, to_replace, cmdline.isset(FLAG_LOOP_CONTRACTS), diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp index d15822489cb4..7dc097efd031 100644 --- a/src/goto-instrument/unwindset.cpp +++ b/src/goto-instrument/unwindset.cpp @@ -33,7 +33,7 @@ void unwindsett::parse_unwindset_one_loop( if(val.empty()) return; - optionalt thread_nr; + std::optional thread_nr; if(isdigit(val[0])) { auto c_pos = val.find(':'); @@ -116,8 +116,8 @@ void unwindsett::parse_unwindset_one_loop( } else { - optionalt nr; - optionalt location; + std::optional nr; + std::optional location; for(const auto &instruction : goto_function.body.instructions) { if( @@ -161,7 +161,7 @@ void unwindsett::parse_unwindset_one_loop( std::string uw_string = val.substr(last_c_pos + 1); // the below initialisation makes g++-5 happy - optionalt uw(0); + std::optional uw(0); if(uw_string.empty()) uw = {}; @@ -187,7 +187,7 @@ void unwindsett::parse_unwindset( parse_unwindset_one_loop(element, message_handler); } -optionalt +std::optional unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const { // We use the most specific limit we have diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h index b62ba11710e5..4e3ffde04456 100644 --- a/src/goto-instrument/unwindset.h +++ b/src/goto-instrument/unwindset.h @@ -13,10 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H #include -#include #include #include +#include #include class abstract_goto_modelt; @@ -43,7 +43,8 @@ class unwindsett message_handlert &message_handler); // queries - optionalt get_limit(const irep_idt &loop, unsigned thread_id) const; + std::optional + get_limit(const irep_idt &loop, unsigned thread_id) const; // read unwindset directives from a file void parse_unwindset_file( @@ -53,16 +54,16 @@ class unwindsett protected: abstract_goto_modelt &goto_model; - optionalt global_limit; + std::optional global_limit; // Limit for all instances of a loop. // This may have 'no value'. - typedef std::map> loop_mapt; + typedef std::map> loop_mapt; loop_mapt loop_map; // separate limits per thread using thread_loop_mapt = - std::map, optionalt>; + std::map, std::optional>; thread_loop_mapt thread_loop_map; void parse_unwindset_one_loop( diff --git a/src/goto-programs/adjust_float_expressions.cpp b/src/goto-programs/adjust_float_expressions.cpp index 9b44d90f1fe2..eafea9ed5a3f 100644 --- a/src/goto-programs/adjust_float_expressions.cpp +++ b/src/goto-programs/adjust_float_expressions.cpp @@ -207,7 +207,7 @@ void adjust_float_expressions( const namespacet &ns) { for(auto &i : goto_function.body.instructions) - i.transform([&ns](exprt expr) -> optionalt { + i.transform([&ns](exprt expr) -> std::optional { if(have_to_adjust_float_expressions(expr)) { adjust_float_expressions(expr, ns); diff --git a/src/goto-programs/destructor_tree.cpp b/src/goto-programs/destructor_tree.cpp index e54528255552..224bb8fb3349 100644 --- a/src/goto-programs/destructor_tree.cpp +++ b/src/goto-programs/destructor_tree.cpp @@ -16,7 +16,7 @@ void destructor_treet::add(const codet &destructor) current_node = new_node; } -optionalt &destructor_treet::get_destructor(node_indext index) +std::optional &destructor_treet::get_destructor(node_indext index) { PRECONDITION(index < destruction_graph.size()); return destruction_graph[index].destructor_value; @@ -54,8 +54,8 @@ const ancestry_resultt destructor_treet::get_nearest_common_ancestor_info( } const std::vector destructor_treet::get_destructors( - optionalt end_index, - optionalt starting_index) + std::optional end_index, + std::optional starting_index) { node_indext next_id = starting_index.value_or(get_current_node()); node_indext end_id = end_index.value_or(0); @@ -74,7 +74,7 @@ const std::vector destructor_treet::get_destructors( return codes; } -void destructor_treet::set_current_node(optionalt val) +void destructor_treet::set_current_node(std::optional val) { if(val) set_current_node(*val); diff --git a/src/goto-programs/destructor_tree.h b/src/goto-programs/destructor_tree.h index 286e5678f82b..719f308babb6 100644 --- a/src/goto-programs/destructor_tree.h +++ b/src/goto-programs/destructor_tree.h @@ -99,7 +99,7 @@ class destructor_treet void add(const codet &destructor); /// Fetches the destructor value for the passed-in node index. - optionalt &get_destructor(node_indext index); + std::optional &get_destructor(node_indext index); /// Builds a vector of destructors that start from starting_index and ends /// at end_index. @@ -110,8 +110,8 @@ class destructor_treet /// \return collection of destructors that should be called for the /// range supplied. const std::vector get_destructors( - optionalt end_index = {}, - optionalt starting_index = {}); + std::optional end_index = {}, + std::optional starting_index = {}); /// Finds the nearest common ancestor of two nodes and then returns it. /// This should be used when you want to find out what parts of the two @@ -123,7 +123,7 @@ class destructor_treet /// Sets the current node. Next time a node is added to the stack it will /// be added as a child of this node. If passed an empty index, no /// assignment will be done. - void set_current_node(optionalt val); + void set_current_node(std::optional val); /// Sets the current node. Next time a node is added to the stack it will /// be added as a child of this node. @@ -145,7 +145,7 @@ class destructor_treet : destructor_value(std::move(destructor)) { } - optionalt destructor_value; + std::optional destructor_value; }; grapht destruction_graph; diff --git a/src/goto-programs/format_strings.cpp b/src/goto-programs/format_strings.cpp index 831a1bc8cf76..ecbf78e5fe50 100644 --- a/src/goto-programs/format_strings.cpp +++ b/src/goto-programs/format_strings.cpp @@ -225,7 +225,7 @@ format_token_listt parse_format_string(const std::string &arg_string) return token_list; } -optionalt get_type(const format_tokent &token) +std::optional get_type(const format_tokent &token) { switch(token.type) { diff --git a/src/goto-programs/format_strings.h b/src/goto-programs/format_strings.h index 82e548d74cff..7e77c032caea 100644 --- a/src/goto-programs/format_strings.h +++ b/src/goto-programs/format_strings.h @@ -12,12 +12,12 @@ Author: CM Wintersteiger #ifndef CPROVER_GOTO_PROGRAMS_FORMAT_STRINGS_H #define CPROVER_GOTO_PROGRAMS_FORMAT_STRINGS_H -#include -#include - #include #include -#include + +#include +#include +#include class typet; @@ -91,6 +91,6 @@ typedef std::list format_token_listt; format_token_listt parse_format_string(const std::string &); -optionalt get_type(const format_tokent &); +std::optional get_type(const format_tokent &); #endif // CPROVER_GOTO_PROGRAMS_FORMAT_STRINGS_H diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 05bc4aae9915..84a48ae06a16 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -359,8 +359,8 @@ class goto_convertt:public messaget const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, - optionalt destructor_start_point = {}, - optionalt destructor_end_point = {}); + std::optional destructor_start_point = {}, + std::optional destructor_end_point = {}); // // gotos diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index f6b0a7a36081..7bb21ac2b613 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -281,8 +281,8 @@ void goto_convertt::unwind_destructor_stack( const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, - optionalt end_index, - optionalt starting_index) + std::optional end_index, + std::optional starting_index) { // As we go we'll keep targets.destructor_stack.current_node pointing at the // next node we intend to destroy, so that if our convert(...) call for each @@ -305,7 +305,7 @@ void goto_convertt::unwind_destructor_stack( { node_indext current_node = targets.destructor_stack.get_current_node(); - optionalt &destructor = + std::optional &destructor = targets.destructor_stack.get_destructor(current_node); // Descend the tree before unwinding so we don't re-do the current node diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 7cb9837c06e7..f7ff84f02d46 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -46,7 +46,7 @@ void goto_convertt::remove_assignment( { const irep_idt statement=expr.get_statement(); - optionalt replacement_expr_opt; + std::optional replacement_expr_opt; if(statement==ID_assign) { diff --git a/src/goto-programs/goto_instruction_code.cpp b/src/goto-programs/goto_instruction_code.cpp index 1547364f1a76..65826ee8b7e8 100644 --- a/src/goto-programs/goto_instruction_code.cpp +++ b/src/goto-programs/goto_instruction_code.cpp @@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com code_inputt::code_inputt( std::vector arguments, - optionalt location) + std::optional location) : codet{ID_input, std::move(arguments)} { if(location) @@ -32,12 +32,13 @@ code_inputt::code_inputt( code_inputt::code_inputt( const irep_idt &description, exprt expression, - optionalt location) - : code_inputt{{address_of_exprt(index_exprt( - string_constantt(description), - from_integer(0, c_index_type()))), - std::move(expression)}, - std::move(location)} + std::optional location) + : code_inputt{ + {address_of_exprt(index_exprt( + string_constantt(description), + from_integer(0, c_index_type()))), + std::move(expression)}, + std::move(location)} { } @@ -49,7 +50,7 @@ void code_inputt::check(const codet &code, const validation_modet vm) code_outputt::code_outputt( std::vector arguments, - optionalt location) + std::optional location) : codet{ID_output, std::move(arguments)} { if(location) @@ -60,12 +61,13 @@ code_outputt::code_outputt( code_outputt::code_outputt( const irep_idt &description, exprt expression, - optionalt location) - : code_outputt{{address_of_exprt(index_exprt( - string_constantt(description), - from_integer(0, c_index_type()))), - std::move(expression)}, - std::move(location)} + std::optional location) + : code_outputt{ + {address_of_exprt(index_exprt( + string_constantt(description), + from_integer(0, c_index_type()))), + std::move(expression)}, + std::move(location)} { } diff --git a/src/goto-programs/goto_instruction_code.h b/src/goto-programs/goto_instruction_code.h index a7d53e678504..946cbe61119a 100644 --- a/src/goto-programs/goto_instruction_code.h +++ b/src/goto-programs/goto_instruction_code.h @@ -411,7 +411,7 @@ class code_inputt : public goto_instruction_codet /// `const char *` and one or more corresponding expression arguments follow. explicit code_inputt( std::vector arguments, - optionalt location = {}); + std::optional location = {}); /// This constructor is intended for generating input instructions as part of /// synthetic entry point code, rather than as part of user code. @@ -424,7 +424,7 @@ class code_inputt : public goto_instruction_codet code_inputt( const irep_idt &description, exprt expression, - optionalt location = {}); + std::optional location = {}); static void check( const goto_instruction_codet &code, @@ -458,7 +458,7 @@ class code_outputt : public goto_instruction_codet /// `const char *` and one or more corresponding expression arguments follow. explicit code_outputt( std::vector arguments, - optionalt location = {}); + std::optional location = {}); /// This constructor is intended for generating output instructions as part of /// synthetic entry point code, rather than as part of user code. @@ -470,7 +470,7 @@ class code_outputt : public goto_instruction_codet code_outputt( const irep_idt &description, exprt expression, - optionalt location = {}); + std::optional location = {}); static void check( const goto_instruction_codet &code, diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index f80328a57224..db89fd0f4fd1 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -982,7 +982,7 @@ void goto_programt::instructiont::validate( } void goto_programt::instructiont::transform( - std::function(exprt)> f) + std::function(exprt)> f) { switch(_type) { diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 8d17e400e25b..5cbe7fc9ac21 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -598,7 +598,7 @@ class goto_programt /// Apply given transformer to all expressions; no return value /// means no change needed. - void transform(std::function(exprt)>); + void transform(std::function(exprt)>); /// Apply given function to all expressions void apply(std::function) const; diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index ed2c4a401e11..1c1f1625028e 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -30,7 +30,7 @@ Author: Daniel Kroening #include -static optionalt get_object_rec(const exprt &src) +static std::optional get_object_rec(const exprt &src) { if(src.id()==ID_symbol) return to_symbol_expr(src); @@ -50,7 +50,7 @@ static optionalt get_object_rec(const exprt &src) return {}; // give up } -optionalt goto_trace_stept::get_lhs_object() const +std::optional goto_trace_stept::get_lhs_object() const { return get_object_rec(full_lhs); } @@ -292,7 +292,7 @@ std::string trace_numeric_value( static void trace_value( messaget::mstreamt &out, const namespacet &ns, - const optionalt &lhs_object, + const std::optional &lhs_object, const exprt &full_lhs, const exprt &value, const trace_optionst &options) diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index e6b6ea727a7b..a9c91cf98e13 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -127,7 +127,7 @@ class goto_trace_stept exprt full_lhs; // the object being assigned - optionalt get_lhs_object() const; + std::optional get_lhs_object() const; // A constant with the new value of the lhs exprt full_lhs_value; diff --git a/src/goto-programs/interpreter_class.h b/src/goto-programs/interpreter_class.h index 425934e87faf..e873546db7ad 100644 --- a/src/goto-programs/interpreter_class.h +++ b/src/goto-programs/interpreter_class.h @@ -107,7 +107,7 @@ class interpretert const goto_functionst &goto_functions; typedef std::unordered_map memory_mapt; - using inverse_memory_mapt = std::map>; + using inverse_memory_mapt = std::map>; memory_mapt memory_map; inverse_memory_mapt inverse_memory_map; diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 5c66ae0d6efd..81ea5b3eddac 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -106,7 +106,7 @@ static bool link_functions( return false; } -optionalt link_goto_model( +std::optional link_goto_model( goto_modelt &dest, goto_modelt &&src, message_handlert &message_handler) @@ -217,7 +217,7 @@ void finalize_linking( { instruction.transform([&object_type_updates](exprt expr) { const bool changed = !object_type_updates.replace(expr); - return changed ? optionalt{expr} : std::nullopt; + return changed ? std::optional{expr} : std::nullopt; }); } } diff --git a/src/goto-programs/link_goto_model.h b/src/goto-programs/link_goto_model.h index cf37cfe4dbac..04ba2cacdf2f 100644 --- a/src/goto-programs/link_goto_model.h +++ b/src/goto-programs/link_goto_model.h @@ -22,7 +22,7 @@ class message_handlert; /// which need to be applied using \ref finalize_linking. /// \return nullopt if linking fails, else a (possibly empty) collection of /// replacements to be applied. -[[nodiscard]] optionalt +[[nodiscard]] std::optional link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &); /// Apply \p type_updates to \p dest, where \p type_updates were constructed diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp index ed26d11a85b0..f37433209201 100644 --- a/src/goto-programs/link_to_library.cpp +++ b/src/goto-programs/link_to_library.cpp @@ -19,7 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "link_goto_model.h" /// Try to add \p missing_function from \p library to \p goto_model. -static std::pair, bool> add_one_function( +static std::pair, bool> +add_one_function( goto_modelt &goto_model, message_handlert &message_handler, const std::function +std::optional read_goto_binary(const std::string &filename, message_handlert &message_handler) { goto_modelt dest; @@ -261,7 +261,7 @@ bool is_goto_binary( /// \param dest: the goto model returned /// \param message_handler: for diagnostics /// \return nullopt on error, type replacements to be applied otherwise -static optionalt read_object_and_link( +static std::optional read_object_and_link( const std::string &file_name, goto_modelt &dest, message_handlert &message_handler) diff --git a/src/goto-programs/read_goto_binary.h b/src/goto-programs/read_goto_binary.h index 462657df8b69..58934b2bc71a 100644 --- a/src/goto-programs/read_goto_binary.h +++ b/src/goto-programs/read_goto_binary.h @@ -13,14 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_PROGRAMS_READ_GOTO_BINARY_H #include +#include #include -#include - class goto_modelt; class message_handlert; -optionalt +std::optional read_goto_binary(const std::string &filename, message_handlert &); bool is_goto_binary(const std::string &filename, message_handlert &); diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index c13ad86bab40..c983692cfb18 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -286,7 +286,7 @@ static void remove_complex( goto_functionst::goto_functiont &goto_function) { for(auto &i : goto_function.body.instructions) - i.transform([](exprt e) -> optionalt { + i.transform([](exprt e) -> std::optional { if(have_to_remove_complex(e)) { remove_complex(e); diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 2c9248965b71..f92f07358aa8 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -59,11 +59,11 @@ class remove_returnst void undo_function_calls( goto_programt &goto_program); - optionalt + std::optional get_or_create_return_value_symbol(const irep_idt &function_id); }; -optionalt +std::optional remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id) { const namespacet ns(symbol_table); @@ -173,7 +173,7 @@ bool remove_returnst::do_function_calls( exprt rhs; bool is_stub = function_is_stub(function_id); - optionalt return_value; + std::optional return_value; if(!is_stub) return_value = get_or_create_return_value_symbol(function_id); diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 32f589e99e3c..2809f8cfa1c1 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -354,7 +354,7 @@ static void remove_vector(symbol_table_baset &symbol_table) void remove_vector(goto_functionst::goto_functiont &goto_function) { for(auto &i : goto_function.body.instructions) - i.transform([](exprt e) -> optionalt { + i.transform([](exprt e) -> std::optional { if(have_to_remove_vector(e)) { remove_vector(e); diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 171a00377745..08eb51fe6406 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -45,13 +45,13 @@ class get_virtual_calleest const class_hierarchyt &class_hierarchy; typedef std::function< - optionalt( + std::optional( const irep_idt &, const irep_idt &)> function_call_resolvert; void get_child_functions_rec( const irep_idt &, - const optionalt &, + const std::optional &, const irep_idt &, dispatch_table_entriest &, dispatch_table_entries_mapt &) const; @@ -507,7 +507,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function( /// \param entry_map: map of class identifiers to dispatch table entries void get_virtual_calleest::get_child_functions_rec( const irep_idt &this_id, - const optionalt &last_method_defn, + const std::optional &last_method_defn, const irep_idt &component_name, dispatch_table_entriest &functions, dispatch_table_entries_mapt &entry_map) const diff --git a/src/goto-programs/remove_virtual_functions.h b/src/goto-programs/remove_virtual_functions.h index 394db351c987..5dd9d7d1e510 100644 --- a/src/goto-programs/remove_virtual_functions.h +++ b/src/goto-programs/remove_virtual_functions.h @@ -15,7 +15,6 @@ Date: April 2016 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H -#include #include #include "goto_program.h" @@ -96,7 +95,7 @@ class dispatch_table_entryt } #endif - optionalt symbol_expr; + std::optional symbol_expr; irep_idt class_id; }; diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp index 4a264460685e..d3d855bbeff3 100644 --- a/src/goto-programs/resolve_inherited_component.cpp +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -32,7 +32,7 @@ resolve_inherited_componentt::resolve_inherited_componentt( /// \param user_filter: Predicate that should return true for symbols that can /// be returned. Those for which it returns false will be ignored. /// \return The concrete component that has been resolved -optionalt +std::optional resolve_inherited_componentt::operator()( const irep_idt &class_id, const irep_idt &component_name, @@ -122,7 +122,7 @@ irep_idt resolve_inherited_componentt::inherited_componentt:: /// class specifier) /// \param symbol_table: Global symbol table /// \return The concrete component that has been resolved -optionalt +std::optional get_inherited_method_implementation( const irep_idt &call_basename, const irep_idt &classname, diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h index 26210b59aff5..a15d61c68e51 100644 --- a/src/goto-programs/resolve_inherited_component.h +++ b/src/goto-programs/resolve_inherited_component.h @@ -14,9 +14,9 @@ Author: Diffblue Ltd. #define CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H #include -#include #include +#include class symbolt; class symbol_table_baset; @@ -47,7 +47,7 @@ class resolve_inherited_componentt irep_idt component_identifier; }; - optionalt operator()( + std::optional operator()( const irep_idt &class_id, const irep_idt &component_name, bool include_interfaces, @@ -62,7 +62,7 @@ class resolve_inherited_componentt const symbol_table_baset &symbol_table; }; -optionalt +std::optional get_inherited_method_implementation( const irep_idt &call_basename, const irep_idt &classname, diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 1fa3c6f94bea..e7ddab4fa06d 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -323,7 +323,7 @@ static std::string resolve_pointer_name( const auto it = goto_model.goto_functions.function_map.find(function_id); if(it != goto_model.goto_functions.function_map.end()) { - optionalt location; + std::optional location; for(const auto &instruction : it->second.body.instructions) { if( @@ -421,7 +421,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( return std::make_pair(pointer_name, target_names); } -optionalt +std::optional function_pointer_restrictionst::get_by_name_restriction( const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, @@ -457,7 +457,7 @@ function_pointer_restrictionst::get_by_name_restriction( if(restriction != by_name_restrictions.end()) { - return optionalt( + return std::optional( std::make_pair( function_pointer_call_site.get_identifier(), restriction->second)); } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index 1046a6b9737c..b934db7d6d74 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -22,7 +22,6 @@ Author: Diffblue Ltd. #include #include -#include #include "goto_program.h" @@ -132,7 +131,7 @@ class function_pointer_restrictionst const std::string &option, const goto_modelt &goto_model); - static optionalt get_by_name_restriction( + static std::optional get_by_name_restriction( const goto_functiont &goto_function, const function_pointer_restrictionst::restrictionst &by_name_restrictions, const goto_programt::const_targett &location); diff --git a/src/goto-programs/rewrite_rw_ok.cpp b/src/goto-programs/rewrite_rw_ok.cpp index 09433e5d8df8..b23c76164028 100644 --- a/src/goto-programs/rewrite_rw_ok.cpp +++ b/src/goto-programs/rewrite_rw_ok.cpp @@ -13,7 +13,7 @@ Author: Michael Tautschnig #include -static optionalt rewrite_rw_ok(exprt expr, const namespacet &ns) +static std::optional rewrite_rw_ok(exprt expr, const namespacet &ns) { bool unchanged = true; diff --git a/src/goto-programs/rewrite_union.cpp b/src/goto-programs/rewrite_union.cpp index f52dfe04f9f8..3fcb4b33e914 100644 --- a/src/goto-programs/rewrite_union.cpp +++ b/src/goto-programs/rewrite_union.cpp @@ -152,7 +152,7 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns) comp.type().id() == ID_array || comp.type().id() == ID_struct || comp.type().id() == ID_struct_tag) { - optionalt result = get_subexpression_at_offset( + std::optional result = get_subexpression_at_offset( member_exprt{be.op(), comp.get_name(), comp.type()}, be.offset(), be.type(), diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 90be11961c2e..c3e94c266003 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -19,9 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_model.h" -optionalt find_property( - const irep_idt &property, - const goto_functionst & goto_functions) +std::optional +find_property(const irep_idt &property, const goto_functionst &goto_functions) { for(const auto &fct : goto_functions.function_map) { diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h index 0e41f5c85d13..1a7cfa494ca9 100644 --- a/src/goto-programs/show_properties.h +++ b/src/goto-programs/show_properties.h @@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H #include -#include + +#include class json_arrayt; class namespacet; @@ -45,9 +46,8 @@ void show_properties( /// the property /// \return optional the location of the /// property, if found. -optionalt find_property( - const irep_idt &property, - const goto_functionst &goto_functions); +std::optional +find_property(const irep_idt &property, const goto_functionst &goto_functions); /// \brief Collects the properties in the goto program into a `json_arrayt` /// \param json_properties: JSON array to hold the properties diff --git a/src/goto-programs/structured_trace_util.cpp b/src/goto-programs/structured_trace_util.cpp index 07260626a9bc..d547f1538537 100644 --- a/src/goto-programs/structured_trace_util.cpp +++ b/src/goto-programs/structured_trace_util.cpp @@ -36,7 +36,7 @@ std::string default_step_name(const default_step_kindt &step_type) UNREACHABLE; } -optionalt default_step( +std::optional default_step( const goto_trace_stept &step, const source_locationt &previous_source_location) { diff --git a/src/goto-programs/structured_trace_util.h b/src/goto-programs/structured_trace_util.h index e8bbbf32b16b..bd48aec9702b 100644 --- a/src/goto-programs/structured_trace_util.h +++ b/src/goto-programs/structured_trace_util.h @@ -46,7 +46,7 @@ struct default_trace_stept source_locationt location; }; -optionalt default_step( +std::optional default_step( const goto_trace_stept &step, const source_locationt &previous_source_location); diff --git a/src/goto-symex/frame.h b/src/goto-symex/frame.h index e5edcf4acb72..cd10b391b62b 100644 --- a/src/goto-symex/frame.h +++ b/src/goto-symex/frame.h @@ -36,7 +36,7 @@ struct framet guardt guard_at_function_start; goto_programt::const_targett end_of_function; exprt call_lhs = nil_exprt(); // cleaned, but not renamed - optionalt return_value_symbol; // not renamed + std::optional return_value_symbol; // not renamed bool hidden_function = false; symex_level1t old_level1; diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp index 9fff87a639d7..f2c88ae4b1b6 100644 --- a/src/goto-symex/goto_symex.cpp +++ b/src/goto-symex/goto_symex.cpp @@ -362,7 +362,7 @@ void goto_symext::associate_array_to_pointer( ssa_expr, expr_skeletont{}, array_to_pointer_app, {}); } -optionalt> +std::optional> goto_symext::try_evaluate_constant_string( const statet &state, const exprt &content) @@ -383,7 +383,7 @@ goto_symext::try_evaluate_constant_string( return try_get_string_data_array(s_pointer_opt->get(), ns); } -optionalt> +std::optional> goto_symext::try_evaluate_constant(const statet &state, const exprt &expr) { if(expr.id() != ID_symbol) @@ -399,7 +399,7 @@ goto_symext::try_evaluate_constant(const statet &state, const exprt &expr) return {}; } - return optionalt>( + return std::optional>( to_constant_expr(constant_expr_opt->get())); } diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 72de8769922b..85b2622aed83 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -742,11 +742,11 @@ class goto_symext const array_exprt &new_char_array, const address_of_exprt &string_data); - optionalt> + std::optional> try_evaluate_constant_string(const statet &state, const exprt &content); // clang-format off - static optionalt> + static std::optional> try_evaluate_constant( const statet &state, const exprt &expr); diff --git a/src/goto-symex/renamed.h b/src/goto-symex/renamed.h index 1f6da139f13a..71bf60403e9d 100644 --- a/src/goto-symex/renamed.h +++ b/src/goto-symex/renamed.h @@ -48,7 +48,7 @@ class renamedt : private underlyingt } using mutator_functiont = - std::function(const renamedt &)>; + std::function(const renamedt &)>; private: underlyingt &value() @@ -99,7 +99,7 @@ void selectively_mutate( for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend; ++it) { - optionalt> replacement = + std::optional> replacement = get_mutated_expr(static_cast &>(*it)); if(replacement) diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp index cb77b6610e3d..7109f4b0c09a 100644 --- a/src/goto-symex/renaming_level.cpp +++ b/src/goto-symex/renaming_level.cpp @@ -52,7 +52,8 @@ void symex_level1t::insert( ssa.get().get_identifier(), std::make_pair(ssa.get(), index)); } -optionalt> symex_level1t::insert_or_replace( +std::optional> +symex_level1t::insert_or_replace( const renamedt &ssa, std::size_t index) { diff --git a/src/goto-symex/renaming_level.h b/src/goto-symex/renaming_level.h index 211b3fc3b868..eda7865f59a4 100644 --- a/src/goto-symex/renaming_level.h +++ b/src/goto-symex/renaming_level.h @@ -44,7 +44,7 @@ struct symex_level1t /// Set the index for \p ssa to index. /// \return if an index for \p ssa was already know, returns it's previous /// value. - optionalt> + std::optional> insert_or_replace(const renamedt &ssa, std::size_t index); /// \return true if \p ssa has an associated index diff --git a/src/goto-symex/shadow_memory.cpp b/src/goto-symex/shadow_memory.cpp index b8481c7c02d8..43dbf4aa899b 100644 --- a/src/goto-symex/shadow_memory.cpp +++ b/src/goto-symex/shadow_memory.cpp @@ -126,7 +126,7 @@ void shadow_memoryt::symex_set_field( // build lhs const exprt &rhs = value; size_t mux_size = 0; - optionalt maybe_lhs = + std::optional maybe_lhs = get_shadow_memory(expr, value_set, addresses, ns, log, mux_size); // add to equation diff --git a/src/goto-symex/shadow_memory_util.cpp b/src/goto-symex/shadow_memory_util.cpp index b33920b258b2..32aa569e307a 100644 --- a/src/goto-symex/shadow_memory_util.cpp +++ b/src/goto-symex/shadow_memory_util.cpp @@ -1127,7 +1127,7 @@ get_shadow_memory_for_matched_object( return result; } -optionalt get_shadow_memory( +std::optional get_shadow_memory( const exprt &expr, const std::vector &value_set, const std::vector &addresses, diff --git a/src/goto-symex/shadow_memory_util.h b/src/goto-symex/shadow_memory_util.h index abe4e70be94d..5f2de25c277a 100644 --- a/src/goto-symex/shadow_memory_util.h +++ b/src/goto-symex/shadow_memory_util.h @@ -193,7 +193,7 @@ bool check_value_set_contains_only_null_ptr( /// set, then we get back an `if e1 then e2 else (if e3 else e4...` /// expression, where `e1`, `e3`, ... are guards (conditions) and `e2`, `e4`, /// etc are the possible values of the object within the value set. -optionalt get_shadow_memory( +std::optional get_shadow_memory( const exprt &expr, const std::vector &value_set, const std::vector &addresses, diff --git a/src/goto-symex/symex_assign.h b/src/goto-symex/symex_assign.h index 42738414b63f..2d8fa1611a77 100644 --- a/src/goto-symex/symex_assign.h +++ b/src/goto-symex/symex_assign.h @@ -28,7 +28,7 @@ class symex_assignt { public: symex_assignt( - optionalt shadow_memory, + std::optional shadow_memory, goto_symex_statet &state, symex_targett::assignment_typet assignment_type, const namespacet &ns, @@ -60,7 +60,7 @@ class symex_assignt exprt::operandst &guard); private: - optionalt shadow_memory; + std::optional shadow_memory; goto_symex_statet &state; symex_targett::assignment_typet assignment_type; const namespacet &ns; diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index ca290a7090d9..6dbe4da94363 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -25,7 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "path_storage.h" -inline static optionalt c_sizeof_type_rec(const exprt &expr) +inline static std::optional c_sizeof_type_rec(const exprt &expr) { const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); @@ -57,7 +57,7 @@ void goto_symext::symex_allocate( return; // ignore exprt size = to_binary_expr(code).op0(); - optionalt object_type; + std::optional object_type; auto function_symbol = outer_symbol_table.lookup(state.source.function_id); INVARIANT(function_symbol, "function associated with allocation not found"); const irep_idt &mode = function_symbol->mode; @@ -341,7 +341,7 @@ static irep_idt get_string_argument(const exprt &src, const namespacet &ns) /// Return an expression if \p operands fulfills all criteria that we expect of /// the expression to be a variable argument list. -static optionalt get_va_args(const exprt::operandst &operands) +static std::optional get_va_args(const exprt::operandst &operands) { if(operands.size() != 2) return {}; @@ -379,7 +379,7 @@ void goto_symext::symex_printf( std::list args; // we either have any number of operands or a va_list as second operand - optionalt va_args = get_va_args(operands); + std::optional va_args = get_va_args(operands); if(!va_args.has_value()) { @@ -475,7 +475,7 @@ void goto_symext::symex_cpp_new( code.get(ID_statement) == ID_java_new_array_data); // value - optionalt type; + std::optional type; if(do_array) { exprt size_arg = diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index b0f82868f6e4..404f04fec723 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -72,13 +72,13 @@ void goto_symext::apply_goto_condition( /// \param symbol_expr: The symbol expression in the condition /// \param other_operand: The other expression in the condition; we only support /// an address of expression, a typecast of an address of expression or a -/// null pointer, and return an empty optionalt in all other cases +/// null pointer, and return an empty std::optional in all other cases /// \param value_set: The value-set for looking up what the symbol can point to /// \param language_mode: The language mode /// \param ns: A namespace /// \return If we were able to evaluate the condition as true or false then we -/// return that, otherwise we return an empty optionalt -static optionalt> try_evaluate_pointer_comparison( +/// return that, otherwise we return an empty std::optional +static std::optional> try_evaluate_pointer_comparison( const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, @@ -179,8 +179,8 @@ static optionalt> try_evaluate_pointer_comparison( /// \param language_mode: The language mode /// \param ns: A namespace /// \return If we were able to evaluate the condition as true or false then we -/// return that, otherwise we return an empty optionalt -static optionalt> try_evaluate_pointer_comparison( +/// return that, otherwise we return an empty std::optional +static std::optional> try_evaluate_pointer_comparison( const renamedt &renamed_expr, const value_sett &value_set, const irep_idt &language_mode, diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index bc1d420f71bd..ab929728998f 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -754,18 +754,18 @@ void goto_symext::kill_instruction_local_symbols(statet &state) /// multiple times) /// \param expr: The expression to examine /// \return If only one unique symbol occurs in \p expr then return it; -/// otherwise return an empty optionalt -static optionalt +/// otherwise return an empty std::optional +static std::optional find_unique_pointer_typed_symbol(const exprt &expr) { - optionalt return_value; + std::optional return_value; for(auto it = expr.depth_cbegin(); it != expr.depth_cend(); ++it) { const symbol_exprt *symbol_expr = expr_try_dynamic_cast(*it); if(symbol_expr && can_cast_type(symbol_expr->type())) { // If we already have a potential return value, check if it is the same - // symbol, and return an empty optionalt if not + // symbol, and return an empty std::optional if not if(return_value && *symbol_expr != *return_value) { return {}; @@ -789,7 +789,7 @@ void goto_symext::try_filter_value_sets( { condition = state.rename(std::move(condition), ns).get(); - optionalt symbol_expr = + std::optional symbol_expr = find_unique_pointer_typed_symbol(condition); if(!symbol_expr) diff --git a/src/goto-synthesizer/cegis_verifier.cpp b/src/goto-synthesizer/cegis_verifier.cpp index 176343c61526..483fe94019e1 100644 --- a/src/goto-synthesizer/cegis_verifier.cpp +++ b/src/goto-synthesizer/cegis_verifier.cpp @@ -546,7 +546,7 @@ void cegis_verifiert::restore_functions() } } -optionalt cegis_verifiert::verify() +std::optional cegis_verifiert::verify() { // This method does the following three things to verify the `goto_model` and // return a formatted counterexample if there is any violated property. @@ -617,7 +617,7 @@ optionalt cegis_verifiert::verify() if(result == resultt::PASS) { restore_functions(); - return optionalt(); + return std::optional(); } if(result == resultt::ERROR || result == resultt::UNKNOWN) @@ -660,7 +660,7 @@ optionalt cegis_verifiert::verify() if(target_violation == properties.end()) { restore_functions(); - return optionalt(); + return std::optional(); } target_violation_id = target_violation->first; diff --git a/src/goto-synthesizer/cegis_verifier.h b/src/goto-synthesizer/cegis_verifier.h index 481246a6688c..dc1e1aaa5be3 100644 --- a/src/goto-synthesizer/cegis_verifier.h +++ b/src/goto-synthesizer/cegis_verifier.h @@ -114,9 +114,9 @@ class cegis_verifiert { } - /// Verify `goto_model`. Return an empty `optionalt if there is no violation. - /// Otherwise, return the formatted counterexample. - optionalt verify(); + /// Verify `goto_model`. Return an empty `std::optional` if there is no + /// violation. Otherwise, return the formatted counterexample. + std::optional verify(); /// Result counterexample. propertiest properties; diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp index ece82ad55070..88432dfbf2dd 100644 --- a/src/linking/static_lifetime_init.cpp +++ b/src/linking/static_lifetime_init.cpp @@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -static optionalt static_lifetime_init( +static std::optional static_lifetime_init( const irep_idt &identifier, symbol_table_baset &symbol_table) { diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 000081db62e0..645ec3c27258 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -86,7 +86,7 @@ mp_integer gdb_value_extractort::get_malloc_size(irep_idt name) return scope_it->size(); } -optionalt gdb_value_extractort::get_malloc_pointee( +std::optional gdb_value_extractort::get_malloc_pointee( const memory_addresst &point, mp_integer member_size) { diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index 569c0f36fe6e..e37f6fe6765f 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -185,7 +185,7 @@ class gdb_value_extractort /// \param point: potentially dynamically allocated memory address /// \param member_size: size of each allocated element /// \return pointee as a string if we have a record of the allocation - optionalt + std::optional get_malloc_pointee(const memory_addresst &point, mp_integer member_size); /// Wrapper for call get_offset_pointer_bits diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index 3ad72ffda248..5cc6d4a27f2e 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -465,7 +465,7 @@ gdb_apit::pointer_valuet gdb_apit::get_memory(const std::string &expr) if(!b) return pointer_valuet{}; - optionalt opt_string; + std::optional opt_string; const std::string string = result[4]; if(!string.empty()) @@ -494,7 +494,7 @@ gdb_apit::pointer_valuet gdb_apit::get_memory(const std::string &expr) return pointer_valuet(result[1], result[2], result[3], opt_string, true); } -optionalt gdb_apit::get_value(const std::string &expr) +std::optional gdb_apit::get_value(const std::string &expr) { PRECONDITION(gdb_state == gdb_statet::STOPPED); diff --git a/src/memory-analyzer/gdb_api.h b/src/memory-analyzer/gdb_api.h index 6edff80a5367..f23c14c89aaf 100644 --- a/src/memory-analyzer/gdb_api.h +++ b/src/memory-analyzer/gdb_api.h @@ -79,7 +79,7 @@ class gdb_apit const std::string &address = "", const std::string &pointee = "", const std::string &character = "", - const optionalt &string = {}, + const std::optional &string = {}, const bool valid = false) : address(address), pointee(pointee), @@ -92,7 +92,7 @@ class gdb_apit memory_addresst address; std::string pointee; std::string character; - optionalt string; + std::optional string; bool has_known_offset() const { @@ -127,7 +127,7 @@ class gdb_apit /// \param expr: an expression of pointer type (e.g., `&x` with `x` being of /// type `int` or `p` with `p` being of type `int *`) /// \return memory address in hex format - optionalt get_value(const std::string &expr); + std::optional get_value(const std::string &expr); /// Get the value of a pointer associated with \p expr /// \param expr: the expression to be analyzed diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index 66f0739b9027..f53947a767b1 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -87,7 +87,7 @@ void add_failed_symbols(symbol_table_baset &symbol_table) add_failed_symbol_if_needed(*symbol, symbol_table); } -optionalt +std::optional get_failed_symbol(const symbol_exprt &expr, const namespacet &ns) { const symbolt &symbol=ns.lookup(expr); diff --git a/src/pointer-analysis/add_failed_symbols.h b/src/pointer-analysis/add_failed_symbols.h index d3b3ac49574a..c52a24b3e71d 100644 --- a/src/pointer-analysis/add_failed_symbols.h +++ b/src/pointer-analysis/add_failed_symbols.h @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_POINTER_ANALYSIS_ADD_FAILED_SYMBOLS_H #include -#include class symbol_table_baset; class symbolt; @@ -32,7 +31,7 @@ irep_idt failed_symbol_id(const irep_idt &identifier); /// \param ns: global namespace /// \return symbol expression for the failed-dereference symbol, or an empty /// optional if none exists. -optionalt +std::optional get_failed_symbol(const symbol_exprt &expr, const namespacet &ns); /// Return true if, and only if, \p expr is the result of failed dereferencing. diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 7a3543f5c2ad..ca0ef7a0cbbe 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -449,7 +449,7 @@ static std::string strip_first_field_from_suffix( return suffix.substr(field.length() + 1); } -optionalt value_sett::get_index_of_symbol( +std::optional value_sett::get_index_of_symbol( irep_idt identifier, const typet &type, const std::string &suffix, @@ -698,10 +698,10 @@ void value_sett::get_value_set_rec( throw expr.id_string()+" expected to have at least two operands"; object_mapt pointer_expr_set; - optionalt i; + std::optional i; // special case for plus/minus and exactly one pointer - optionalt ptr_operand; + std::optional ptr_operand; if( expr_type.id() == ID_pointer && (expr.id() == ID_plus || expr.id() == ID_minus)) diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h index 3d00dbf7e9c1..5c71946acd8b 100644 --- a/src/pointer-analysis/value_set.h +++ b/src/pointer-analysis/value_set.h @@ -78,7 +78,7 @@ class value_sett /// Represents the offset into an object: either a unique integer offset, /// or an unknown value, represented by `!offset`. - typedef optionalt offsett; + typedef std::optional offsett; /// Represents a set of expressions (`exprt` instances) with corresponding /// offsets (`offsett` instances). This is the RHS set of a single row of @@ -417,7 +417,7 @@ class value_sett /// \param ns: The global namespace, for following \p type if it is a /// struct tag type or a union tag type /// \return The index if the symbol is known, else `nullopt`. - optionalt get_index_of_symbol( + std::optional get_index_of_symbol( irep_idt identifier, const typet &type, const std::string &suffix, diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 924480fbe254..74ef37f4911c 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -103,8 +103,8 @@ static json_objectt value_set_dereference_stats_to_json( /// If `expr` is of the form (c1 ? e1[o1] : c2 ? e2[o2] : c3 ? ...) /// then return `c1 ? e1[o1 + offset] : e2[o2 + offset] : c3 ? ...` -/// otherwise return an empty optionalt. -static optionalt +/// otherwise return an empty std::optional. +static std::optional try_add_offset_to_indices(const exprt &expr, const exprt &offset_elements) { if(const auto *index_expr = expr_try_dynamic_cast(expr)) @@ -773,7 +773,7 @@ bool value_set_dereferencet::memory_model_bytes( auto from_type_element_type_size = from_type.id() == ID_array ? pointer_offset_size(to_array_type(from_type).element_type(), ns) - : optionalt{}; + : std::optional{}; auto to_type_size = pointer_offset_size(to_type, ns); diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h index 859a8fc38d54..8b3ad907ddec 100644 --- a/src/pointer-analysis/value_set_fi.h +++ b/src/pointer-analysis/value_set_fi.h @@ -57,7 +57,7 @@ class value_set_fit /// Represents the offset into an object: either a unique integer offset, /// or an unknown value, represented by `!offset`. - typedef optionalt offsett; + typedef std::optional offsett; bool offset_is_zero(const offsett &offset) const { return offset && offset->is_zero(); diff --git a/src/solvers/README.md b/src/solvers/README.md index 2a19e79f88b7..075bedb5355b 100644 --- a/src/solvers/README.md +++ b/src/solvers/README.md @@ -181,7 +181,7 @@ Note: `bvt` mentioned below is an alias to a vector of literalt. Which takes an exprt then calls the associated transformation functions to generate the \ref literalt vector to then pass to the internal \ref propt instance. -`const bvt & boolbvt::convert_bv(const exprt &expr, optionalt expected_width)` +`const bvt & boolbvt::convert_bv(const exprt &expr, std::optional expected_width)` Similar to convert_bitvector except it also provides basic caching and freezing results for incremental solving. It calls convert_bitvector diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 360f68f0f996..cfc6297791a9 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -715,7 +715,7 @@ void arrayst::add_array_constraints_array_constant( // We have a constant index - just pick the element at that index from the // array constant. - const optionalt i = + const std::optional i = numeric_cast(to_constant_expr(index)); // if the access is out of bounds, we leave it unconstrained if(!i.has_value() || *i >= operands.size()) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 1ee94ac9f54a..3f026d4b3b71 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -34,8 +34,9 @@ endianness_mapt boolbvt::endianness_map(const typet &type) const /// Convert expression to vector of literalts, using an internal /// cache to speed up conversion if available. Also assert the resultant /// vector is of a specific size, and freeze any elements if appropriate. -const bvt & -boolbvt::convert_bv(const exprt &expr, optionalt expected_width) +const bvt &boolbvt::convert_bv( + const exprt &expr, + std::optional expected_width) { // check cache first std::pair cache_result= diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 882a3eb1f8f8..fb88fa73fd76 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -59,7 +59,7 @@ class boolbvt:public arrayst virtual const bvt &convert_bv( // check cache const exprt &expr, - const optionalt expected_width = {}); + const std::optional expected_width = {}); virtual bvt convert_bitvector(const exprt &expr); // no cache diff --git a/src/solvers/flattening/boolbv_map.h b/src/solvers/flattening/boolbv_map.h index ee6b74259553..a9ba30630795 100644 --- a/src/solvers/flattening/boolbv_map.h +++ b/src/solvers/flattening/boolbv_map.h @@ -53,14 +53,15 @@ class boolbv_mapt const irep_idt &identifier, const typet &type); - optionalt> + std::optional> get_map_entry(const irep_idt &identifier) const { const auto entry = mapping.find(identifier); if(entry == mapping.end()) return {}; - return optionalt>(entry->second); + return std::optional>( + entry->second); } const mappingt &get_mapping() const diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index dcebd389089f..a32dd19a13b9 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -117,7 +117,7 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) const bvt &bv1 = convert_bv( expr.rhs(), can_cast_expr(expr) - ? optionalt{bv0.size()} + ? std::optional{bv0.size()} : std::nullopt); const bv_utilst::representationt rep = diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 0887966fb2c9..5ca7c77b243d 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -22,7 +22,7 @@ static bool expr_eq(const exprt &expr1, const exprt &expr2) /// To obtain the min value for the quantifier variable of the specified /// forall/exists operator. The min variable is in the form of "!(var_expr > /// constant)". -static optionalt +static std::optional get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr) { if(quantifier_expr.id()==ID_or) @@ -74,7 +74,7 @@ get_quantifier_var_min(const exprt &var_expr, const exprt &quantifier_expr) /// To obtain the max value for the quantifier variable of the specified /// forall/exists operator. -static optionalt +static std::optional get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) { if(quantifier_expr.id()==ID_or) @@ -149,7 +149,7 @@ get_quantifier_var_max(const exprt &var_expr, const exprt &quantifier_expr) return {}; } -static optionalt eager_quantifier_instantiation( +static std::optional eager_quantifier_instantiation( const quantifier_exprt &expr, const namespacet &ns) { @@ -199,9 +199,9 @@ static optionalt eager_quantifier_instantiation( UNREACHABLE; } - const optionalt min_i = + const std::optional min_i = get_quantifier_var_min(var_expr, where_simplified); - const optionalt max_i = + const std::optional max_i = get_quantifier_var_max(var_expr, where_simplified); if(!min_i.has_value() || !max_i.has_value()) diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h index 24c8909fe004..d6e66f75c099 100644 --- a/src/solvers/flattening/boolbv_width.h +++ b/src/solvers/flattening/boolbv_width.h @@ -28,7 +28,7 @@ class boolbv_widtht return entry_opt->total_width; } - virtual optionalt get_width_opt(const typet &type) const + virtual std::optional get_width_opt(const typet &type) const { const auto &entry_opt = get_entry(type); if(!entry_opt.has_value()) @@ -56,7 +56,7 @@ class boolbv_widtht std::size_t total_width; std::vector members; }; - using entryt = optionalt; + using entryt = std::optional; typedef std::unordered_map cachet; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index be28f5eef2e6..66af5ce4953d 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -231,7 +231,7 @@ bv_pointerst::bv_pointerst( { } -optionalt bv_pointerst::convert_address_of_rec(const exprt &expr) +std::optional bv_pointerst::convert_address_of_rec(const exprt &expr) { if(expr.id()==ID_symbol) { diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 151a1205c636..57958d2e9f3a 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -51,7 +51,7 @@ class bv_pointerst:public boolbvt exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override; - [[nodiscard]] optionalt convert_address_of_rec(const exprt &); + [[nodiscard]] std::optional convert_address_of_rec(const exprt &); [[nodiscard]] bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &); diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index b82ad7f342ba..7ca6632f1f5e 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -74,7 +74,7 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier) return literal; } -optionalt prop_conv_solvert::get_bool(const exprt &expr) const +std::optional prop_conv_solvert::get_bool(const exprt &expr) const { // trivial cases diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index ba41bc912224..a32ce9431883 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -110,7 +110,7 @@ class prop_conv_solvert : public conflict_providert, /// Get a _boolean_ value from the model if the formula is satisfiable. /// If the argument is not a boolean expression from the formula, /// {} is returned. - virtual optionalt get_bool(const exprt &expr) const; + virtual std::optional get_bool(const exprt &expr) const; virtual literalt convert_rest(const exprt &expr); virtual literalt convert_bool(const exprt &expr); diff --git a/src/solvers/smt2/smt2irep.cpp b/src/solvers/smt2/smt2irep.cpp index 14e75e16863a..9eeeb58921a7 100644 --- a/src/solvers/smt2/smt2irep.cpp +++ b/src/solvers/smt2/smt2irep.cpp @@ -22,13 +22,13 @@ class smt2irept:public smt2_tokenizert { } - optionalt operator()(); + std::optional operator()(); protected: messaget log; }; -optionalt smt2irept::operator()() +std::optional smt2irept::operator()() { try { @@ -88,7 +88,8 @@ optionalt smt2irept::operator()() } } -optionalt smt2irep(std::istream &in, message_handlert &message_handler) +std::optional +smt2irep(std::istream &in, message_handlert &message_handler) { return smt2irept(in, message_handler)(); } diff --git a/src/solvers/smt2/smt2irep.h b/src/solvers/smt2/smt2irep.h index f34ece51ba23..bc2a03748c3a 100644 --- a/src/solvers/smt2/smt2irep.h +++ b/src/solvers/smt2/smt2irep.h @@ -11,14 +11,13 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_SMT2_SMT2IREP_H #include - -#include +#include class irept; class message_handlert; /// returns an irep for an SMT-LIB2 expression read from a given stream /// returns {} when EOF is encountered before reading non-whitespace input -optionalt smt2irep(std::istream &, message_handlert &); +std::optional smt2irep(std::istream &, message_handlert &); #endif // CPROVER_SOLVERS_SMT2_SMT2IREP_H diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp index 39a0ec141474..4b88e8fad56f 100644 --- a/src/solvers/strings/array_pool.cpp +++ b/src/solvers/strings/array_pool.cpp @@ -44,7 +44,7 @@ exprt array_poolt::get_or_create_length(const array_string_exprt &s) return emplace_result.first->second; } -optionalt +std::optional array_poolt::get_length_if_exists(const array_string_exprt &s) const { auto find_result = length_of_array.find(s); diff --git a/src/solvers/strings/array_pool.h b/src/solvers/strings/array_pool.h index 99bb9a835132..fc210f76f5f3 100644 --- a/src/solvers/strings/array_pool.h +++ b/src/solvers/strings/array_pool.h @@ -68,7 +68,7 @@ class array_poolt final /// return an empty optional. /// \param s: array expression representing a string /// \return expression for the length of `s`, or empty optional - optionalt get_length_if_exists(const array_string_exprt &s) const; + std::optional get_length_if_exists(const array_string_exprt &s) const; void insert(const exprt &pointer_expr, const array_string_exprt &array); diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp index b3e08da91cc7..689818c4aaf4 100644 --- a/src/solvers/strings/string_builtin_function.cpp +++ b/src/solvers/strings/string_builtin_function.cpp @@ -21,7 +21,7 @@ string_transformation_builtin_functiont:: result = array_pool.find(fun_args[1], fun_args[0]); } -optionalt> eval_string( +std::optional> eval_string( const array_string_exprt &a, const std::function &get_value) { @@ -73,7 +73,7 @@ make_string(const std::vector &array, const array_typet &array_type) return make_string(array.begin(), array.end(), array_type); } -optionalt string_concat_char_builtin_functiont::eval( +std::optional string_concat_char_builtin_functiont::eval( const std::function &get_value) const { auto input_opt = eval_string(input, get_value); @@ -126,7 +126,7 @@ exprt string_concat_char_builtin_functiont::length_constraint() const return length_constraint_for_concat_char(result, input, array_pool); } -optionalt string_set_char_builtin_functiont::eval( +std::optional string_set_char_builtin_functiont::eval( const std::function &get_value) const { auto input_opt = eval_string(input, get_value); @@ -217,7 +217,7 @@ static bool eval_is_upper_case(const mp_integer &c) (0xd8 <= c && c <= 0xde); } -optionalt string_to_lower_case_builtin_functiont::eval( +std::optional string_to_lower_case_builtin_functiont::eval( const std::function &get_value) const { auto input_opt = eval_string(input, get_value); @@ -313,7 +313,7 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints( return constraints; } -optionalt string_to_upper_case_builtin_functiont::eval( +std::optional string_to_upper_case_builtin_functiont::eval( const std::function &get_value) const { auto input_opt = eval_string(input, get_value); @@ -380,7 +380,7 @@ string_creation_builtin_functiont::string_creation_builtin_functiont( arg = fun_args[2]; } -optionalt string_of_int_builtin_functiont::eval( +std::optional string_of_int_builtin_functiont::eval( const std::function &get_value) const { const auto arg_value = numeric_cast(get_value(arg)); diff --git a/src/solvers/strings/string_builtin_function.h b/src/solvers/strings/string_builtin_function.h index 510f909ee3bc..d515c7f46523 100644 --- a/src/solvers/strings/string_builtin_function.h +++ b/src/solvers/strings/string_builtin_function.h @@ -75,7 +75,7 @@ class string_builtin_functiont string_builtin_functiont(const string_builtin_functiont &) = delete; virtual ~string_builtin_functiont() = default; - virtual optionalt string_result() const + virtual std::optional string_result() const { return {}; } @@ -89,7 +89,7 @@ class string_builtin_functiont /// attempt to find the result of the builtin function. /// If not enough information can be gathered from `get_value`, return an /// empty optional. - virtual optionalt + virtual std::optional eval(const std::function &get_value) const = 0; virtual std::string name() const = 0; @@ -154,7 +154,7 @@ class string_transformation_builtin_functiont : public string_builtin_functiont const std::vector &fun_args, array_poolt &array_pool); - optionalt string_result() const override + std::optional string_result() const override { return result; } @@ -189,7 +189,7 @@ class string_concat_char_builtin_functiont character = fun_args[3]; } - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override @@ -227,7 +227,7 @@ class string_set_char_builtin_functiont character = fun_args[4]; } - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override @@ -258,7 +258,7 @@ class string_to_lower_case_builtin_functiont { } - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override @@ -307,7 +307,7 @@ class string_to_upper_case_builtin_functiont { } - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override @@ -348,7 +348,7 @@ class string_creation_builtin_functiont : public string_builtin_functiont const std::vector &fun_args, array_poolt &array_pool); - optionalt string_result() const override + std::optional string_result() const override { return result; } @@ -376,7 +376,7 @@ class string_of_int_builtin_functiont : public string_creation_builtin_functiont radix = from_integer(10, arg.type()); }; - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override @@ -415,7 +415,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont { public: function_application_exprt function_application; - optionalt string_res; + std::optional string_res; std::vector string_args; std::vector args; @@ -434,12 +434,12 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont { return std::vector(string_args); } - optionalt string_result() const override + std::optional string_result() const override { return string_res; } - optionalt + std::optional eval(const std::function &) const override { return {}; @@ -460,7 +460,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont /// Given a function `get_value` which gives a valuation to expressions, attempt /// to find the current value of the array `a`. If the valuation of some /// characters are missing, then return an empty optional. -optionalt> eval_string( +std::optional> eval_string( const array_string_exprt &a, const std::function &get_value); diff --git a/src/solvers/strings/string_constraint_generator.h b/src/solvers/strings/string_constraint_generator.h index 1e36064f49f7..f439e5f28b3b 100644 --- a/src/solvers/strings/string_constraint_generator.h +++ b/src/solvers/strings/string_constraint_generator.h @@ -67,7 +67,7 @@ class string_constraint_generatort final /// Associate array to pointer, and array to length /// \return an expression if the given function application is one of /// associate pointer and associate length - optionalt make_array_pointer_association( + std::optional make_array_pointer_association( const exprt &return_code, const function_application_exprt &expr); diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp index acc8d874059a..33dcb782a024 100644 --- a/src/solvers/strings/string_constraint_generator_main.cpp +++ b/src/solvers/strings/string_constraint_generator_main.cpp @@ -192,7 +192,8 @@ static irep_idt get_function_name(const function_application_exprt &expr) return to_symbol_expr(name).get_identifier(); } -optionalt string_constraint_generatort::make_array_pointer_association( +std::optional +string_constraint_generatort::make_array_pointer_association( const exprt &return_code, const function_application_exprt &expr) { diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp index 6d82b14307dd..fc33eaec8615 100644 --- a/src/solvers/strings/string_constraint_generator_transformation.cpp +++ b/src/solvers/strings/string_constraint_generator_transformation.cpp @@ -269,7 +269,7 @@ string_constraint_generatort::add_axioms_for_trim( /// not primitive chars. /// \param array_pool: pool of arrays representing strings /// \return Optional pair of two expressions -static optionalt> to_char_pair( +static std::optional> to_char_pair( exprt expr1, exprt expr2, std::function get_string_expr, diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp index ccc02c05e481..039557734a1f 100644 --- a/src/solvers/strings/string_constraint_generator_valueof.cpp +++ b/src/solvers/strings/string_constraint_generator_valueof.cpp @@ -421,7 +421,7 @@ string_constraint_generatort::add_axioms_for_characters_in_integer_string( // a digit, which is `max_string_length - 2` because of the space left for // a minus sign. That assumes that we were able to identify the radix. If we // weren't then we check for overflow on every index. - optionalt no_overflow; + std::optional no_overflow; if(size - 1 >= max_string_length - 2 || radix_ul == 0) { no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)), diff --git a/src/solvers/strings/string_dependencies.cpp b/src/solvers/strings/string_dependencies.cpp index 2a0ab220886d..17a5105c8f88 100644 --- a/src/solvers/strings/string_dependencies.cpp +++ b/src/solvers/strings/string_dependencies.cpp @@ -165,7 +165,7 @@ static void add_dependency_to_string_subexprs( } } -optionalt string_dependenciest::eval( +std::optional string_dependenciest::eval( const array_string_exprt &s, const std::function &get_value) const { @@ -194,7 +194,7 @@ void string_dependenciest::clean_cache() e.reset(); } -optionalt add_node( +std::optional add_node( string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, diff --git a/src/solvers/strings/string_dependencies.h b/src/solvers/strings/string_dependencies.h index 68b30868bc18..eac3cf3219ab 100644 --- a/src/solvers/strings/string_dependencies.h +++ b/src/solvers/strings/string_dependencies.h @@ -64,7 +64,7 @@ class string_dependenciest // \todo should these we shared pointers? std::vector dependencies; // builtin function of which it is the result - optionalt result_from; + std::optional result_from; explicit string_nodet(array_string_exprt e, const std::size_t index) : expr(std::move(e)), index(index) @@ -101,7 +101,7 @@ class string_dependenciest /// of strings on which it depends /// Warning: eval uses a cache which must be cleaned everytime the valuations /// given by get_value can change. - optionalt eval( + std::optional eval( const array_string_exprt &s, const std::function &get_value) const; @@ -169,7 +169,7 @@ class string_dependenciest } }; - mutable std::vector> eval_string_cache; + mutable std::vector> eval_string_cache; /// Applies `f` on all nodes void for_each_node(const std::function &f) const; @@ -197,7 +197,7 @@ class string_dependenciest /// builtin function. Or an empty optional when no function applications has /// been encountered /// \todo there should be a class with just the three functions we require here -optionalt add_node( +std::optional add_node( string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index c8f07ab666b6..20ce1f8ab2a1 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -516,7 +516,7 @@ static std::vector eval_format_specifier( INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]"); } -optionalt string_format_builtin_functiont::eval( +std::optional string_format_builtin_functiont::eval( const std::function &get_value) const { if(!format_string.has_value()) diff --git a/src/solvers/strings/string_format_builtin_function.h b/src/solvers/strings/string_format_builtin_function.h index 0b2d1112542d..62d8a02eae99 100644 --- a/src/solvers/strings/string_format_builtin_function.h +++ b/src/solvers/strings/string_format_builtin_function.h @@ -65,7 +65,7 @@ class string_format_builtin_functiont final : public string_builtin_functiont array_string_exprt result; /// Only set when the format string is a constant. In the other case, the /// result will be non-deterministic - optionalt format_string; + std::optional format_string; std::vector inputs; /// Constructor from arguments of a function application. @@ -78,7 +78,7 @@ class string_format_builtin_functiont final : public string_builtin_functiont const std::vector &fun_args, array_poolt &array_pool); - optionalt string_result() const override + std::optional string_result() const override { return result; } @@ -88,7 +88,7 @@ class string_format_builtin_functiont final : public string_builtin_functiont return inputs; } - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override diff --git a/src/solvers/strings/string_insertion_builtin_function.cpp b/src/solvers/strings/string_insertion_builtin_function.cpp index 626097580850..3135fddf276e 100644 --- a/src/solvers/strings/string_insertion_builtin_function.cpp +++ b/src/solvers/strings/string_insertion_builtin_function.cpp @@ -62,7 +62,7 @@ std::vector string_insertion_builtin_functiont::eval( return eval_result; } -optionalt string_insertion_builtin_functiont::eval( +std::optional string_insertion_builtin_functiont::eval( const std::function &get_value) const { const auto &input1_value = eval_string(input1, get_value); diff --git a/src/solvers/strings/string_insertion_builtin_function.h b/src/solvers/strings/string_insertion_builtin_function.h index 877d764aa2f5..fbf03d38d53e 100644 --- a/src/solvers/strings/string_insertion_builtin_function.h +++ b/src/solvers/strings/string_insertion_builtin_function.h @@ -31,7 +31,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont const std::vector &fun_args, array_poolt &array_pool); - optionalt string_result() const override + std::optional string_result() const override { return result; } @@ -46,7 +46,7 @@ class string_insertion_builtin_functiont : public string_builtin_functiont const std::vector &input2_value, const std::vector &args_value) const; - optionalt + std::optional eval(const std::function &get_value) const override; std::string name() const override diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 155598dac6df..45cd53fffba2 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -40,7 +40,7 @@ static bool is_valid_string_constraint( const namespacet &ns, const string_constraintt &constraint); -static optionalt find_counter_example( +static std::optional find_counter_example( const namespacet &ns, const exprt &axiom, const symbol_exprt &var, @@ -106,14 +106,14 @@ static std::vector instantiate( const std::unordered_map &witnesses); -static optionalt get_array( +static std::optional get_array( const std::function &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool); -static optionalt substitute_array_access( +static std::optional substitute_array_access( const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate); @@ -686,7 +686,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() // in the graph. const exprt eq_with_char_array_replaced_with_representative_elements = replace_expr_copy(symbol_resolve, eq); - const optionalt new_equation = add_node( + const std::optional new_equation = add_node( dependencies, eq_with_char_array_replaced_with_representative_elements, generator.array_pool, @@ -954,7 +954,7 @@ void string_refinementt::add_lemma( /// \param array_pool: pool of arrays representing strings /// \return an optional expression representing the size of the array that can /// be cast to size_t -static optionalt get_valid_array_size( +static std::optional get_valid_array_size( const std::function &super_get, const namespacet &ns, messaget::mstreamt &stream, @@ -998,7 +998,7 @@ static optionalt get_valid_array_size( /// \param arr: expression of type array representing a string /// \param array_pool: pool of arrays representing strings /// \return an optional array expression or array_of_exprt -static optionalt get_array( +static std::optional get_array( const std::function &super_get, const namespacet &ns, messaget::mstreamt &stream, @@ -1188,9 +1188,9 @@ static exprt substitute_array_access( exprt false_index = index_exprt(if_expr.false_case(), index); // Substitute recursively in branches of conditional expressions - optionalt substituted_true_case = + std::optional substituted_true_case = substitute_array_access(true_index, symbol_generator, left_propagate); - optionalt substituted_false_case = + std::optional substituted_false_case = substitute_array_access(false_index, symbol_generator, left_propagate); return if_exprt( @@ -1199,7 +1199,7 @@ static exprt substitute_array_access( substituted_false_case ? *substituted_false_case : false_index); } -static optionalt substitute_array_access( +static std::optional substitute_array_access( const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate) @@ -1238,7 +1238,7 @@ static void substitute_array_access_in_place( { if(const auto index_expr = expr_try_dynamic_cast(*it)) { - optionalt result = + std::optional result = substitute_array_access(*index_expr, symbol_generator, left_propagate); // Only perform a write when we have something changed. @@ -1904,7 +1904,7 @@ exprt string_refinementt::get(const exprt &expr) const /// \param message_handler: message handler /// \return the witness of the satisfying assignment if one /// exists. If UNSAT, then behaviour is undefined. -static optionalt find_counter_example( +static std::optional find_counter_example( const namespacet &ns, const exprt &axiom, const symbol_exprt &var, diff --git a/src/solvers/strings/string_refinement_util.cpp b/src/solvers/strings/string_refinement_util.cpp index e916d2804357..db1cc2a57c18 100644 --- a/src/solvers/strings/string_refinement_util.cpp +++ b/src/solvers/strings/string_refinement_util.cpp @@ -154,7 +154,7 @@ interval_sparse_arrayt::interval_sparse_arrayt( } } -optionalt +std::optional interval_sparse_arrayt::of_expr(const exprt &expr, const exprt &extra_value) { if(const auto &array_expr = expr_try_dynamic_cast(expr)) diff --git a/src/solvers/strings/string_refinement_util.h b/src/solvers/strings/string_refinement_util.h index adabff4287d6..f7531df0233e 100644 --- a/src/solvers/strings/string_refinement_util.h +++ b/src/solvers/strings/string_refinement_util.h @@ -122,7 +122,7 @@ class interval_sparse_arrayt final : public sparse_arrayt /// If the expression is an array_exprt or a with_exprt uses the appropriate /// constructor, otherwise returns empty optional. - static optionalt + static std::optional of_expr(const exprt &expr, const exprt &extra_value); /// Convert to an array representation, ignores elements at index >= size diff --git a/src/statement-list/statement_list_parse_tree.h b/src/statement-list/statement_list_parse_tree.h index 406b4b5acbf4..4f5e8efcd1f7 100644 --- a/src/statement-list/statement_list_parse_tree.h +++ b/src/statement-list/statement_list_parse_tree.h @@ -31,7 +31,7 @@ class statement_list_parse_treet /// Representation of the variable, including identifier and type. symbol_exprt variable; /// Optional default value of the variable. - optionalt default_value; + std::optional default_value; /// Creates a new. variable declaration. /// \param symbol: The variable, including type and name. @@ -58,7 +58,7 @@ class statement_list_parse_treet /// and may contain zero or more instructions. struct networkt { - optionalt title; + std::optional title; instructionst instructions; /// Sets the title of the network to a specific value. diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h index d5aa518b05d5..cfebbce7795d 100644 --- a/src/util/arith_tools.h +++ b/src/util/arith_tools.h @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "invariant.h" #include "mp_arith.h" -#include "optional.h" #include "std_expr.h" #include @@ -37,7 +36,7 @@ struct numeric_castt final template <> struct numeric_castt final { - optionalt operator()(const exprt &expr) const + std::optional operator()(const exprt &expr) const { if(!expr.is_constant()) return {}; @@ -45,7 +44,7 @@ struct numeric_castt final return operator()(to_constant_expr(expr)); } - optionalt operator()(const constant_exprt &expr) const + std::optional operator()(const constant_exprt &expr) const { mp_integer out; if(to_integer(expr, out)) @@ -79,7 +78,7 @@ struct numeric_castt operator()(const mp_integer &mpi) const + std::optional operator()(const mp_integer &mpi) const { static_assert( std::numeric_limits::max() <= @@ -98,7 +97,7 @@ struct numeric_castt operator()(const exprt &expr) const + std::optional operator()(const exprt &expr) const { if(expr.is_constant()) return numeric_castt{}(to_constant_expr(expr)); @@ -107,7 +106,7 @@ struct numeric_castt operator()(const constant_exprt &expr) const + std::optional operator()(const constant_exprt &expr) const { if(auto mpi_opt = numeric_castt{}(expr)) return numeric_castt{}(*mpi_opt); @@ -122,7 +121,7 @@ struct numeric_castt -optionalt numeric_cast(const exprt &arg) +std::optional numeric_cast(const exprt &arg) { return numeric_castt{}(arg); } diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index 8e24f1dd8255..2b18e322f59c 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -296,12 +296,12 @@ std::string c_type_as_string(const irep_idt &c_type) return ""; } -optionalt> +std::optional> union_typet::find_widest_union_component(const namespacet &ns) const { const union_typet::componentst &comps = components(); - optionalt max_width; + std::optional max_width; typet max_comp_type; irep_idt max_comp_name; diff --git a/src/util/c_types.h b/src/util/c_types.h index 00d75bf45d2a..7fbad42c8008 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -160,7 +160,7 @@ class union_typet : public struct_union_typet /// \param ns: Namespace to resolve tag types. /// \return Pair of a componentt pointing to the maximum fixed bit-width /// member of the union type and the bit width of that member. - optionalt> + std::optional> find_widest_union_component(const namespacet &ns) const; }; diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp index 84530430ae1a..a22b5e8b0e75 100644 --- a/src/util/cmdline.cpp +++ b/src/util/cmdline.cpp @@ -132,22 +132,22 @@ cmdlinet::get_comma_separated_values(const char *option) const return separated_values; } -optionalt cmdlinet::getoptnr(char option) const +std::optional cmdlinet::getoptnr(char option) const { for(std::size_t i=0; i(); + return std::optional(); } -optionalt cmdlinet::getoptnr(const std::string &option) const +std::optional cmdlinet::getoptnr(const std::string &option) const { for(std::size_t i=0; i(); + return std::optional(); } bool cmdlinet::parse(int argc, const char **argv, const char *optstring) @@ -274,7 +274,7 @@ bool cmdlinet::parse_arguments(int argc, const char **argv) args.push_back(argv[i]); else { - optionalt optnr; + std::optional optnr; if(argv[i][1] != 0 && argv[i][2] == 0) optnr = getoptnr(argv[i][1]); // single-letter option -X diff --git a/src/util/cmdline.h b/src/util/cmdline.h index b5f688796381..bc624f678e18 100644 --- a/src/util/cmdline.h +++ b/src/util/cmdline.h @@ -12,11 +12,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include -#include "optional.h" - class cmdlinet { public: @@ -190,8 +189,8 @@ class cmdlinet std::vector options; - optionalt getoptnr(char option) const; - optionalt getoptnr(const std::string &option) const; + std::optional getoptnr(char option) const; + std::optional getoptnr(const std::string &option) const; }; #endif // CPROVER_UTIL_CMDLINE_H diff --git a/src/util/config.h b/src/util/config.h index 7a58e41918ad..0bfedadc627f 100644 --- a/src/util/config.h +++ b/src/util/config.h @@ -9,11 +9,11 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_CONFIG_H #define CPROVER_UTIL_CONFIG_H -#include - #include "ieee_float.h" #include "irep.h" -#include "optional.h" + +#include +#include class cmdlinet; class symbol_table_baset; @@ -287,7 +287,7 @@ class configt /// Maximum value of argc, which is operating-systems dependent: Windows /// limits the number of characters accepte by CreateProcess, and Unix /// systems have sysconf(ARG_MAX). - optionalt max_argc; + std::optional max_argc; } ansi_c; struct cppt @@ -348,7 +348,7 @@ class configt } bv_encoding; // this is the function to start executing - optionalt main; + std::optional main; void set_arch(const irep_idt &); diff --git a/src/util/dense_integer_map.h b/src/util/dense_integer_map.h index aafcc9201071..8160d80d079d 100644 --- a/src/util/dense_integer_map.h +++ b/src/util/dense_integer_map.h @@ -17,7 +17,6 @@ Author: Diffblue Ltd #include #include -#include /// Identity functor. When we use C++20 this can be replaced with std::identity. class identity_functort @@ -41,10 +40,11 @@ class identity_functort /// /// The type is optimised for fast lookups at the expense of flexibility. /// It makes one compromise on the iterface of std::map / unordered_map: the -/// iterator refers to a pair>, where the value optional -/// will always be defined. This is because the backing store uses optionalt -/// this way and we don't want to impose the price of copying the key and value -/// each time we move the iterator just so we have a & to give out. +/// iterator refers to a pair>, where the value +/// optional will always be defined. This is because the backing store uses +/// std::optional this way and we don't want to impose the price of copying the +/// key and value each time we move the iterator just so we have a +/// & to give out. /// /// Undocumented functions with matching names have the same semantics as /// std::map equivalents (including perfect iterator stability, with ordering @@ -71,8 +71,8 @@ class dense_integer_mapt // Indicates whether a given position in \ref map's value has been set, and // therefore whether our iterators should stop at a given location. We use - // this auxiliary structure rather than `pair>` in \ref map - // because this way we can more easily return a std::map-like + // this auxiliary structure rather than `pair>` in + // \ref map because this way we can more easily return a std::map-like // std::pair & from the iterator. std::vector value_set; diff --git a/src/util/edit_distance.cpp b/src/util/edit_distance.cpp index b2361ed6ba8d..9f0a73c360c2 100644 --- a/src/util/edit_distance.cpp +++ b/src/util/edit_distance.cpp @@ -54,7 +54,7 @@ bool levenshtein_automatont::matches(const std::string &string) const return get_edit_distance(string).has_value(); } -optionalt +std::optional levenshtein_automatont::get_edit_distance(const std::string &string) const { auto current = nfa.initial_state(0); diff --git a/src/util/edit_distance.h b/src/util/edit_distance.h index 2d72586ec795..7d9e1a2a4a99 100644 --- a/src/util/edit_distance.h +++ b/src/util/edit_distance.h @@ -15,10 +15,9 @@ #include "nfa.h" #include +#include #include -#include - /// Simple automaton that can detect whether a string can be transformed into /// another with a limited number of deletions, insertions or substitutions. /// Not a very fast implementation, but should be good enough for small strings. @@ -35,7 +34,7 @@ struct levenshtein_automatont std::size_t allowed_errors = 2); bool matches(const std::string &string) const; - optionalt get_edit_distance(const std::string &string) const; + std::optional get_edit_distance(const std::string &string) const; void dump_automaton_dot_to(std::ostream &out) { diff --git a/src/util/expr_cast.h b/src/util/expr_cast.h index 52992f0c5ea7..c568692366e3 100644 --- a/src/util/expr_cast.h +++ b/src/util/expr_cast.h @@ -101,10 +101,10 @@ auto expr_try_dynamic_cast(TExpr &base) /// \tparam T: The type to cast the \p base param to. /// \tparam TType: The original type to cast from, must be a exprt rvalue. /// \param base: A generic \ref exprt rvalue. -/// \return Cast value in an optionalt or empty if \a base is not an instance -/// of T. +/// \return Cast value in an std::optional or empty if \a base is not an +/// instance of T. template -optionalt expr_try_dynamic_cast(TExpr &&base) +std::optional expr_try_dynamic_cast(TExpr &&base) { static_assert( std::is_rvalue_reference::value, @@ -118,7 +118,7 @@ optionalt expr_try_dynamic_cast(TExpr &&base) static_assert(!std::is_const::value, "Attempted to move from const."); if(!can_cast_expr(base)) return {}; - optionalt ret{static_cast(base)}; + std::optional ret{static_cast(base)}; validate_expr(*ret); return ret; } @@ -153,10 +153,10 @@ auto type_try_dynamic_cast(TType &base) -> /// \tparam T: The type to cast the \p base param to. /// \tparam TType: The original type to cast from, must be a typet rvalue. /// \param base: A generic \ref typet rvalue. -/// \return Cast value in an optionalt or empty if \a base is not an instance -/// of T. +/// \return Cast value in an std::optional or empty if \a base is not an +/// instance of T. template -optionalt type_try_dynamic_cast(TType &&base) +std::optional type_try_dynamic_cast(TType &&base) { static_assert( std::is_rvalue_reference::value, @@ -171,7 +171,7 @@ optionalt type_try_dynamic_cast(TType &&base) if(!can_cast_type(base)) return {}; TType::check(base); - optionalt ret{static_cast(base)}; + std::optional ret{static_cast(base)}; return ret; } diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 2cd605253b25..3525b2804e12 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -29,7 +29,7 @@ class expr_initializert { } - optionalt operator()( + std::optional operator()( const typet &type, const source_locationt &source_location, const exprt &init_expr) @@ -40,13 +40,13 @@ class expr_initializert protected: const namespacet &ns; - optionalt expr_initializer_rec( + std::optional expr_initializer_rec( const typet &type, const source_locationt &source_location, const exprt &init_expr); }; -optionalt expr_initializert::expr_initializer_rec( +std::optional expr_initializert::expr_initializer_rec( const typet &type, const source_locationt &source_location, const exprt &init_expr) @@ -305,7 +305,7 @@ optionalt expr_initializert::expr_initializer_rec( /// \param ns: Namespace to perform type symbol/tag lookups. /// \return An expression if a constant expression of the input type can be /// built. -optionalt zero_initializer( +std::optional zero_initializer( const typet &type, const source_locationt &source_location, const namespacet &ns) @@ -321,7 +321,7 @@ optionalt zero_initializer( /// \param ns: Namespace to perform type symbol/tag lookups. /// \return An expression if a non-deterministic expression of the input type /// can be built. -optionalt nondet_initializer( +std::optional nondet_initializer( const typet &type, const source_locationt &source_location, const namespacet &ns) @@ -337,7 +337,7 @@ optionalt nondet_initializer( /// \param init_byte_expr: Value to be used for initialization. /// \return An expression if a byte-initialized expression of the input type /// can be built. -optionalt expr_initializer( +std::optional expr_initializer( const typet &type, const source_locationt &source_location, const namespacet &ns, diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h index f9421ef56e5d..4a3c8ee67de9 100644 --- a/src/util/expr_initializer.h +++ b/src/util/expr_initializer.h @@ -12,22 +12,22 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_EXPR_INITIALIZER_H #define CPROVER_UTIL_EXPR_INITIALIZER_H -#include "optional.h" +#include class exprt; class namespacet; class source_locationt; class typet; -optionalt +std::optional zero_initializer(const typet &, const source_locationt &, const namespacet &); -optionalt nondet_initializer( +std::optional nondet_initializer( const typet &type, const source_locationt &source_location, const namespacet &ns); -optionalt expr_initializer( +std::optional expr_initializer( const typet &type, const source_locationt &source_location, const namespacet &ns, diff --git a/src/util/interval_union.cpp b/src/util/interval_union.cpp index ef342d2fc382..239ac7a161d4 100644 --- a/src/util/interval_union.cpp +++ b/src/util/interval_union.cpp @@ -149,7 +149,7 @@ bool interval_uniont::is_empty() const return intervals.empty(); } -optionalt interval_uniont::maximum() const +std::optional interval_uniont::maximum() const { if(intervals.empty()) return {}; @@ -159,7 +159,7 @@ optionalt interval_uniont::maximum() const return {}; } -optionalt interval_uniont::minimum() const +std::optional interval_uniont::minimum() const { if(intervals.empty()) return {}; @@ -213,7 +213,7 @@ interval_uniont::of_interval(interval_uniont::intervalt interval) return result; } -optionalt +std::optional interval_uniont::of_string(const std::string &to_parse) { const std::regex limits_regex("\\[(-\\d+|\\d*):(-\\d+|\\d*)\\]"); @@ -235,7 +235,7 @@ interval_uniont::of_string(const std::string &to_parse) return result; } -optionalt interval_uniont::as_singleton() const +std::optional interval_uniont::as_singleton() const { if(intervals.size() != 1) return {}; diff --git a/src/util/interval_union.h b/src/util/interval_union.h index d4ddf1aee936..ea535e110bd1 100644 --- a/src/util/interval_union.h +++ b/src/util/interval_union.h @@ -14,7 +14,8 @@ Author: Diffblue Limited #include #include -#include + +#include #include class exprt; @@ -54,11 +55,11 @@ class interval_uniont /// empty optional means either unbounded on the right or empty, /// \ref is_empty has to be called to distinguish between the two - optionalt maximum() const; + std::optional maximum() const; /// empty optional means either unbounded on the left or empty, /// \ref is_empty has to be called to distinguish between the two - optionalt minimum() const; + std::optional minimum() const; /// Convert the set to a string representing a sequence of intervals, each /// interval being of the form "[lower:upper]", "[:upper]" if there is no @@ -69,7 +70,7 @@ class interval_uniont /// Parse a string which is a comma `,` separated list of intervals of the /// form "[lower1:upper1]", for example: "[-3:-2],[4:5]". /// Return an empty optional if the string doesn't match the format. - static optionalt of_string(const std::string &to_parse); + static std::optional of_string(const std::string &to_parse); /// Construct interval union from a single interval static interval_uniont of_interval(intervalt interval); @@ -78,7 +79,7 @@ class interval_uniont exprt make_contains_expr(const exprt &e) const; /// If the set contains only one element, return the value of this element. - optionalt as_singleton() const; + std::optional as_singleton() const; private: /// Non-overlapping intervals stored in order of their lower bound, so that diff --git a/src/util/lazy.h b/src/util/lazy.h index 46458200e40a..eb903db69a0a 100644 --- a/src/util/lazy.h +++ b/src/util/lazy.h @@ -10,7 +10,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #define CPROVER_UTIL_LAZY_H #include -#include template class lazyt @@ -34,7 +33,7 @@ class lazyt } private: - optionalt value; + std::optional value; std::function evaluation_function; explicit lazyt(std::function fun) diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 37c7fb9ee693..a9dc5e4213f7 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -409,8 +409,8 @@ static exprt bv_to_expr( static exprt unpack_rec( const exprt &src, bool little_endian, - const optionalt &offset_bytes, - const optionalt &max_bytes, + const std::optional &offset_bytes, + const std::optional &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array = false); @@ -537,11 +537,11 @@ static exprt unpack_array_vector_no_known_bounds( /// \return Array expression holding unpacked elements or array comprehension static exprt unpack_array_vector( const exprt &src, - const optionalt &src_size, + const std::optional &src_size, const mp_integer &element_bits, bool little_endian, - const optionalt &offset_bytes, - const optionalt &max_bytes, + const std::optional &offset_bytes, + const std::optional &max_bytes, const std::size_t bits_per_byte, const namespacet &ns) { @@ -562,7 +562,7 @@ static exprt unpack_array_vector( // refine the number of elements to extract in case the element width is known // and a multiple of bytes; otherwise we will expand the entire array/vector - optionalt num_elements = src_size; + std::optional num_elements = src_size; if(element_bits > 0 && element_bits % bits_per_byte == 0) { if(!num_elements.has_value()) @@ -614,10 +614,10 @@ static exprt unpack_array_vector( // recursively unpack each element so that we eventually just have an array // of bytes left - const optionalt element_max_bytes = + const std::optional element_max_bytes = max_bytes ? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size()) - : optionalt{}; + : std::optional{}; const std::size_t element_max_bytes_int = element_max_bytes ? numeric_cast_v(*element_max_bytes) : el_bytes; @@ -655,8 +655,8 @@ static void process_bit_fields( std::size_t total_bits, exprt::operandst &dest, bool little_endian, - const optionalt &offset_bytes, - const optionalt &max_bytes, + const std::optional &offset_bytes, + const std::optional &max_bytes, const std::size_t bits_per_byte, const namespacet &ns) { @@ -691,17 +691,17 @@ static void process_bit_fields( static array_exprt unpack_struct( const exprt &src, bool little_endian, - const optionalt &offset_bytes, - const optionalt &max_bytes, + const std::optional &offset_bytes, + const std::optional &max_bytes, const std::size_t bits_per_byte, const namespacet &ns) { const struct_typet &struct_type = to_struct_type(ns.follow(src.type())); const struct_typet::componentst &components = struct_type.components(); - optionalt offset_in_member; - optionalt max_bytes_left; - optionalt> bit_fields; + std::optional offset_in_member; + std::optional max_bytes_left; + std::optional> bit_fields; mp_integer member_offset_bits = 0; exprt::operandst byte_operands; @@ -895,8 +895,8 @@ static array_exprt unpack_complex( static exprt unpack_rec( const exprt &src, bool little_endian, - const optionalt &offset_bytes, - const optionalt &max_bytes, + const std::optional &offset_bytes, + const std::optional &max_bytes, const std::size_t bits_per_byte, const namespacet &ns, bool unpack_byte_array) @@ -1102,7 +1102,7 @@ static exprt lower_byte_extract_array_vector( const mp_integer &element_bits, const namespacet &ns) { - optionalt num_elements; + std::optional num_elements; if(src.type().id() == ID_array) num_elements = numeric_cast(to_array_type(src.type()).size()); else @@ -1176,7 +1176,7 @@ static exprt lower_byte_extract_array_vector( /// \param ns: Namespace /// \return An expression if the subtype size is known, else `nullopt` so that a /// fall-back to more generic code can be used. -static optionalt lower_byte_extract_complex( +static std::optional lower_byte_extract_complex( const byte_extract_exprt &src, const byte_extract_exprt &unpacked, const namespacet &ns) @@ -1380,8 +1380,8 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) const exprt &root = unpacked.op(); const exprt &offset = unpacked.offset(); - optionalt subtype; - optionalt index_type; + std::optional subtype; + std::optional index_type; if(root.type().id() == ID_vector) { subtype = to_vector_type(root.type()).element_type(); @@ -1464,7 +1464,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) static exprt lower_byte_update( const byte_update_exprt &src, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns); /// Apply a byte update \p src to an array/vector of bytes using the byte-array @@ -1549,7 +1549,7 @@ static exprt lower_byte_update_byte_array_vector( const byte_update_exprt &src, const typet &subtype, const array_exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { PRECONDITION( @@ -1765,7 +1765,7 @@ static exprt lower_byte_update_array_vector_non_const( const byte_update_exprt &src, const typet &subtype, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { // do all arithmetic below using index/offset types - the array theory @@ -1918,7 +1918,7 @@ static exprt lower_byte_update_single_element( const mp_integer &subtype_bits, const mp_integer &bits_already_set, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { // We need to take one or more bytes from value_as_byte_array to modify the @@ -2048,7 +2048,7 @@ static exprt lower_byte_update_single_element( new_value, src.get_bits_per_byte()}; - optionalt update_bound; + std::optional update_bound; if(non_const_update_bound.has_value()) { // The size of the update is not constant, and thus is to be symbolically @@ -2091,9 +2091,9 @@ static exprt lower_byte_update_single_element( static exprt lower_byte_update_array_vector( const byte_update_exprt &src, const typet &subtype, - const optionalt &subtype_bits, + const std::optional &subtype_bits, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { const bool is_array = src.type().id() == ID_array; @@ -2176,7 +2176,7 @@ static exprt lower_byte_update_struct( const byte_update_exprt &src, const struct_typet &struct_type, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { exprt::operandst elements; @@ -2280,7 +2280,7 @@ static exprt lower_byte_update_union( const byte_update_exprt &src, const union_typet &union_type, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { const auto widest_member = union_type.find_widest_union_component(ns); @@ -2311,12 +2311,12 @@ static exprt lower_byte_update_union( static exprt lower_byte_update( const byte_update_exprt &src, const exprt &value_as_byte_array, - const optionalt &non_const_update_bound, + const std::optional &non_const_update_bound, const namespacet &ns) { if(src.type().id() == ID_array || src.type().id() == ID_vector) { - optionalt subtype; + std::optional subtype; if(src.type().id() == ID_vector) subtype = to_vector_type(src.type()).element_type(); else @@ -2558,7 +2558,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) // use a "with" expression to encode the update; else update the values in // place. // 4) Construct a new object. - optionalt non_const_update_bound; + std::optional non_const_update_bound; // update value, may require extension to full bytes exprt update_value = src.value(); auto update_size_expr_opt = size_of_expr(update_value.type(), ns); diff --git a/src/util/numbering.h b/src/util/numbering.h index b12ae04e6f3a..d8a9f3325b21 100644 --- a/src/util/numbering.h +++ b/src/util/numbering.h @@ -9,12 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_UTIL_NUMBERING_H #define CPROVER_UTIL_NUMBERING_H +#include "invariant.h" + +#include #include #include -#include "invariant.h" -#include "optional.h" - /// \tparam keyt: The type of keys which will be numbered. /// \tparam hasht: The type of hashing functor used to hash keys. template > @@ -47,7 +47,7 @@ class numberingt final return (result.first)->second; } - optionalt get_number(const key_type &a) const + std::optional get_number(const key_type &a) const { const auto it = numbers_.find(a); if(it == numbers_.end()) diff --git a/src/util/optional.h b/src/util/optional.h deleted file mode 100644 index 5cf349d29711..000000000000 --- a/src/util/optional.h +++ /dev/null @@ -1,27 +0,0 @@ -/*******************************************************************\ - -Module: typedef for optional class template. New code should directly - use std::optional. - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#ifndef CPROVER_UTIL_OPTIONAL_H -#define CPROVER_UTIL_OPTIONAL_H - -#include "deprecate.h" - -#include - -template -using optionalt -#ifndef _WIN32 - // Visual Studio doesn't support [deprecated] in this place - DEPRECATED(SINCE(2023, 11, 17, "directly use std::optional instead")) = -#else - = -#endif - std::optional; // NOLINT template typedef - -#endif // CPROVER_UTIL_OPTIONAL_H diff --git a/src/util/optional_utils.h b/src/util/optional_utils.h index 6ddbd1cba51d..8a21946af5aa 100644 --- a/src/util/optional_utils.h +++ b/src/util/optional_utils.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: functions that are useful with optionalt +Module: functions that are useful with std::optional Author: Diffblue Ltd. @@ -9,13 +9,11 @@ Author: Diffblue Ltd. #ifndef CPROVER_UTIL_OPTIONAL_UTILS_H #define CPROVER_UTIL_OPTIONAL_UTILS_H -#include "optional.h" - /// Lookup a key in a map, if found return the associated value, /// nullopt otherwise template auto optional_lookup(const map_like_collectiont &map, const keyt &key) - -> optionaltsecond)> + -> std::optionalsecond)> { auto const it = map.find(key); if(it != map.end()) diff --git a/src/util/piped_process.cpp b/src/util/piped_process.cpp index 30737050007a..bd5e8c7031b1 100644 --- a/src/util/piped_process.cpp +++ b/src/util/piped_process.cpp @@ -90,7 +90,6 @@ #include "exception_utils.h" #include "invariant.h" #include "narrow.h" -#include "optional.h" #include "piped_process.h" #include // library for strerror function (on linux) @@ -448,7 +447,7 @@ piped_processt::statet piped_processt::get_status() return process_state; } -bool piped_processt::can_receive(optionalt wait_time) +bool piped_processt::can_receive(std::optional wait_time) { // unwrap the optional argument here const int timeout = wait_time ? narrow(*wait_time) : -1; diff --git a/src/util/piped_process.h b/src/util/piped_process.h index c95e4b14b218..c270999adb51 100644 --- a/src/util/piped_process.h +++ b/src/util/piped_process.h @@ -14,12 +14,11 @@ typedef void *HANDLE; // NOLINT #endif #include "message.h" -#include "optional.h" #include #define PIPED_PROCESS_INFINITE_TIMEOUT \ - optionalt \ + std::optional \ { \ } @@ -63,7 +62,7 @@ class piped_processt /// * 0 signifying non-blocking immediate return, and /// * an empty optional representing infinite wait time. /// \return true is there is data to read from process, false otherwise - bool can_receive(optionalt wait_time); + bool can_receive(std::optional wait_time); /// See if this process can receive data from the other process. /// Note this calls can_receive(0); diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 0c838161b3cd..b0c4de893b46 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ssa_expr.h" #include "std_expr.h" -optionalt member_offset( +std::optional member_offset( const struct_typet &type, const irep_idt &member, const namespacet &ns) @@ -63,7 +63,7 @@ optionalt member_offset( return result; } -optionalt member_offset_bits( +std::optional member_offset_bits( const struct_typet &type, const irep_idt &member, const namespacet &ns) @@ -87,7 +87,7 @@ optionalt member_offset_bits( } /// Compute the size of a type in bytes, rounding up to full bytes -optionalt +std::optional pointer_offset_size(const typet &type, const namespacet &ns) { auto bits = pointer_offset_bits(type, ns); @@ -98,7 +98,7 @@ pointer_offset_size(const typet &type, const namespacet &ns) return {}; } -optionalt +std::optional pointer_offset_bits(const typet &type, const namespacet &ns) { if(type.id()==ID_array) @@ -218,7 +218,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns) return {}; } -optionalt +std::optional member_offset_expr(const member_exprt &member_expr, const namespacet &ns) { // need to distinguish structs and unions @@ -232,7 +232,7 @@ member_offset_expr(const member_exprt &member_expr, const namespacet &ns) return {}; } -optionalt member_offset_expr( +std::optional member_offset_expr( const struct_typet &type, const irep_idt &member, const namespacet &ns) @@ -278,7 +278,7 @@ optionalt member_offset_expr( return simplify_expr(std::move(result), ns); } -optionalt size_of_expr(const typet &type, const namespacet &ns) +std::optional size_of_expr(const typet &type, const namespacet &ns) { if(type.id()==ID_array) { @@ -504,7 +504,7 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) return {}; } -optionalt +std::optional compute_pointer_offset(const exprt &expr, const namespacet &ns) { if(expr.id()==ID_symbol) @@ -566,7 +566,7 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns) return {}; // don't know } -optionalt get_subexpression_at_offset( +std::optional get_subexpression_at_offset( const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, @@ -689,7 +689,7 @@ optionalt get_subexpression_at_offset( expr, from_integer(offset_bytes, c_index_type()), target_type_raw); } -optionalt get_subexpression_at_offset( +std::optional get_subexpression_at_offset( const exprt &expr, const exprt &offset, const typet &target_type, diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h index b4ce99dbf73d..97107b11b87a 100644 --- a/src/util/pointer_offset_size.h +++ b/src/util/pointer_offset_size.h @@ -14,7 +14,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "irep.h" #include "mp_arith.h" -#include "optional.h" + +#include class exprt; class namespacet; @@ -22,41 +23,42 @@ class struct_typet; class typet; class member_exprt; -optionalt member_offset( +std::optional member_offset( const struct_typet &type, const irep_idt &member, const namespacet &ns); -optionalt member_offset_bits( +std::optional member_offset_bits( const struct_typet &type, const irep_idt &member, const namespacet &ns); -optionalt +std::optional pointer_offset_size(const typet &type, const namespacet &ns); -optionalt +std::optional pointer_offset_bits(const typet &type, const namespacet &ns); -optionalt +std::optional compute_pointer_offset(const exprt &expr, const namespacet &ns); -optionalt member_offset_expr(const member_exprt &, const namespacet &ns); +std::optional +member_offset_expr(const member_exprt &, const namespacet &ns); -optionalt member_offset_expr( +std::optional member_offset_expr( const struct_typet &type, const irep_idt &member, const namespacet &ns); -optionalt size_of_expr(const typet &type, const namespacet &ns); +std::optional size_of_expr(const typet &type, const namespacet &ns); -optionalt get_subexpression_at_offset( +std::optional get_subexpression_at_offset( const exprt &expr, const mp_integer &offset, const typet &target_type, const namespacet &ns); -optionalt get_subexpression_at_offset( +std::optional get_subexpression_at_offset( const exprt &expr, const exprt &offset, const typet &target_type, diff --git a/src/util/sharing_map.h b/src/util/sharing_map.h index a45b693fad72..2727f019223e 100644 --- a/src/util/sharing_map.h +++ b/src/util/sharing_map.h @@ -16,9 +16,15 @@ Author: Daniel Poetzl # include #endif +#include "as_const.h" +#include "irep.h" +#include "sharing_node.h" +#include "threeval.h" + #include #include #include +#include #include #include #include @@ -27,12 +33,6 @@ Author: Daniel Poetzl #include #include -#include "as_const.h" -#include "irep.h" -#include "optional.h" -#include "sharing_node.h" -#include "threeval.h" - #ifdef SM_INTERNAL_CHECKS # define SM_ASSERT(b) INVARIANT(b, "Sharing map internal invariant") #else @@ -332,8 +332,8 @@ class sharing_mapt /// - Best case: O(1) /// /// \param k: The key of the element to search - /// \return optionalt containing a const reference to the value if found - optionalt> + /// \return std::optional containing a const reference to the value if found + std::optional> find(const key_type &k) const; /// Swap with other map @@ -1448,7 +1448,7 @@ ::update(const key_type &k, std::function mutator) "method to check if an update is needed beforehand"); } -SHARING_MAPT2(optionalt>)::find( +SHARING_MAPT2(std::optional>)::find( const key_type &k) const { const nodet *lp = get_leaf_node(k); @@ -1456,7 +1456,8 @@ SHARING_MAPT2(optionalt>)::find( if(lp == nullptr) return std::nullopt; - return optionalt>(lp->get_value()); + return std::optional>( + lp->get_value()); } // static constants diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h index 4caf809bb55a..601b43b83524 100644 --- a/src/util/sharing_node.h +++ b/src/util/sharing_node.h @@ -17,6 +17,7 @@ Author: Daniel Poetzl #endif #include +#include #include #ifndef SN_SMALL_MAP diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 01f969bc74d5..6112e4c45fe8 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1717,7 +1717,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) // try to simplify byte_extract(byte_update(...)) auto const bu = expr_try_dynamic_cast(expr.op()); - optionalt update_offset; + std::optional update_offset; if(bu) update_offset = numeric_cast(bu->offset()); if(bu && el_size.has_value() && update_offset.has_value()) @@ -2028,7 +2028,7 @@ simplify_exprt::simplify_byte_extract_preorder(const byte_extract_exprt &expr) } else { - optionalt new_operands; + std::optional new_operands; for(std::size_t i = 0; i < expr.operands().size(); ++i) { @@ -2665,7 +2665,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) { if(skip_typecast(sum->op0()) == tc_op1 && sum->operands().size() == 2) { - optionalt offset; + std::optional offset; if(sum->type().id() == ID_pointer) { offset = std::move(simplify_pointer_offset( @@ -2711,7 +2711,7 @@ simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) return unchanged(expr); // preserve the sizeof type annotation - optionalt c_sizeof_type; + std::optional c_sizeof_type; for(const auto &op : expr.operands()) { const typet &sizeof_type = @@ -2808,7 +2808,7 @@ simplify_exprt::simplify_node_preorder(const exprt &expr) } else if(expr.has_operands()) { - optionalt new_operands; + std::optional new_operands; for(std::size_t i = 0; i < expr.operands().size(); ++i) { diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp index 2d71032069f9..f33ace7c29cd 100644 --- a/src/util/simplify_expr_array.cpp +++ b/src/util/simplify_expr_array.cpp @@ -169,7 +169,7 @@ simplify_exprt::simplify_index(const index_exprt &expr) if(array.type().id() == ID_array || array.type().id() == ID_vector) { - optionalt subtype; + std::optional subtype; if(array.type().id() == ID_array) subtype = to_array_type(array.type()).element_type(); else @@ -215,7 +215,7 @@ simplify_exprt::simplify_index_preorder(const index_exprt &expr) } else { - optionalt new_operands; + std::optional new_operands; for(std::size_t i = 0; i < expr.operands().size(); ++i) { diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 585b2254f8dd..569c91ef837c 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -235,7 +235,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr) if(may_be_reducible_to_interval) { - optionalt symbol_opt; + std::optional symbol_opt; std::set values; for(const exprt &op : new_operands) { diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 3d132ca47fa3..826cf4ae34db 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -177,7 +177,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_mult(const mult_exprt &expr) // true if we have found a constant bool constant_found = false; - optionalt c_sizeof_type; + std::optional c_sizeof_type; // scan all the operands for(exprt::operandst::iterator it = new_operands.begin(); diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 2e66c929a85a..a270d01296f4 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -221,7 +221,7 @@ simplify_exprt::simplify_member(const member_exprt &expr) // type and offset with respect to x. if(op_type.id() == ID_struct) { - optionalt requested_offset = + std::optional requested_offset = member_offset(to_struct_type(op_type), component_name, ns); if(requested_offset.has_value()) { diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index 2e949b8583f1..3b61acd4d084 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -193,7 +193,7 @@ bool join_operands(exprt &expr) return sort_and_join(expr, false); } -optionalt bits2expr( +std::optional bits2expr( const std::string &bits, const typet &type, bool little_endian, @@ -410,7 +410,7 @@ optionalt bits2expr( return {}; } -optionalt +std::optional expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) { // extract bits from lowest to highest memory address @@ -485,7 +485,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) return {}; } -optionalt> +std::optional> try_get_string_data_array(const exprt &content, const namespacet &ns) { if(content.id() != ID_address_of) @@ -522,5 +522,5 @@ try_get_string_data_array(const exprt &content, const namespacet &ns) const auto &char_seq = to_array_expr(symbol_ptr->value); - return optionalt>(char_seq); + return std::optional>(char_seq); } diff --git a/src/util/simplify_utils.h b/src/util/simplify_utils.h index c65011a2129c..d3e40799f874 100644 --- a/src/util/simplify_utils.h +++ b/src/util/simplify_utils.h @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_UTIL_SIMPLIFY_UTILS_H #include "expr.h" -#include "optional.h" #include @@ -25,13 +24,13 @@ bool join_operands(exprt &expr); bool sort_and_join(exprt &expr); // bit-level conversions -optionalt bits2expr( +std::optional bits2expr( const std::string &bits, const typet &type, bool little_endian, const namespacet &ns); -optionalt +std::optional expr2bits(const exprt &, bool little_endian, const namespacet &ns); /// Get char sequence from content field of a refined string expression @@ -46,7 +45,7 @@ expr2bits(const exprt &, bool little_endian, const namespacet &ns); /// \return array expression representing the char sequence which forms the /// content of the refined string expression, empty optional if the content /// cannot be determined -optionalt> +std::optional> try_get_string_data_array(const exprt &content, const namespacet &ns); #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 58897b858da5..7f93bf4b2533 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -82,7 +82,7 @@ void source_locationt::merge(const source_locationt &from) /// Get a path to the file, including working directory. /// \return Full path unless the file name is empty or refers /// to a built-in, in which case {} is returned. -optionalt source_locationt::full_path() const +std::optional source_locationt::full_path() const { const auto file = id2string(get_file()); diff --git a/src/util/source_location.h b/src/util/source_location.h index 340644fef294..fe99c578fb3a 100644 --- a/src/util/source_location.h +++ b/src/util/source_location.h @@ -12,8 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "deprecate.h" #include "irep.h" -#include "optional.h" +#include #include class source_locationt:public irept @@ -189,7 +189,7 @@ class source_locationt:public irept return static_cast(get_nil_irep()); } - optionalt full_path() const; + std::optional full_path() const; void add_pragma(const irep_idt &pragma) { diff --git a/src/util/std_code.h b/src/util/std_code.h index fb55e510b097..6cd7f9eddd3f 100644 --- a/src/util/std_code.h +++ b/src/util/std_code.h @@ -370,7 +370,7 @@ class code_frontend_declt : public codet /// or empty in the case where no initialisation is included. /// \note: Initial values may be present in the front end but they must be /// separated into a separate assignment when used in a `goto_instructiont`. - optionalt initial_value() const + std::optional initial_value() const { if(operands().size() < 2) return {}; @@ -381,7 +381,7 @@ class code_frontend_declt : public codet /// variable. Empty optional maybe passed to remove existing initialisation. /// \note: Initial values may be present in the front end but they must be /// separated into a separate assignment when used in a `goto_instructiont`. - void set_initial_value(optionalt initial_value) + void set_initial_value(std::optional initial_value) { if(!initial_value) { diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp index 117c7672ffa7..2fc68862ee18 100644 --- a/src/util/std_types.cpp +++ b/src/util/std_types.cpp @@ -100,7 +100,8 @@ void struct_typet::add_base(const struct_tag_typet &base) bases().push_back(baset(base)); } -optionalt struct_typet::get_base(const irep_idt &id) const +std::optional +struct_typet::get_base(const irep_idt &id) const { for(const auto &b : bases()) { diff --git a/src/util/std_types.h b/src/util/std_types.h index acc03e9e703b..37849dce9c13 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -277,7 +277,7 @@ class struct_typet:public struct_union_typet /// Return the base with the given name, if exists. /// \param id: The name of the base we are looking for. /// \return The base if exists. - optionalt get_base(const irep_idt &id) const; + std::optional get_base(const irep_idt &id) const; /// Test whether `id` is a base class/struct. /// \param id: symbol type name diff --git a/src/util/string2int.cpp b/src/util/string2int.cpp index 6cf4bf75b122..02a90120a520 100644 --- a/src/util/string2int.cpp +++ b/src/util/string2int.cpp @@ -56,17 +56,19 @@ unsigned long long int unsafe_string2unsignedlonglong( return *string2optional(str, base); } -optionalt string2optional_int(const std::string &str, int base) +std::optional string2optional_int(const std::string &str, int base) { return string2optional(str, base); } -optionalt string2optional_unsigned(const std::string &str, int base) +std::optional +string2optional_unsigned(const std::string &str, int base) { return string2optional(str, base); } -optionalt string2optional_size_t(const std::string &str, int base) +std::optional +string2optional_size_t(const std::string &str, int base) { return string2optional(str, base); } diff --git a/src/util/string2int.h b/src/util/string2int.h index 0d9d71defe84..cafb137e85b5 100644 --- a/src/util/string2int.h +++ b/src/util/string2int.h @@ -11,7 +11,8 @@ Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk #define CPROVER_UTIL_STRING2INT_H #include "narrow.h" -#include "optional.h" + +#include #include #include @@ -38,18 +39,18 @@ long long unsigned int unsafe_string2unsignedlonglong( /// Convert string to integer as per stoi, but return nullopt when /// stoi would throw -optionalt string2optional_int(const std::string &, int base = 10); +std::optional string2optional_int(const std::string &, int base = 10); /// Convert string to unsigned similar to the stoul or stoull functions, /// return nullopt when the conversion fails. /// Note: Unlike stoul or stoull negative inputs are disallowed -optionalt +std::optional string2optional_unsigned(const std::string &, int base = 10); /// Convert string to size_t similar to the stoul or stoull functions, /// return nullopt when the conversion fails. /// Note: Unlike stoul or stoull negative inputs are disallowed -optionalt +std::optional string2optional_size_t(const std::string &, int base = 10); /// convert string to signed long long if T is signed @@ -86,7 +87,7 @@ auto string2optional_base(const std::string &str, int base) -> /// with out_of_range or invalid_argument template auto wrap_string_conversion(do_conversiont do_conversion) - -> optionalt + -> std::optional { try { @@ -107,7 +108,7 @@ auto wrap_string_conversion(do_conversiont do_conversion) /// (unsigned) long long /// does not accept negative inputs when the result type is unsigned template -optionalt string2optional(const std::string &str, int base = 10) +std::optional string2optional(const std::string &str, int base = 10) { return wrap_string_conversion([&]() { return narrow_or_throw_out_of_range(string2optional_base(str, base)); diff --git a/src/util/substitute_symbols.cpp b/src/util/substitute_symbols.cpp index f28ac87c8e13..95a2fc7ed76e 100644 --- a/src/util/substitute_symbols.cpp +++ b/src/util/substitute_symbols.cpp @@ -13,7 +13,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "std_expr.h" -static optionalt substitute_symbols_rec( +static std::optional substitute_symbols_rec( const std::map &substitutions, exprt src) { @@ -107,7 +107,7 @@ static optionalt substitute_symbols_rec( return {}; } -optionalt +std::optional substitute_symbols(const std::map &substitutions, exprt src) { return substitute_symbols_rec(substitutions, src); diff --git a/src/util/substitute_symbols.h b/src/util/substitute_symbols.h index 0c4ded4b494a..dd4e867c2d24 100644 --- a/src/util/substitute_symbols.h +++ b/src/util/substitute_symbols.h @@ -13,9 +13,9 @@ Author: Daniel Kroening, dkr@amazon.com /// Symbol Substitution #include "irep.h" -#include "optional.h" #include +#include class exprt; @@ -25,7 +25,7 @@ class exprt; /// substituted. /// \returns expression after substitution, /// or {} when no substitution took place -optionalt +std::optional substitute_symbols(const std::map &substitutions, exprt); #endif // CPROVER_UTIL_SUBSTITUTE_SYMBOLS_H diff --git a/src/util/union_find.h b/src/util/union_find.h index 95a83db9b1b9..f38a7e990223 100644 --- a/src/util/union_find.h +++ b/src/util/union_find.h @@ -172,8 +172,8 @@ class union_find final // are 'a' and 'b' in the same set? bool same_set(const T &a, const T &b) const { - const optionalt na = numbers.get_number(a); - const optionalt nb = numbers.get_number(b); + const std::optional na = numbers.get_number(a); + const std::optional nb = numbers.get_number(b); if(na && nb) return uuf.same_set(*na, *nb); @@ -260,7 +260,7 @@ class union_find final uuf.isolate(number(a)); } - optionalt get_number(const T &a) const + std::optional get_number(const T &a) const { return numbers.get_number(a); } diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp index 15d50d012e23..5b9ea1dcd460 100644 --- a/unit/analyses/ai/ai.cpp +++ b/unit/analyses/ai/ai.cpp @@ -23,7 +23,6 @@ Author: Diffblue Ltd. #include #include #include -#include /// A very simple analysis that counts executed instructions along a particular /// path, taking the max at merge points and saturating at 100 instructions. @@ -33,8 +32,7 @@ Author: Diffblue Ltd. class instruction_counter_domaint : public ai_domain_baset { public: - - optionalt path_length; + std::optional path_length; void transform( const irep_idt &, diff --git a/unit/ansi-c/c_typecheck_base.cpp b/unit/ansi-c/c_typecheck_base.cpp index 1723bc300195..a737f27bbe65 100644 --- a/unit/ansi-c/c_typecheck_base.cpp +++ b/unit/ansi-c/c_typecheck_base.cpp @@ -28,7 +28,7 @@ class c_typecheck_testt : public c_typecheck_baset { } - optionalt test_typecheck_shadow_memory_builtin( + std::optional test_typecheck_shadow_memory_builtin( const side_effect_expr_function_callt &expr) { return typecheck_shadow_memory_builtin(expr); diff --git a/unit/goto-cc/armcc_cmdline.cpp b/unit/goto-cc/armcc_cmdline.cpp index e9d9ec4f1540..99dd3a3026b8 100644 --- a/unit/goto-cc/armcc_cmdline.cpp +++ b/unit/goto-cc/armcc_cmdline.cpp @@ -4,12 +4,10 @@ #include -#include - #include #include -optionalt +std::optional prefix_in_list(const std::string &option, const std::vector &list); static const std::vector test_list{"spam", "eggs", "and", "ham"}; diff --git a/unit/solvers/smt2_incremental/ast/smt_index.cpp b/unit/solvers/smt2_incremental/ast/smt_index.cpp index bba659b8d70a..e2e2d42e7209 100644 --- a/unit/solvers/smt2_incremental/ast/smt_index.cpp +++ b/unit/solvers/smt2_incremental/ast/smt_index.cpp @@ -1,7 +1,5 @@ // Author: Diffblue Ltd. -#include - #include #include @@ -35,8 +33,8 @@ TEST_CASE("Visiting smt_indext", "[core][smt2_incremental]") class : public smt_index_const_downcast_visitort { public: - optionalt numeral_visited{}; - optionalt symbol_visited{}; + std::optional numeral_visited{}; + std::optional symbol_visited{}; void visit(const smt_numeral_indext &numeral) override { diff --git a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index 11a2ec1c2a40..76cedc3115e7 100644 --- a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -65,8 +65,8 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]") make_c_enum_tag_instance_symbol(enum_type_symbol); symbol_table.insert(enum_type_symbol); symbol_table.insert(enum_tag_value_symbol); - optionalt input_term; - optionalt expected_result; + std::optional input_term; + std::optional expected_result; using rowt = std::pair; @@ -143,8 +143,8 @@ TEST_CASE( make_c_enum_tag_instance_symbol(enum_type_symbol); symbol_table.insert(enum_type_symbol); symbol_table.insert(enum_tag_value_symbol); - optionalt input_term; - optionalt input_type; + std::optional input_term; + std::optional input_type; std::string invariant_reason; using rowt = std::tuple; diff --git a/unit/testing-utils/expr_query.h b/unit/testing-utils/expr_query.h index 84a2d20910b2..83c13d683f48 100644 --- a/unit/testing-utils/expr_query.h +++ b/unit/testing-utils/expr_query.h @@ -17,8 +17,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include -/// Wrapper for optionalt with useful method for queries to be used in -/// unit tests. +/// Wrapper for std::optional with useful method for queries to be used +/// in unit tests. template class expr_queryt { diff --git a/unit/testing-utils/smt2irep.h b/unit/testing-utils/smt2irep.h index 8e4eac54ac53..f465020c04fc 100644 --- a/unit/testing-utils/smt2irep.h +++ b/unit/testing-utils/smt2irep.h @@ -6,13 +6,12 @@ #include #include -#include #include struct smt2_parser_test_resultt { - optionalt parsed_output; + std::optional parsed_output; std::string messages; }; diff --git a/unit/util/expr_cast/expr_cast.cpp b/unit/util/expr_cast/expr_cast.cpp index 3272a8374809..30204c4059ff 100644 --- a/unit/util/expr_cast/expr_cast.cpp +++ b/unit/util/expr_cast/expr_cast.cpp @@ -127,7 +127,7 @@ SCENARIO("expr_dynamic_cast", "Trying casting from an exprt rvalue reference to a symbol_exprt should " "yield a non empty optional.") { - optionalt result = + std::optional result = expr_try_dynamic_cast(std::move(expr)); REQUIRE(result.has_value()); } @@ -136,7 +136,8 @@ SCENARIO("expr_dynamic_cast", "Trying casting from an exprt rvalue reference to a transt should yield " "a empty optional.") { - optionalt result = expr_try_dynamic_cast(std::move(expr)); + std::optional result = + expr_try_dynamic_cast(std::move(expr)); REQUIRE_FALSE(result.has_value()); } } @@ -242,7 +243,7 @@ SCENARIO("type_dynamic_cast", "[core][utils][expr_cast][type_dynamic_cast]") "Trying casting from a typet rvalue reference to a symbol_exprt should " "yield a non empty optional.") { - optionalt result = + std::optional result = type_try_dynamic_cast(std::move(type)); REQUIRE(result.has_value()); } @@ -251,7 +252,7 @@ SCENARIO("type_dynamic_cast", "[core][utils][expr_cast][type_dynamic_cast]") "Trying casting from a typet rvalue reference to a struct_typet should " "yield a empty optional.") { - optionalt result = + std::optional result = type_try_dynamic_cast(std::move(type)); REQUIRE_FALSE(result.has_value()); } diff --git a/unit/util/json_object.cpp b/unit/util/json_object.cpp index 23096e1a0abf..74d70147fb34 100644 --- a/unit/util/json_object.cpp +++ b/unit/util/json_object.cpp @@ -9,7 +9,6 @@ Author: Diffblue Ltd. #include #include -#include #include #include @@ -38,13 +37,13 @@ SCENARIO( return make_pair(number, json_stringt{number}); }); - const optionalt one = optional_lookup(object, "one"); + const std::optional one = optional_lookup(object, "one"); REQUIRE(one); REQUIRE(one->value == "one"); - const optionalt two = optional_lookup(object, "two"); + const std::optional two = optional_lookup(object, "two"); REQUIRE(two); REQUIRE(two->value == "two"); - const optionalt three = optional_lookup(object, "three"); + const std::optional three = optional_lookup(object, "three"); REQUIRE(three); REQUIRE(three->value == "three"); }