From 400821daffa7ee61d7e94010faf5ddfdc9b4669a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 24 Mar 2022 01:19:30 +0000 Subject: [PATCH] Do not use optionalt::value() std::optional::value() is unavailable in earlier versions of macOS. We generally use operator* already, which always works. --- .../java_bytecode_convert_class.cpp | 57 ++++++++----------- .../java_bytecode_convert_method.cpp | 8 +-- .../java_bytecode/java_bytecode_language.cpp | 8 +-- jbmc/src/java_bytecode/java_entry_point.cpp | 4 +- jbmc/src/java_bytecode/java_types.h | 2 +- .../require_goto_statements.cpp | 2 +- jbmc/unit/java-testing-utils/require_type.cpp | 4 +- .../java_types/generic_type_index.cpp | 8 +-- .../abstract_environment.cpp | 4 +- .../full_array_abstract_object.cpp | 8 +-- .../full_struct_abstract_object.cpp | 13 ++--- .../interval_abstract_value.cpp | 2 +- .../variable-sensitivity/liveness_context.cpp | 2 +- src/ansi-c/ansi_c_entry_point.cpp | 8 +-- src/ansi-c/c_typecheck_expr.cpp | 12 ++-- src/ansi-c/c_typecheck_type.cpp | 4 +- src/ansi-c/expr2c.cpp | 2 +- src/ansi-c/goto_check_c.cpp | 15 +++-- src/ansi-c/padding.cpp | 4 +- src/cpp/cpp_constructor.cpp | 2 +- src/cpp/cpp_destructor.cpp | 2 +- src/cpp/cpp_typecheck.cpp | 2 +- src/cpp/cpp_typecheck_code.cpp | 4 +- src/cpp/cpp_typecheck_compound_type.cpp | 2 +- src/cpp/cpp_typecheck_declaration.cpp | 2 +- src/cpp/cpp_typecheck_destructor.cpp | 4 +- src/cpp/cpp_typecheck_expr.cpp | 8 +-- src/cpp/cpp_typecheck_initializer.cpp | 2 +- src/crangler/c_wrangler.cpp | 2 +- src/goto-analyzer/show_on_source.cpp | 4 +- src/goto-analyzer/taint_analysis.cpp | 10 ++-- src/goto-cc/cl_message_handler.cpp | 4 +- src/goto-cc/gcc_message_handler.cpp | 4 +- src/goto-harness/goto_harness_generator.cpp | 2 +- .../goto_harness_parse_options.cpp | 2 +- src/goto-harness/recursive_initialization.cpp | 10 ++-- src/goto-instrument/aggressive_slicer.cpp | 2 +- src/goto-instrument/contracts/contracts.cpp | 6 +- .../contracts/instrument_spec_assigns.cpp | 31 +++++----- src/goto-instrument/count_eloc.cpp | 4 +- src/goto-instrument/dump_c.cpp | 2 +- .../goto_instrument_parse_options.cpp | 2 +- src/goto-instrument/model_argc_argv.cpp | 2 +- src/goto-programs/allocate_objects.cpp | 2 +- src/goto-programs/goto_convert.cpp | 4 +- src/goto-programs/goto_program.cpp | 6 +- src/goto-programs/interpreter_evaluate.cpp | 2 +- src/goto-programs/mm_io.cpp | 5 +- src/goto-symex/symex_clean_expr.cpp | 8 +-- src/goto-symex/symex_function_call.cpp | 4 +- src/goto-symex/symex_other.cpp | 4 +- src/goto-symex/symex_set_return_value.cpp | 2 +- src/jsil/jsil_entry_point.cpp | 8 +-- src/linking/remove_internal_symbols.cpp | 5 +- .../memory_analyzer_parse_options.cpp | 2 +- .../value_set_dereference.cpp | 11 ++-- src/solvers/flattening/boolbv_extractbits.cpp | 4 +- src/solvers/flattening/boolbv_index.cpp | 2 +- src/solvers/flattening/boolbv_quantifier.cpp | 4 +- src/solvers/flattening/bv_pointers.cpp | 4 +- src/solvers/flattening/pointer_logic.cpp | 2 +- src/solvers/lowering/byte_operators.cpp | 15 +++-- src/solvers/smt2/smt2_conv.cpp | 8 +-- src/solvers/smt2/smt2_dec.cpp | 2 +- .../smt_response_validation.cpp | 2 +- .../strings/string_builtin_function.cpp | 32 +++++------ .../string_constraint_instantiation.cpp | 2 +- .../string_format_builtin_function.cpp | 6 +- src/solvers/strings/string_refinement.cpp | 8 +-- .../statement_list_entry_point.cpp | 5 +- .../statement_list_parse_tree_io.cpp | 2 +- src/util/cmdline.cpp | 4 +- src/util/pointer_expr.cpp | 5 +- src/util/pointer_offset_size.cpp | 18 +++--- src/util/pointer_predicates.cpp | 2 +- src/util/simplify_expr.cpp | 16 +++--- src/util/simplify_expr_pointer.cpp | 2 +- src/util/simplify_expr_struct.cpp | 8 +-- src/util/simplify_utils.cpp | 2 +- src/util/std_expr.cpp | 13 ++--- .../length_of_decimal_int.cpp | 3 +- unit/util/edit_distance.cpp | 50 ++++++++-------- unit/util/interval/eval.cpp | 4 +- unit/util/interval/subtract.cpp | 8 +-- unit/util/interval_union.cpp | 4 +- unit/util/optional_utils.cpp | 4 +- unit/util/pointer_offset_size.cpp | 32 +++++------ 87 files changed, 294 insertions(+), 324 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index e58d844f3da..24ce35c6c08 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -190,16 +190,15 @@ extract_generic_superclass_reference(const optionalt &signature) { // skip the (potential) list of generic parameters at the beginning of the // signature - const size_t start = - signature.value().front() == '<' - ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1 - : 0; + const size_t start = signature->front() == '<' + ? find_closing_delimiter(*signature, 0, '<', '>') + 1 + : 0; // extract the superclass reference const size_t end = - find_closing_semi_colon_for_reference_type(signature.value(), start); + find_closing_semi_colon_for_reference_type(*signature, start); const std::string superclass_ref = - signature.value().substr(start, (end - start) + 1); + signature->substr(start, (end - start) + 1); // if the superclass is generic then the reference is of form // `Lsuperclass-name;` if it is implicitly generic, then the @@ -231,15 +230,13 @@ static optionalt extract_generic_interface_reference( { // skip the (potential) list of generic parameters at the beginning of the // signature - size_t start = - signature.value().front() == '<' - ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1 - : 0; + size_t start = signature->front() == '<' + ? find_closing_delimiter(*signature, 0, '<', '>') + 1 + : 0; // skip the superclass reference (if there is at least one interface // reference in the signature, then there is a superclass reference) - start = - find_closing_semi_colon_for_reference_type(signature.value(), start) + 1; + start = find_closing_semi_colon_for_reference_type(*signature, start) + 1; // if the interface name includes package name, convert dots to slashes std::string interface_name_slash_to_dot = interface_name; @@ -249,13 +246,12 @@ static optionalt extract_generic_interface_reference( '.', '/'); - start = - signature.value().find("L" + interface_name_slash_to_dot + "<", start); + start = signature->find("L" + interface_name_slash_to_dot + "<", start); if(start != std::string::npos) { const size_t &end = - find_closing_semi_colon_for_reference_type(signature.value(), start); - return signature.value().substr(start, (end - start) + 1); + find_closing_semi_colon_for_reference_type(*signature, start); + return signature->substr(start, (end - start) + 1); } } return {}; @@ -277,20 +273,17 @@ void java_bytecode_convert_classt::convert( } java_class_typet class_type; - if(c.signature.has_value() && c.signature.value()[0]=='<') + if(c.signature.has_value() && (*c.signature)[0] == '<') { java_generic_class_typet generic_class_type; #ifdef DEBUG - std::cout << "INFO: found generic class signature " - << c.signature.value() - << " in parsed class " - << c.name << "\n"; + std::cout << "INFO: found generic class signature " << *c.signature + << " in parsed class " << c.name << "\n"; #endif try { - const std::vector &generic_types=java_generic_type_from_string( - id2string(c.name), - c.signature.value()); + const std::vector &generic_types = + java_generic_type_from_string(id2string(c.name), *c.signature); for(const typet &t : generic_types) { generic_class_type.generic_types() @@ -301,9 +294,9 @@ void java_bytecode_convert_classt::convert( catch(const unsupported_java_class_signature_exceptiont &e) { log.debug() << "Class: " << c.name - << "\n could not parse signature: " << c.signature.value() - << "\n " << e.what() - << "\n ignoring that the class is generic" << messaget::eom; + << "\n could not parse signature: " << *c.signature << "\n " + << e.what() << "\n ignoring that the class is generic" + << messaget::eom; } } @@ -359,15 +352,15 @@ void java_bytecode_convert_classt::convert( try { const java_generic_struct_tag_typet generic_base( - base, superclass_ref.value(), qualified_classname); + base, *superclass_ref, qualified_classname); class_type.add_base(generic_base); } catch(const unsupported_java_class_signature_exceptiont &e) { log.debug() << "Superclass: " << c.super_class << " of class: " << c.name - << "\n could not parse signature: " - << superclass_ref.value() << "\n " << e.what() + << "\n could not parse signature: " << *superclass_ref + << "\n " << e.what() << "\n ignoring that the superclass is generic" << messaget::eom; class_type.add_base(base); @@ -401,13 +394,13 @@ void java_bytecode_convert_classt::convert( try { const java_generic_struct_tag_typet generic_base( - base, interface_ref.value(), qualified_classname); + base, *interface_ref, qualified_classname); class_type.add_base(generic_base); } catch(const unsupported_java_class_signature_exceptiont &e) { log.debug() << "Interface: " << interface << " of class: " << c.name - << "\n could not parse signature: " << interface_ref.value() + << "\n could not parse signature: " << *interface_ref << "\n " << e.what() << "\n ignoring that the interface is generic" << messaget::eom; diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 18f145556c5..221a17ca3af 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -255,7 +255,7 @@ java_method_typet member_type_lazy( try { auto member_type_from_signature = - java_type_from_string(signature.value(), class_name); + java_type_from_string(*signature, class_name); INVARIANT( member_type_from_signature.has_value() && member_type_from_signature->id() == ID_code, @@ -269,7 +269,7 @@ java_method_typet member_type_lazy( else { message.debug() << "Method: " << class_name << "." << method_name - << "\n signature: " << signature.value() + << "\n signature: " << *signature << "\n descriptor: " << descriptor << "\n different number of parameters, reverting to " "descriptor" @@ -279,8 +279,8 @@ java_method_typet member_type_lazy( catch(const unsupported_java_class_signature_exceptiont &e) { message.debug() << "Method: " << class_name << "." << method_name - << "\n could not parse signature: " << signature.value() - << "\n " << e.what() << "\n" + << "\n could not parse signature: " << *signature << "\n " + << e.what() << "\n" << " reverting to descriptor: " << descriptor << message.eom; } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 92ed7db4747..91ce547ab3f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -338,10 +338,10 @@ void java_bytecode_languaget::parse_from_main_class() throwMainClassLoadingError(id2string(main_class)); return; } - status() << "Trying to load Java main class: " << maybe_class_name.value() + status() << "Trying to load Java main class: " << *maybe_class_name << eom; if(!java_class_loader.can_load_class( - maybe_class_name.value(), get_message_handler())) + *maybe_class_name, get_message_handler())) { throwMainClassLoadingError(id2string(main_class)); return; @@ -349,7 +349,7 @@ void java_bytecode_languaget::parse_from_main_class() // Everything went well. We have a loadable main class. // The entry point ('main') will be checked later. config.main = id2string(main_class); - main_class = maybe_class_name.value(); + main_class = *maybe_class_name; } status() << "Found Java main class: " << main_class << eom; // Now really load it. @@ -403,7 +403,7 @@ bool java_bytecode_languaget::parse( // If we have an entry method, we can derive a main class. if(config.main.has_value()) { - const std::string &entry_method = config.main.value(); + const std::string &entry_method = *config.main; const auto last_dot_position = entry_method.find_last_of('.'); main_class = entry_method.substr(0, last_dot_position); } diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 58c5d1160bd..9e5c04c7a15 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -557,8 +557,8 @@ main_function_resultt get_main_symbol( if(config.main.has_value()) { std::string error_message; - irep_idt main_symbol_id = resolve_friendly_method_name( - config.main.value(), symbol_table, error_message); + irep_idt main_symbol_id = + resolve_friendly_method_name(*config.main, symbol_table, error_message); if(main_symbol_id.empty()) { diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 2db1df9f1af..49661b1432a 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -1145,7 +1145,7 @@ inline optionalt java_type_from_string_with_exception( { try { - return java_type_from_string(signature.value(), class_name); + return java_type_from_string(*signature, class_name); } catch(unsupported_java_class_signature_exceptiont &) { diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 8822e4b6c25..460a2c2644f 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -102,7 +102,7 @@ require_goto_statements::find_struct_component_assignments( const member_exprt &superclass_expr = to_member_expr(member_expr.compound()); const irep_idt supercomponent_name = - "@" + id2string(superclass_name.value()); + "@" + id2string(*superclass_name); object_descriptor_exprt ode; const namespacet ns(symbol_table); diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 89aaa8036d7..ad7ca156133 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -23,7 +23,7 @@ pointer_typet require_type::require_pointer( const pointer_typet &pointer = to_pointer_type(type); if(subtype) - REQUIRE(pointer.subtype() == subtype.value()); + REQUIRE(pointer.subtype() == *subtype); return pointer; } @@ -248,7 +248,7 @@ const typet &require_type::require_java_non_generic_type( REQUIRE(!is_java_generic_parameter(type)); REQUIRE(!is_java_generic_type(type)); if(expect_subtype) - REQUIRE(type.subtype() == expect_subtype.value()); + REQUIRE(type.subtype() == *expect_subtype); return type; } diff --git a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp index 4c5e42a06fb..885f31954bf 100644 --- a/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp +++ b/jbmc/unit/java_bytecode/java_types/generic_type_index.cpp @@ -34,9 +34,9 @@ SCENARIO("generic_type_index", "[core][java_types]") THEN("X has index 0, Y index 1 and Z is not found") { REQUIRE(indexX.has_value()); - REQUIRE(indexX.value() == 0); + REQUIRE(*indexX == 0); REQUIRE(index_value.has_value()); - REQUIRE(index_value.value() == 1); + REQUIRE(*index_value == 1); REQUIRE_FALSE(indexZ.has_value()); } } @@ -66,9 +66,9 @@ SCENARIO("generic_type_index", "[core][java_types]") THEN("K has index 0, V index 1 and T is not found") { REQUIRE(index_param0.has_value()); - REQUIRE(index_param0.value() == 0); + REQUIRE(*index_param0 == 0); REQUIRE(index_param1.has_value()); - REQUIRE(index_param1.value() == 1); + REQUIRE(*index_param1 == 1); REQUIRE_FALSE(index_param2.has_value()); } } diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index 4a89216ea2f..156cac833ee 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -140,7 +140,7 @@ abstract_object_pointert abstract_environmentt::resolve_symbol( const auto symbol_entry = map.find(symbol.get_identifier()); if(symbol_entry.has_value()) - return symbol_entry.value(); + return *symbol_entry; return abstract_object_factory(expr.type(), ns, true, false); } @@ -490,7 +490,7 @@ abstract_environmentt::modified_symbols( const auto &second_entry = second.map.find(entry.first); if(second_entry.has_value()) { - if(second_entry.value().get()->has_been_modified(entry.second)) + if(second_entry->get()->has_been_modified(entry.second)) { CHECK_RETURN(!entry.first.empty()); symbols_diff.push_back(entry.first); diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 8fcdcc3f6db..631bfb68d71 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -334,8 +334,7 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( { result->map.replace( index.value, - abstract_objectt::merge(old_value.value(), value, widen_modet::no) - .object); + abstract_objectt::merge(*old_value, value, widen_modet::no).object); } DATA_INVARIANT(result->verify(), "Structural invariants maintained"); @@ -371,8 +370,7 @@ void full_array_abstract_objectt::map_put( // if we're over the max_index, merge with existing value auto replacement_value = overrun - ? abstract_objectt::merge(old_value.value(), value, widen_modet::no) - .object + ? abstract_objectt::merge(*old_value, value, widen_modet::no).object : value; map.replace(index_value, replacement_value); @@ -386,7 +384,7 @@ abstract_object_pointert full_array_abstract_objectt::map_find_or_top( { auto value = map.find(index_value); if(value.has_value()) - return value.value(); + return *value; return get_top_entry(env, ns); } diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index a512725c6cf..6a00b9cbc10 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -97,7 +97,7 @@ abstract_object_pointert full_struct_abstract_objectt::read_component( if(value.has_value()) { - return value.value(); + return *value; } else { @@ -144,8 +144,7 @@ abstract_object_pointert full_struct_abstract_objectt::write_component( else { result->map.replace( - c, - environment.write(old_value.value(), value, stack, ns, merging_write)); + c, environment.write(*old_value, value, stack, ns, merging_write)); } result->set_not_top(); @@ -178,9 +177,7 @@ abstract_object_pointert full_struct_abstract_objectt::write_component( } result->map.replace( - c, - abstract_objectt::merge(old_value.value(), value, widen_modet::no) - .object); + c, abstract_objectt::merge(*old_value, value, widen_modet::no).object); } else { @@ -225,8 +222,8 @@ void full_struct_abstract_objectt::output( out << ", "; } out << '.' << field.get_name() << '='; - static_cast(value.value()) - ->output(out, ai, ns); + static_cast(*value)->output( + out, ai, ns); first = false; } } diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 7ad4eb52908..3b7d9ea2cf1 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -120,7 +120,7 @@ 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); INVARIANT(maybe_integer_value.has_value(), "Input has to have a value"); - return maybe_integer_value.value(); + return *maybe_integer_value; } static inline constant_interval_exprt diff --git a/src/analyses/variable-sensitivity/liveness_context.cpp b/src/analyses/variable-sensitivity/liveness_context.cpp index 1ff3e9b5dc2..582aad6ece0 100644 --- a/src/analyses/variable-sensitivity/liveness_context.cpp +++ b/src/analyses/variable-sensitivity/liveness_context.cpp @@ -15,7 +15,7 @@ bool liveness_contextt::has_location() const abstract_objectt::locationt liveness_contextt::get_location() const { - return assign_location.value(); + return *assign_location; } /** diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 6c10396e08e..54322fca484 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -121,7 +121,7 @@ bool ansi_c_entry_point( std::list matches; for(const auto &symbol_name_entry : - equal_range(symbol_table.symbol_base_map, config.main.value())) + equal_range(symbol_table.symbol_base_map, *config.main)) { // look it up symbol_tablet::symbolst::const_iterator s_it = @@ -137,7 +137,7 @@ bool ansi_c_entry_point( if(matches.empty()) { messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() << "' not found" + message.error() << "main symbol '" << *config.main << "' not found" << messaget::eom; return true; // give up } @@ -145,8 +145,8 @@ bool ansi_c_entry_point( if(matches.size()>=2) { messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() - << "' is ambiguous" << messaget::eom; + message.error() << "main symbol '" << *config.main << "' is ambiguous" + << messaget::eom; return true; } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 63bfaa3fff0..f39bbca31d5 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -632,8 +632,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) } result = plus_exprt( - result, - typecast_exprt::conditional_cast(o_opt.value(), size_type())); + result, typecast_exprt::conditional_cast(*o_opt, size_type())); } type=struct_union_type.get_component(component_name).type(); @@ -666,8 +665,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) result = plus_exprt( result, - typecast_exprt::conditional_cast( - o_opt.value(), size_type())); + typecast_exprt::conditional_cast(*o_opt, size_type())); } typet tmp = follow(c.type()); @@ -716,7 +714,7 @@ void c_typecheck_baset::typecheck_expr_builtin_offsetof(exprt &expr) index = typecast_exprt::conditional_cast(index, size_type()); - result = plus_exprt(result, mult_exprt(element_size_opt.value(), index)); + result = plus_exprt(result, mult_exprt(*element_size_opt, index)); typet tmp=type.subtype(); type=tmp; @@ -1012,7 +1010,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) throw 0; } - new_expr = size_of_opt.value(); + new_expr = *size_of_opt; } new_expr.swap(expr); @@ -2710,7 +2708,7 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - size_expr = std::move(size_expr_opt.value()); + size_expr = std::move(*size_expr_opt); } irep_idt id = identifier == CPROVER_PREFIX "r_ok" diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 26bf7d194f0..61fb2c79355 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -710,9 +710,9 @@ void c_typecheck_baset::typecheck_vector_type(typet &type) throw 0; } - simplify(sub_size_expr_opt.value(), *this); + simplify(*sub_size_expr_opt, *this); - const auto sub_size = numeric_cast(sub_size_expr_opt.value()); + const auto sub_size = numeric_cast(*sub_size_expr_opt); if(!sub_size.has_value()) { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index b776bfe6b16..cd9101fd396 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -1905,7 +1905,7 @@ std::string expr2ct::convert_constant( if(sizeof_expr_opt.has_value()) { ++sizeof_nesting; - dest = convert(sizeof_expr_opt.value()) + " /*" + dest + "*/ "; + dest = convert(*sizeof_expr_opt) + " /*" + dest + "*/ "; --sizeof_nesting; } } diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 26a11444880..06ec08d582e 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1342,7 +1342,7 @@ void goto_check_ct::pointer_overflow_check( { auto size_of_expr_opt = size_of_expr(object_type, ns); CHECK_RETURN(size_of_expr_opt.has_value()); - exprt object_size = size_of_expr_opt.value(); + exprt object_size = *size_of_expr_opt; const binary_exprt &binary_expr = to_binary_expr(expr); exprt offset_operand = binary_expr.lhs().type().id() == ID_pointer @@ -1401,7 +1401,7 @@ void goto_check_ct::pointer_validity_check( { auto size_of_expr_opt = size_of_expr(expr.type(), ns); CHECK_RETURN(size_of_expr_opt.has_value()); - size = size_of_expr_opt.value(); + size = *size_of_expr_opt; } auto conditions = get_pointer_dereferenceable_conditions(pointer, size); @@ -1448,7 +1448,7 @@ void goto_check_ct::pointer_primitive_check( const exprt size = !size_of_expr_opt.has_value() ? from_integer(1, size_type()) - : size_of_expr_opt.value(); + : *size_of_expr_opt; const conditionst &conditions = get_pointer_points_to_valid_memory_conditions(pointer, size); @@ -1642,10 +1642,9 @@ void goto_check_ct::bounds_check_index( CHECK_RETURN(type_size_opt.has_value()); binary_relation_exprt inequality( - typecast_exprt::conditional_cast( - ode.offset(), type_size_opt.value().type()), + typecast_exprt::conditional_cast(ode.offset(), type_size_opt->type()), ID_lt, - type_size_opt.value()); + *type_size_opt); add_guarded_property( inequality, @@ -1832,7 +1831,7 @@ bool goto_check_ct::check_rec_member( plus_exprt{ char_pointer, typecast_exprt::conditional_cast( - member_offset_opt.value(), pointer_diff_type())}, + *member_offset_opt, pointer_diff_type())}, new_pointer_type); dereference_exprt new_deref{new_address_casted}; @@ -2053,7 +2052,7 @@ void goto_check_ct::goto_check( auto matched = match_named_check(d.first); if(matched.has_value()) { - auto named_check = matched.value(); + auto named_check = *matched; auto name = named_check.first; auto status = named_check.second; bool *flag = name_to_flag.find(name)->second; diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp index 9829ebdc767..bbfcb9be05e 100644 --- a/src/ansi-c/padding.cpp +++ b/src/ansi-c/padding.cpp @@ -493,8 +493,8 @@ void add_padding(union_typet &type, const namespacet &ns) if(c.type().id() == ID_c_bit_field) { auto w = underlying_width(to_c_bit_field_type(c.type()), ns); - if(w.has_value() && w.value() > max_alignment_bits) - max_alignment_bits = w.value(); + if(w.has_value() && *w > max_alignment_bits) + max_alignment_bits = *w; } } diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp index 4262663b173..c24c7a5a3fe 100644 --- a/src/cpp/cpp_constructor.cpp +++ b/src/cpp/cpp_constructor.cpp @@ -113,7 +113,7 @@ optionalt cpp_typecheckt::cpp_constructor( auto i_code = cpp_constructor(source_location, index, tmp_operands); if(i_code.has_value()) - new_code.add(std::move(i_code.value())); + new_code.add(std::move(*i_code)); } return std::move(new_code); } diff --git a/src/cpp/cpp_destructor.cpp b/src/cpp/cpp_destructor.cpp index 2282b5d4186..472f500798a 100644 --- a/src/cpp/cpp_destructor.cpp +++ b/src/cpp/cpp_destructor.cpp @@ -64,7 +64,7 @@ optionalt cpp_typecheckt::cpp_destructor( auto i_code = cpp_destructor(source_location, index); if(i_code.has_value()) - new_code.add_to_operands(std::move(i_code.value())); + new_code.add_to_operands(std::move(*i_code)); } return std::move(new_code); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index 7687c1303ac..250a111acda 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -188,7 +188,7 @@ void cpp_typecheckt::static_and_dynamic_initialization() auto call = cpp_constructor(symbol.location, symbol_expr, ops); if(call.has_value()) - init_block.add(call.value()); + init_block.add(*call); } } diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp index 15e4e32a0e2..d2c609bd171 100644 --- a/src/cpp/cpp_typecheck_code.cpp +++ b/src/cpp/cpp_typecheck_code.cpp @@ -374,7 +374,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code) cpp_constructor(code.source_location(), symbol_expr, code.operands()); if(call.has_value()) - code.swap(call.value()); + code.swap(*call); else { auto source_location = code.source_location(); @@ -491,7 +491,7 @@ void cpp_typecheckt::typecheck_decl(codet &code) symbol.location, object_expr, declarator.init_args().operands()); if(constructor_call.has_value()) - new_code.add_to_operands(std::move(constructor_call.value())); + new_code.add_to_operands(std::move(*constructor_call)); } } diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 193f1515dfc..d38b5bb853a 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -760,7 +760,7 @@ void cpp_typecheckt::typecheck_compound_declarator( auto defcode = cpp_constructor(source_locationt(), symexpr, ops); CHECK_RETURN(defcode.has_value()); - new_symbol->value.swap(defcode.value()); + new_symbol->value.swap(*defcode); } } } diff --git a/src/cpp/cpp_typecheck_declaration.cpp b/src/cpp/cpp_typecheck_declaration.cpp index c1e0043b679..eadda2012f8 100644 --- a/src/cpp/cpp_typecheck_declaration.cpp +++ b/src/cpp/cpp_typecheck_declaration.cpp @@ -182,7 +182,7 @@ void cpp_typecheckt::convert_non_template_declaration( declarator.init_args().operands()); if(constructor.has_value()) - symbol.value = constructor.value(); + symbol.value = *constructor; else symbol.value = nil_exprt(); } diff --git a/src/cpp/cpp_typecheck_destructor.cpp b/src/cpp/cpp_typecheck_destructor.cpp index 4a7683a5f9e..f4bec479d41 100644 --- a/src/cpp/cpp_typecheck_destructor.cpp +++ b/src/cpp/cpp_typecheck_destructor.cpp @@ -124,7 +124,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr) disable_access_control = disabled_access_control; if(dtor_code.has_value()) - block.add(dtor_code.value()); + block.add(*dtor_code); } if(symbol.type.id() == ID_union) @@ -149,7 +149,7 @@ codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr) disable_access_control = disabled_access_control; if(dtor_code.has_value()) - block.add(dtor_code.value()); + block.add(*dtor_code); } return std::move(block); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index 10d112a0508..a27d8029ae3 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -810,7 +810,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) expr.find_source_location(), object_expr, initializer.operands()); if(code.has_value()) - expr.add(ID_initializer).swap(code.value()); + expr.add(ID_initializer).swap(*code); else expr.add(ID_initializer) = nil_exprt(); @@ -821,7 +821,7 @@ void cpp_typecheckt::typecheck_expr_new(exprt &expr) if(size_of_opt.has_value()) { auto &sizeof_expr = static_cast(expr.add(ID_sizeof)); - sizeof_expr = size_of_opt.value(); + sizeof_expr = *size_of_opt; sizeof_expr.add(ID_C_c_sizeof_type) = expr.type().subtype(); } } @@ -1041,8 +1041,8 @@ void cpp_typecheckt::typecheck_expr_delete(exprt &expr) if(destructor_code.has_value()) { // this isn't typechecked yet - typecheck_code(destructor_code.value()); - expr.set(ID_destructor, destructor_code.value()); + typecheck_code(*destructor_code); + expr.set(ID_destructor, *destructor_code); } else expr.set(ID_destructor, nil_exprt()); diff --git a/src/cpp/cpp_typecheck_initializer.cpp b/src/cpp/cpp_typecheck_initializer.cpp index 2fbda5d90a9..e8c5a7a7aeb 100644 --- a/src/cpp/cpp_typecheck_initializer.cpp +++ b/src/cpp/cpp_typecheck_initializer.cpp @@ -187,7 +187,7 @@ void cpp_typecheckt::convert_initializer(symbolt &symbol) cpp_constructor(symbol.value.source_location(), expr_symbol, ops); if(constructor.has_value()) - symbol.value = constructor.value(); + symbol.value = *constructor; else symbol.value = nil_exprt(); } diff --git a/src/crangler/c_wrangler.cpp b/src/crangler/c_wrangler.cpp index 369bf736f8e..33e3e14a3e3 100644 --- a/src/crangler/c_wrangler.cpp +++ b/src/crangler/c_wrangler.cpp @@ -371,7 +371,7 @@ static void mangle_function( if(function_config.stub.has_value()) { // replace by stub - out << function_config.stub.value(); + out << *function_config.stub; } else { diff --git a/src/goto-analyzer/show_on_source.cpp b/src/goto-analyzer/show_on_source.cpp index f7a1c1981f8..7aba668fbca 100644 --- a/src/goto-analyzer/show_on_source.cpp +++ b/src/goto-analyzer/show_on_source.cpp @@ -45,7 +45,7 @@ get_source_files(const goto_modelt &goto_model, const ai_baset &ai) { const auto file = show_location(ai, i_it); if(file.has_value()) - files.insert(file.value()); + files.insert(*file); } } @@ -98,7 +98,7 @@ void show_on_source( forall_goto_program_instructions(i_it, f.second.body) { const auto file = show_location(ai, i_it); - if(file.has_value() && file.value() == source_file) + if(file.has_value() && *file == source_file) { const std::size_t line_no = stoull(id2string(i_it->source_location().get_line())); diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index d229d885c95..bee7fa60e66 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -382,17 +382,17 @@ bool taint_analysist::operator()( if(use_json) { - std::ofstream json_out(json_file_name.value()); + std::ofstream json_out(*json_file_name); if(!json_out) { - log.error() << "Failed to open json output '" << json_file_name.value() - << "'" << messaget::eom; + log.error() << "Failed to open json output '" << *json_file_name << "'" + << messaget::eom; return true; } - log.status() << "Analysis result is written to '" - << json_file_name.value() << "'" << messaget::eom; + log.status() << "Analysis result is written to '" << *json_file_name + << "'" << messaget::eom; json_out << json_result << '\n'; } diff --git a/src/goto-cc/cl_message_handler.cpp b/src/goto-cc/cl_message_handler.cpp index bf3d360d107..dccc0b01a09 100644 --- a/src/goto-cc/cl_message_handler.cpp +++ b/src/goto-cc/cl_message_handler.cpp @@ -43,9 +43,9 @@ void cl_message_handlert::print( if(full_path.has_value() && !line.empty()) { #ifdef _MSC_VER - std::ifstream in(widen(full_path.value())); + std::ifstream in(widen(*full_path)); #else - std::ifstream in(full_path.value()); + std::ifstream in(*full_path); #endif if(in) { diff --git a/src/goto-cc/gcc_message_handler.cpp b/src/goto-cc/gcc_message_handler.cpp index 53e7a4e00e4..b745f3a9eb5 100644 --- a/src/goto-cc/gcc_message_handler.cpp +++ b/src/goto-cc/gcc_message_handler.cpp @@ -69,9 +69,9 @@ void gcc_message_handlert::print( if(file_name.has_value() && !line.empty()) { #ifdef _MSC_VER - std::ifstream in(widen(file_name.value())); + std::ifstream in(widen(*file_name)); #else - std::ifstream in(file_name.value()); + std::ifstream in(*file_name); #endif if(in) { diff --git a/src/goto-harness/goto_harness_generator.cpp b/src/goto-harness/goto_harness_generator.cpp index 87f4b48d787..99b9e836a2e 100644 --- a/src/goto-harness/goto_harness_generator.cpp +++ b/src/goto-harness/goto_harness_generator.cpp @@ -46,7 +46,7 @@ std::size_t require_one_size_value( auto value = string2optional(string_value, 10); if(value.has_value()) { - return value.value(); + return *value; } else { diff --git a/src/goto-harness/goto_harness_parse_options.cpp b/src/goto-harness/goto_harness_parse_options.cpp index cf3d26687ee..2b77160f1c3 100644 --- a/src/goto-harness/goto_harness_parse_options.cpp +++ b/src/goto-harness/goto_harness_parse_options.cpp @@ -119,7 +119,7 @@ int goto_harness_parse_optionst::doit() throw deserialization_exceptiont{"failed to read goto program from file '" + got_harness_config.in_file + "'"}; } - auto goto_model = std::move(read_goto_binary_result.value()); + auto goto_model = std::move(*read_goto_binary_result); auto const goto_model_without_harness_symbols = get_symbol_names_from_goto_model(goto_model); diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 1a79b787da4..681a892ad9c 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -39,7 +39,7 @@ bool recursive_initialization_configt::handle_option( string2optional(value, 10); if(user_min_null_tree_depth.has_value()) { - min_null_tree_depth = user_min_null_tree_depth.value(); + min_null_tree_depth = *user_min_null_tree_depth; } else { @@ -57,7 +57,7 @@ bool recursive_initialization_configt::handle_option( string2optional(value, 10); if(user_max_nondet_tree_depth.has_value()) { - max_nondet_tree_depth = user_max_nondet_tree_depth.value(); + max_nondet_tree_depth = *user_max_nondet_tree_depth; } else { @@ -203,7 +203,7 @@ void recursive_initializationt::initialize( if(size_var.has_value()) { const symbol_exprt &size_symbol = - goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr(); + goto_model.symbol_table.lookup_ref(*size_var).symbol_expr(); body.add(code_function_callt{ fun_symbol.symbol_expr(), {depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}}); @@ -303,8 +303,8 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) if(expr.id() == ID_symbol) { expr_name = to_symbol_expr(expr).get_identifier(); - is_nullable = initialization_config.potential_null_function_pointers.count( - expr_name.value()); + is_nullable = + initialization_config.potential_null_function_pointers.count(*expr_name); if(should_be_treated_as_array(*expr_name)) { size_var = get_associated_size_variable(*expr_name); diff --git a/src/goto-instrument/aggressive_slicer.cpp b/src/goto-instrument/aggressive_slicer.cpp index 46f092774b4..33264c898c2 100644 --- a/src/goto-instrument/aggressive_slicer.cpp +++ b/src/goto-instrument/aggressive_slicer.cpp @@ -100,7 +100,7 @@ void aggressive_slicert::doit() auto property_loc = find_property(p, goto_model.goto_functions); if(!property_loc.has_value()) throw "unable to find property in call graph"; - note_functions_to_keep(property_loc.value().get_function()); + note_functions_to_keep(property_loc->get_function()); } // Add functions within distance of shortest path functions diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 430535b3b32..2562f5ebd5b 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -889,7 +889,7 @@ void code_contractst::apply_function_contract( // ... for the return value if(call_ret_opt.has_value()) { - auto &call_ret = call_ret_opt.value(); + auto &call_ret = *call_ret_opt; auto &loc = call_ret.source_location(); auto &type = call_ret.type(); @@ -920,7 +920,7 @@ void code_contractst::apply_function_contract( { function_body.output_instruction(ns, "", log.warning(), *target); auto dead_inst = - goto_programt::make_dead(to_symbol_expr(call_ret_opt.value()), location); + goto_programt::make_dead(to_symbol_expr(*call_ret_opt), location); function_body.insert_before_swap(target, dead_inst); ++target; } @@ -1514,7 +1514,7 @@ void code_contractst::add_contract_check( if(code_type.return_type() != empty_typet()) { check.add(goto_programt::make_set_return_value( - return_stmt.value().return_value(), skip->source_location())); + return_stmt->return_value(), skip->source_location())); } // prepend the new code to dest diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index 835f0eb3377..2b051b6cbc4 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -323,7 +323,7 @@ void instrument_spec_assignst::instrument_instructions( { instruction_it++; if(cfg_info_opt.has_value()) - cfg_info_opt.value().step(); + cfg_info_opt->step(); continue; } @@ -398,7 +398,7 @@ void instrument_spec_assignst::instrument_instructions( // Move to the next instruction instruction_it++; if(cfg_info_opt.has_value()) - cfg_info_opt.value().step(); + cfg_info_opt->step(); } } @@ -488,14 +488,15 @@ car_exprt instrument_spec_assignst::create_car_expr( size.has_value(), "no definite size for lvalue target:\n" + target.pretty()); - return {condition, - target, - typecast_exprt::conditional_cast( - address_of_exprt{target}, pointer_type(char_type())), - typecast_exprt::conditional_cast(size.value(), signed_size_type()), - valid_var, - lower_bound_var, - upper_bound_var}; + return { + condition, + target, + typecast_exprt::conditional_cast( + address_of_exprt{target}, pointer_type(char_type())), + typecast_exprt::conditional_cast(*size, signed_size_type()), + valid_var, + lower_bound_var, + upper_bound_var}; }; UNREACHABLE; @@ -677,9 +678,7 @@ exprt instrument_spec_assignst::inclusion_check_full( for(const auto &pair : from_stack_alloc) { // skip dead targets - if( - cfg_info_opt.has_value() && - !cfg_info_opt.value().is_maybe_alive(pair.first)) + if(cfg_info_opt.has_value() && !cfg_info_opt->is_maybe_alive(pair.first)) continue; disjuncts.push_back(inclusion_check_single(car, pair.second)); @@ -818,7 +817,7 @@ bool instrument_spec_assignst::must_check_assign( } if(cfg_info_opt.has_value()) - return !cfg_info_opt.value().is_local(symbol_expr->get_identifier()); + return !cfg_info_opt->is_local(symbol_expr->get_identifier()); } return true; @@ -839,7 +838,7 @@ bool instrument_spec_assignst::must_track_decl( { if(cfg_info_opt.has_value()) { - return cfg_info_opt.value().is_not_local_or_dirty_local( + return cfg_info_opt->is_not_local_or_dirty_local( target->decl_symbol().get_identifier()); } // Unless proved non-dirty by the CFG analysis we assume it is dirty. @@ -856,7 +855,7 @@ bool instrument_spec_assignst::must_track_dead( if(!cfg_info_opt.has_value()) return true; - return cfg_info_opt.value().is_not_local_or_dirty_local( + return cfg_info_opt->is_not_local_or_dirty_local( target->dead_symbol().get_identifier()); } diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index 51bf3e825d4..afd7edf1790 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -200,8 +200,8 @@ void print_global_state_size(const goto_modelt &goto_model) } const auto bits = pointer_offset_bits(symbol.type, ns); - if(bits.has_value() && bits.value() > 0) - total_size += bits.value(); + if(bits.has_value() && *bits > 0) + total_size += *bits; } std::cout << "Total size of global objects: " << total_size << " bits\n"; diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 3de84264a78..cb40ef55d60 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -243,7 +243,7 @@ void dump_ct::operator()(std::ostream &os) !harness && func_entry != goto_functions.function_map.end() && func_entry->second.body_available() && (symbol.name == ID_main || - (config.main.has_value() && symbol.name == config.main.value()))) + (config.main.has_value() && symbol.name == *config.main))) { skip_function_main=true; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efea60220bd..170d62399c4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -990,7 +990,7 @@ void goto_instrument_parse_optionst::get_goto_program() if(!result.has_value()) throw 0; - goto_model = std::move(result.value()); + goto_model = std::move(*result); config.set_from_symbol_table(goto_model.symbol_table); } diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp index ca3c5d1e26b..b37def5bc00 100644 --- a/src/goto-instrument/model_argc_argv.cpp +++ b/src/goto-instrument/model_argc_argv.cpp @@ -54,7 +54,7 @@ bool model_argc_argv( } const symbolt &main_symbol = - ns.lookup(config.main.has_value() ? config.main.value() : ID_main); + ns.lookup(config.main.has_value() ? *config.main : ID_main); if(main_symbol.mode!=ID_C) { diff --git a/src/goto-programs/allocate_objects.cpp b/src/goto-programs/allocate_objects.cpp index 91de4260ea0..421802a689a 100644 --- a/src/goto-programs/allocate_objects.cpp +++ b/src/goto-programs/allocate_objects.cpp @@ -156,7 +156,7 @@ exprt allocate_objectst::allocate_dynamic_object_symbol( add_created_symbol(malloc_sym); code_frontend_assignt assign = - make_allocate_code(malloc_sym.symbol_expr(), object_size.value()); + make_allocate_code(malloc_sym.symbol_expr(), *object_size); output_code.add(assign); exprt malloc_symbol_expr = typecast_exprt::conditional_cast( diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 92ca061523e..8a283ea3e47 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1800,8 +1800,8 @@ bool goto_convertt::get_string_constant( if(!i.has_value()) return true; - if(i.value() != 0) // to skip terminating 0 - result += static_cast(i.value()); + if(*i != 0) // to skip terminating 0 + result += static_cast(*i); } return value=result, false; diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 165f9fcfdac..1f02459ac53 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -983,9 +983,9 @@ void goto_programt::instructiont::transform( auto new_assign_lhs = f(assign_lhs()); auto new_assign_rhs = f(assign_rhs()); if(new_assign_lhs.has_value()) - assign_lhs_nonconst() = new_assign_lhs.value(); + assign_lhs_nonconst() = *new_assign_lhs; if(new_assign_rhs.has_value()) - assign_rhs_nonconst() = new_assign_rhs.value(); + assign_rhs_nonconst() = *new_assign_rhs; } break; @@ -1051,7 +1051,7 @@ void goto_programt::instructiont::transform( { auto new_condition = f(get_condition()); if(new_condition.has_value()) - set_condition(new_condition.value()); + set_condition(*new_condition); } } } diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp index fffe09c59d1..632f23acb66 100644 --- a/src/goto-programs/interpreter_evaluate.cpp +++ b/src/goto-programs/interpreter_evaluate.cpp @@ -261,7 +261,7 @@ bool interpretert::memory_offset_to_byte_offset( const auto member_offset_result = member_offset(st, comp.get_name(), ns); CHECK_RETURN(member_offset_result.has_value()); - result = member_offset_result.value() + subtype_result; + result = *member_offset_result + subtype_result; return ret; } else diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index d26b9b0afb2..245492fe005 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -75,8 +75,7 @@ void mm_io( auto call = goto_programt::make_function_call( mm_io_r_value, mm_io_r, - {typecast_exprt(d.pointer(), pt), - typecast_exprt(size_opt.value(), st)}, + {typecast_exprt(d.pointer(), pt), typecast_exprt(*size_opt, st)}, source_location); goto_function.body.insert_before_swap(it, call); it++; @@ -98,7 +97,7 @@ void mm_io( const code_function_callt fc( mm_io_w, {typecast_exprt(d.pointer(), pt), - typecast_exprt(size_opt.value(), st), + typecast_exprt(*size_opt, st), typecast_exprt(a_rhs, vt)}); goto_function.body.insert_before_swap(it); *it = goto_programt::make_function_call(fc, source_location); diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp index 230468a18ad..e155b40fb3a 100644 --- a/src/goto-symex/symex_clean_expr.cpp +++ b/src/goto-symex/symex_clean_expr.cpp @@ -90,11 +90,11 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns) auto array_size = size_of_expr(expr.type(), ns); CHECK_RETURN(array_size.has_value()); if(do_simplify) - simplify(array_size.value(), ns); + simplify(*array_size, ns); expr = make_byte_extract( expr, from_integer(0, c_index_type()), - array_typet(char_type(), array_size.value())); + array_typet(char_type(), *array_size)); } // given an array type T[N], i.e., an array of N elements of type T, and a @@ -108,8 +108,8 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns) typecast_exprt::conditional_cast(ode.offset(), array_size_type); auto subtype_size_opt = size_of_expr(subtype, ns); CHECK_RETURN(subtype_size_opt.has_value()); - exprt subtype_size = typecast_exprt::conditional_cast( - subtype_size_opt.value(), array_size_type); + exprt subtype_size = + typecast_exprt::conditional_cast(*subtype_size_opt, array_size_type); new_offset = div_exprt(new_offset, subtype_size); minus_exprt subtraction{prev_array_type.size(), new_offset}; if_exprt new_size{ diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index da047c50625..981b7d01585 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -451,8 +451,8 @@ void goto_symext::symex_end_of_function(statet &state) return_value_symbol.has_value(), "must have return value symbol when assigning call lhs"); // the type of the call lhs and the return type might not match - auto casted_return_value = typecast_exprt::conditional_cast( - return_value_symbol.value(), call_lhs.type()); + auto casted_return_value = + typecast_exprt::conditional_cast(*return_value_symbol, call_lhs.type()); symex_assign(state, call_lhs, casted_return_value); } } diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 3539348e6b1..26b3cc25d52 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -188,11 +188,11 @@ void goto_symext::symex_other( { auto array_size = size_of_expr(array_expr.type(), ns); CHECK_RETURN(array_size.has_value()); - do_simplify(array_size.value()); + do_simplify(*array_size); array_expr = make_byte_extract( array_expr, from_integer(0, c_index_type()), - array_typet(char_type(), array_size.value())); + array_typet(char_type(), *array_size)); } const array_typet &array_type = to_array_type(array_expr.type()); diff --git a/src/goto-symex/symex_set_return_value.cpp b/src/goto-symex/symex_set_return_value.cpp index c0cbc28e83d..720fb587e67 100644 --- a/src/goto-symex/symex_set_return_value.cpp +++ b/src/goto-symex/symex_set_return_value.cpp @@ -21,6 +21,6 @@ void goto_symext::symex_set_return_value( framet &frame = state.call_stack().top(); if(frame.return_value_symbol.has_value()) { - symex_assign(state, frame.return_value_symbol.value(), return_value); + symex_assign(state, *frame.return_value_symbol, return_value); } } diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 422805948c3..cfab314a16a 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -65,7 +65,7 @@ bool jsil_entry_point( std::list matches; for(const auto &symbol_name_entry : - equal_range(symbol_table.symbol_base_map, config.main.value())) + equal_range(symbol_table.symbol_base_map, *config.main)) { // look it up symbol_tablet::symbolst::const_iterator s_it = @@ -81,7 +81,7 @@ bool jsil_entry_point( if(matches.empty()) { messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() << "' not found" + message.error() << "main symbol '" << *config.main << "' not found" << messaget::eom; return true; // give up } @@ -89,8 +89,8 @@ bool jsil_entry_point( if(matches.size()>=2) { messaget message(message_handler); - message.error() << "main symbol '" << config.main.value() - << "' is ambiguous" << messaget::eom; + message.error() << "main symbol '" << *config.main << "' is ambiguous" + << messaget::eom; return true; } diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 5258d149210..8f79f78f5ad 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -169,9 +169,8 @@ void remove_internal_symbols( { // body? not local (i.e., "static")? if( - has_body && - (!is_file_local || - (config.main.has_value() && symbol.base_name == config.main.value()))) + has_body && (!is_file_local || (config.main.has_value() && + symbol.base_name == *config.main))) { get_symbols(ns, symbol, exported); } diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp index 3e6b93d5dc9..a6aa78fd5d1 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.cpp +++ b/src/memory-analyzer/memory_analyzer_parse_options.cpp @@ -113,7 +113,7 @@ int memory_analyzer_parse_optionst::doit() "cannot read goto binary '" + binary + "'"); } - const goto_modelt goto_model(std::move(opt.value())); + const goto_modelt goto_model(std::move(*opt)); gdb_value_extractort gdb_value_extractor( goto_model.symbol_table, cmdline.args); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 8717eb8a740..9f4a5777e08 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -625,17 +625,16 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( auto subexpr = get_subexpression_at_offset( root_object_subexpression, o.offset(), dereference_type, ns); if(subexpr.has_value()) - simplify(subexpr.value(), ns); + simplify(*subexpr, ns); if( - subexpr.has_value() && - subexpr.value().id() != ID_byte_extract_little_endian && - subexpr.value().id() != ID_byte_extract_big_endian) + subexpr.has_value() && subexpr->id() != ID_byte_extract_little_endian && + subexpr->id() != ID_byte_extract_big_endian) { // Successfully found a member, array index, or combination thereof // that matches the desired type and offset: - result.value = subexpr.value(); + result.value = *subexpr; result.pointer = typecast_exprt::conditional_cast( - address_of_exprt{skip_typecast(subexpr.value())}, pointer_type); + address_of_exprt{skip_typecast(*subexpr)}, pointer_type); return result; } diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index c8de549a2df..77568bf315b 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -28,8 +28,8 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value()) return conversion_failed(expr); - auto upper_as_int = maybe_upper_as_int.value(); - auto lower_as_int = maybe_lower_as_int.value(); + auto upper_as_int = *maybe_upper_as_int; + auto lower_as_int = *maybe_lower_as_int; DATA_INVARIANT_WITH_DIAGNOSTICS( upper_as_int >= 0 && upper_as_int < src_bv.size(), diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index a399606ae50..abd2ed0fc0f 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -97,7 +97,7 @@ bvt boolbvt::convert_index(const index_exprt &expr) auto maybe_index_value = numeric_cast(index); if(maybe_index_value.has_value()) { - return convert_index(array, maybe_index_value.value()); + return convert_index(array, *maybe_index_value); } } diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index fb5e201aa3e..fae454370cc 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -195,8 +195,8 @@ static optionalt eager_quantifier_instantiation( if(!min_i.has_value() || !max_i.has_value()) return nullopt; - mp_integer lb = numeric_cast_v(min_i.value()); - mp_integer ub = numeric_cast_v(max_i.value()); + mp_integer lb = numeric_cast_v(*min_i); + mp_integer ub = numeric_cast_v(*max_i); if(lb > ub) return nullopt; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 06e69676aae..ba41eb04022 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -952,8 +952,8 @@ void bv_pointerst::do_postponed( if(!size_expr.has_value()) continue; - const exprt object_size = typecast_exprt::conditional_cast( - size_expr.value(), postponed.expr.type()); + const exprt object_size = + typecast_exprt::conditional_cast(*size_expr, postponed.expr.type()); // only compare object part pointer_typet pt = pointer_type(expr.type()); diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 4dfaa2fc34e..13b734e117c 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -116,7 +116,7 @@ exprt pointer_logict::pointer_expr( auto deep_object_opt = get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns); CHECK_RETURN(deep_object_opt.has_value()); - exprt deep_object = deep_object_opt.value(); + exprt deep_object = *deep_object_opt; simplify(deep_object, ns); if( deep_object.id() != ID_byte_extract_little_endian && diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index 925f4446fb9..a3b6fc8e846 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -1146,9 +1146,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) { upper_bound_opt = simplify_expr( plus_exprt( - upper_bound_opt.value(), + *upper_bound_opt, typecast_exprt::conditional_cast( - src.offset(), upper_bound_opt.value().type())), + src.offset(), upper_bound_opt->type())), ns); } else if(src.type().id() == ID_empty) @@ -1220,7 +1220,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) plus_exprt new_offset( unpacked.offset(), typecast_exprt::conditional_cast( - member_offset_opt.value(), unpacked.offset().type())); + *member_offset_opt, unpacked.offset().type())); byte_extract_exprt tmp(unpacked); tmp.type()=comp.type(); @@ -1603,8 +1603,7 @@ static exprt lower_byte_update_array_vector_non_const( CHECK_RETURN(subtype_size_opt.has_value()); const exprt subtype_size = simplify_expr( - typecast_exprt::conditional_cast( - subtype_size_opt.value(), src.offset().type()), + typecast_exprt::conditional_cast(*subtype_size_opt, src.offset().type()), ns); // compute the index of the first element of the array/vector that may be @@ -1903,7 +1902,7 @@ static exprt lower_byte_update_struct( extract_opcode, src.op(), from_integer(0, src.offset().type()), - array_typet{bv_typet{8}, src_size_opt.value()}}; + array_typet{bv_typet{8}, *src_size_opt}}; byte_update_exprt bu = src; bu.set_op(lower_byte_extract(byte_extract_expr, ns)); @@ -2299,9 +2298,9 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) exprt update_value = src.value(); auto update_size_expr_opt = size_of_expr(update_value.type(), ns); CHECK_RETURN(update_size_expr_opt.has_value()); - simplify(update_size_expr_opt.value(), ns); + simplify(*update_size_expr_opt, ns); - if(!update_size_expr_opt.value().is_constant()) + if(!update_size_expr_opt->is_constant()) non_const_update_bound = *update_size_expr_opt; else { diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index a84d0c90260..9ddd97bc7c3 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -492,7 +492,7 @@ exprt smt2_convt::parse_array( auto maybe_size = numeric_cast(type.size()); if(maybe_size.has_value()) { - while(i < maybe_size.value()) + while(i < *maybe_size) { auto found_op = operands_map.find(i); if(found_op != operands_map.end()) @@ -1532,7 +1532,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(distance_int_op.has_value()) { - out << distance_int_op.value(); + out << *distance_int_op; } else UNEXPECTEDCASE( @@ -4212,8 +4212,8 @@ void smt2_convt::convert_member(const member_exprt &expr) CHECK_RETURN_WITH_DIAGNOSTICS( member_offset.has_value(), "failed to get struct member offset"); - out << "((_ extract " << (member_offset.value() + member_width - 1) << " " - << member_offset.value() << ") "; + out << "((_ extract " << (*member_offset + member_width - 1) << " " + << *member_offset << ") "; convert_expr(struct_op); out << ")"; } diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index 79a55b4bd0d..ad4fa9fb2d7 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -148,7 +148,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in) if(!parsed_opt.has_value()) break; - const auto &parsed = parsed_opt.value(); + const auto &parsed = *parsed_opt; if(parsed.id()=="sat") res=resultt::D_SATISFIABLE; diff --git a/src/solvers/smt2_incremental/smt_response_validation.cpp b/src/solvers/smt2_incremental/smt_response_validation.cpp index 143e0f03099..b2c8d1a717d 100644 --- a/src/solvers/smt2_incremental/smt_response_validation.cpp +++ b/src/solvers/smt2_incremental/smt_response_validation.cpp @@ -46,7 +46,7 @@ const smtt *response_or_errort::get_if_valid() const smt.has_value() == messages.empty(), "The response_or_errort class must be in the valid state or error state, " "exclusively."); - return smt.has_value() ? &smt.value() : nullptr; + return smt.has_value() ? &(*smt) : nullptr; } template diff --git a/src/solvers/strings/string_builtin_function.cpp b/src/solvers/strings/string_builtin_function.cpp index 0507281bd56..b595d913ed5 100644 --- a/src/solvers/strings/string_builtin_function.cpp +++ b/src/solvers/strings/string_builtin_function.cpp @@ -87,11 +87,10 @@ optionalt string_concat_char_builtin_functiont::eval( "character valuation should only contain constants and unknown"); return mp_integer(CHARACTER_FOR_UNKNOWN); }(); - input_opt.value().push_back(char_val); - const auto length = - from_integer(input_opt.value().size(), result.length_type()); + input_opt->push_back(char_val); + const auto length = from_integer(input_opt->size(), result.length_type()); const array_typet type(to_type_with_subtype(result.type()).subtype(), length); - return make_string(input_opt.value(), type); + return make_string(*input_opt, type); } /// Set of constraints enforcing that `result` is the concatenation @@ -133,12 +132,11 @@ optionalt string_set_char_builtin_functiont::eval( const auto position_opt = numeric_cast(get_value(position)); if(!input_opt || !char_opt || !position_opt) return {}; - if(0 <= *position_opt && *position_opt < input_opt.value().size()) - input_opt.value()[numeric_cast_v(*position_opt)] = *char_opt; - const auto length = - from_integer(input_opt.value().size(), result.length_type()); + if(0 <= *position_opt && *position_opt < input_opt->size()) + (*input_opt)[numeric_cast_v(*position_opt)] = *char_opt; + const auto length = from_integer(input_opt->size(), result.length_type()); const array_typet type(to_type_with_subtype(result.type()).subtype(), length); - return make_string(input_opt.value(), type); + return make_string(*input_opt, type); } /// Set of constraints ensuring that `result` is similar to `input` @@ -219,15 +217,14 @@ optionalt string_to_lower_case_builtin_functiont::eval( auto input_opt = eval_string(input, get_value); if(!input_opt) return {}; - for(mp_integer &c : input_opt.value()) + for(mp_integer &c : *input_opt) { if(eval_is_upper_case(c)) c += 0x20; } - const auto length = - from_integer(input_opt.value().size(), result.length_type()); + const auto length = from_integer(input_opt->size(), result.length_type()); const array_typet type(to_type_with_subtype(result.type()).subtype(), length); - return make_string(input_opt.value(), type); + return make_string(*input_opt, type); } /// Expression which is true for uppercase characters of the Basic Latin and @@ -313,15 +310,14 @@ optionalt string_to_upper_case_builtin_functiont::eval( auto input_opt = eval_string(input, get_value); if(!input_opt) return {}; - for(mp_integer &c : input_opt.value()) + for(mp_integer &c : *input_opt) { if(eval_is_upper_case(c - 0x20)) c -= 0x20; } - const auto length = - from_integer(input_opt.value().size(), result.length_type()); + const auto length = from_integer(input_opt->size(), result.length_type()); const array_typet type(to_type_with_subtype(result.type()).subtype(), length); - return make_string(input_opt.value(), type); + return make_string(*input_opt, type); } /// Set of constraints ensuring `result` corresponds to `input` in which @@ -418,7 +414,7 @@ exprt string_of_int_builtin_functiont::length_constraint() const { const typet &type = result.length_type(); const auto radix_opt = numeric_cast(radix); - const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2; + const auto radix_value = radix_opt.value_or(2); const std::size_t upper_bound = max_printed_string_length(arg.type(), radix_value); const exprt negative_arg = diff --git a/src/solvers/strings/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp index 6fa966a6ac9..bdb7b2fb87f 100644 --- a/src/solvers/strings/string_constraint_instantiation.cpp +++ b/src/solvers/strings/string_constraint_instantiation.cpp @@ -70,7 +70,7 @@ linear_functiont::linear_functiont(const exprt &f) to_process.pop_back(); if(auto integer = numeric_cast(cur)) { - constant_coefficient += positive ? integer.value() : -integer.value(); + constant_coefficient += positive ? *integer : -*integer; } else if(cur.id() == ID_plus) { diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp index 9b24668cb94..af46ce0b31d 100644 --- a/src/solvers/strings/string_format_builtin_function.cpp +++ b/src/solvers/strings/string_format_builtin_function.cpp @@ -519,7 +519,7 @@ optionalt string_format_builtin_functiont::eval( return {}; const std::vector format_strings = - parse_format_string(format_string.value()); + parse_format_string(*format_string); std::vector result_vector; std::size_t arg_count = 0; @@ -593,7 +593,7 @@ string_constraintst string_format_builtin_functiont::constraints( auto result_constraint_pair = add_axioms_for_format( generator, result, - format_string.value(), + *format_string, inputs, // TODO: get rid of this argument messaget{message_handler}); @@ -771,7 +771,7 @@ exprt string_format_builtin_functiont::length_constraint() const exprt::operandst constraints; const std::vector format_strings = - parse_format_string(format_string.value()); + parse_format_string(*format_string); std::vector intermediary_string_lengths; std::size_t arg_count = 0; const typet &index_type = result.length_type(); diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 634f9159f2f..91d82458c9e 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -964,7 +964,7 @@ static optionalt get_valid_array_size( exprt size_val; if(size_from_pool.has_value()) { - const exprt size = size_from_pool.value(); + const exprt size = *size_from_pool; size_val = simplify_expr(super_get(size), ns); if(size_val.id() != ID_constant) { @@ -1011,7 +1011,7 @@ static optionalt get_array( return {}; } - const size_t n = numeric_cast(size.value()).value(); + const size_t n = *numeric_cast(*size); if(n > MAX_CONCRETE_STRING_SIZE) { @@ -1032,7 +1032,7 @@ static optionalt get_array( const exprt arr_val = simplify_expr(super_get(arr), ns); const typet char_type = to_array_type(arr.type()).subtype(); - const typet &index_type = size.value().type(); + const typet &index_type = size->type(); if( const auto &array = interval_sparse_arrayt::of_expr( @@ -1879,7 +1879,7 @@ exprt string_refinementt::get(const exprt &expr) const const auto &length_from_pool = generator.array_pool.get_length_if_exists(arr)) { - const exprt length = super_get(length_from_pool.value()); + const exprt length = super_get(*length_from_pool); if(const auto n = numeric_cast(length)) { diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 47e95bf3210..51d212a99f0 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -209,10 +209,9 @@ bool statement_list_entry_point( // Find main symbol given by the user. if(config.main.has_value()) { - if(is_main_symbol_invalid( - symbol_table, message_handler, config.main.value())) + if(is_main_symbol_invalid(symbol_table, message_handler, *config.main)) return true; - main_symbol_name = config.main.value(); + main_symbol_name = *config.main; } // Fallback: Search for block with TIA main standard name. // TODO: Support the standard entry point of STL (organisation blocks). diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp index b0abbb3cb3b..2ab4fba5f22 100644 --- a/src/statement-list/statement_list_parse_tree_io.cpp +++ b/src/statement-list/statement_list_parse_tree_io.cpp @@ -187,7 +187,7 @@ void output_var_declaration( if(declaration.default_value) { const constant_exprt &constant = - to_constant_expr(declaration.default_value.value()); + to_constant_expr(*declaration.default_value); output_constant(os, constant); } else diff --git a/src/util/cmdline.cpp b/src/util/cmdline.cpp index 84530430ae1..0fe17a166f6 100644 --- a/src/util/cmdline.cpp +++ b/src/util/cmdline.cpp @@ -232,7 +232,7 @@ cmdlinet::get_argument_suggestions(const std::string &unknown_argument) const auto long_name = "--" + option.optstring; if(auto distance = argument_matcher.get_edit_distance(long_name)) { - argument_suggestions.push_back({distance.value(), long_name}); + argument_suggestions.push_back({*distance, long_name}); } } if(!option.islong) @@ -240,7 +240,7 @@ cmdlinet::get_argument_suggestions(const std::string &unknown_argument) const auto short_name = std::string{"-"} + option.optchar; if(auto distance = argument_matcher.get_edit_distance(short_name)) { - argument_suggestions.push_back({distance.value(), short_name}); + argument_suggestions.push_back({*distance, short_name}); } } } diff --git a/src/util/pointer_expr.cpp b/src/util/pointer_expr.cpp index f125aef62ea..da9ac9d8400 100644 --- a/src/util/pointer_expr.cpp +++ b/src/util/pointer_expr.cpp @@ -44,7 +44,7 @@ static void build_object_descriptor_rec( dest.offset(), mult_exprt( typecast_exprt::conditional_cast(index.index(), c_index_type()), - typecast_exprt::conditional_cast(sub_size.value(), c_index_type()))); + typecast_exprt::conditional_cast(*sub_size, c_index_type()))); } else if(expr.id() == ID_member) { @@ -57,8 +57,7 @@ static void build_object_descriptor_rec( CHECK_RETURN(offset.has_value()); dest.offset() = plus_exprt( - dest.offset(), - typecast_exprt::conditional_cast(offset.value(), c_index_type())); + dest.offset(), typecast_exprt::conditional_cast(*offset, c_index_type())); } else if( expr.id() == ID_byte_extract_little_endian || diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 0dcfe6c188d..cba7b906e9d 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -270,7 +270,7 @@ optionalt member_offset_expr( auto sub_size = size_of_expr(subtype, ns); if(!sub_size.has_value()) return {}; // give up - result = plus_exprt(result, sub_size.value()); + result = plus_exprt(result, *sub_size); } } @@ -302,9 +302,9 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) return {}; const auto size_casted = - typecast_exprt::conditional_cast(size, sub.value().type()); + typecast_exprt::conditional_cast(size, sub->type()); - return simplify_expr(mult_exprt{size_casted, sub.value()}, ns); + return simplify_expr(mult_exprt{size_casted, *sub}, ns); } else if(type.id()==ID_vector) { @@ -329,9 +329,9 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) return {}; const auto size_casted = - typecast_exprt::conditional_cast(size, sub.value().type()); + typecast_exprt::conditional_cast(size, sub->type()); - return simplify_expr(mult_exprt{size_casted, sub.value()}, ns); + return simplify_expr(mult_exprt{size_casted, *sub}, ns); } else if(type.id()==ID_complex) { @@ -339,8 +339,8 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) if(!sub.has_value()) return {}; - exprt size = from_integer(2, sub.value().type()); - return simplify_expr(mult_exprt{std::move(size), sub.value()}, ns); + exprt size = from_integer(2, sub->type()); + return simplify_expr(mult_exprt{std::move(size), *sub}, ns); } else if(type.id()==ID_struct) { @@ -382,7 +382,7 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) if(!sub_size_opt.has_value()) return {}; - result = plus_exprt(result, sub_size_opt.value()); + result = plus_exprt(result, *sub_size_opt); } } @@ -411,7 +411,7 @@ optionalt size_of_expr(const typet &type, const namespacet &ns) auto sub_size_opt = size_of_expr(subtype, ns); if(!sub_size_opt.has_value()) return {}; - sub_size = sub_size_opt.value(); + sub_size = *sub_size_opt; } else { diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index dd03c43507d..407e0763961 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -79,7 +79,7 @@ exprt good_pointer_def( const and_exprt good_bounds{ not_exprt{object_lower_bound(pointer, nil_exprt())}, - not_exprt{object_upper_bound(pointer, size_of_expr_opt.value())}}; + not_exprt{object_upper_bound(pointer, *size_of_expr_opt)}}; return and_exprt(not_null, not_invalid, good_dynamic, good_bounds); } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index cf64b8636e3..5547f31b280 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1699,7 +1699,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) if(!const_bits_opt.has_value()) return unchanged(expr); - std::string const_bits=const_bits_opt.value(); + std::string const_bits = *const_bits_opt; DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty"); @@ -1760,7 +1760,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) !struct_has_flexible_array_member) { std::string bits_cut = std::string( - bits.value(), + *bits, numeric_cast_v(*offset * 8), numeric_cast_v(*el_size)); @@ -1806,10 +1806,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) break; } - exprt new_offset = simplify_rec( - plus_exprt{expr.offset(), - typecast_exprt::conditional_cast( - member_offset_opt.value(), expr.offset().type())}); + exprt new_offset = simplify_rec(plus_exprt{ + expr.offset(), + typecast_exprt::conditional_cast( + *member_offset_opt, expr.offset().type())}); byte_extract_exprt tmp = expr; tmp.type() = comp.type(); @@ -1839,10 +1839,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr) // try to refine it down to extracting from a member or an index in an array auto subexpr = get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns); - if(!subexpr.has_value() || subexpr.value() == expr) + if(!subexpr.has_value() || *subexpr == expr) return unchanged(expr); - return changed(simplify_rec(subexpr.value())); // recursive call + return changed(simplify_rec(*subexpr)); // recursive call } simplify_exprt::resultt<> diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index 876c3f06447..9f75b75f28c 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -665,7 +665,7 @@ simplify_exprt::simplify_object_size(const unary_exprt &expr) if(size_opt.has_value()) { const typet &expr_type = expr.type(); - exprt size = size_opt.value(); + exprt size = *size_opt; if(size.type() != expr_type) size = simplify_typecast(typecast_exprt(size, expr_type)); diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp index 3e88dc6e838..be49575640d 100644 --- a/src/util/simplify_expr_struct.cpp +++ b/src/util/simplify_expr_struct.cpp @@ -181,7 +181,7 @@ simplify_exprt::simplify_member(const member_exprt &expr) if(target_size.has_value()) { - mp_integer target_bits = target_size.value() * 8; + mp_integer target_bits = *target_size * 8; const auto bits = expr2bits(op, true, ns); if(bits.has_value() && @@ -227,10 +227,10 @@ simplify_exprt::simplify_member(const member_exprt &expr) // optimisation. if( equivalent_member.has_value() && - equivalent_member.value().id() != ID_byte_extract_little_endian && - equivalent_member.value().id() != ID_byte_extract_big_endian) + equivalent_member->id() != ID_byte_extract_little_endian && + equivalent_member->id() != ID_byte_extract_big_endian) { - auto tmp = equivalent_member.value(); + auto tmp = *equivalent_member; return changed(simplify_rec(tmp)); } } diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp index c48f1cc813a..1498913c859 100644 --- a/src/util/simplify_utils.cpp +++ b/src/util/simplify_utils.cpp @@ -471,7 +471,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns) auto tmp = expr2bits(*it, little_endian, ns); if(!tmp.has_value()) return {}; // failed - result += tmp.value(); + result += *tmp; } return result; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 686901503ab..42b42716368 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -164,10 +164,7 @@ static optionalt substitute_symbols_rec( substitute_symbols_rec(new_substitutions, binding_expr.where()); if(op_result.has_value()) return binding_exprt( - src.id(), - binding_expr.variables(), - op_result.value(), - binding_expr.type()); + src.id(), binding_expr.variables(), *op_result, binding_expr.type()); else return {}; } @@ -190,7 +187,7 @@ static optionalt substitute_symbols_rec( if(op_result.has_value()) { - op = op_result.value(); + op = *op_result; op_changed = true; } } @@ -199,7 +196,7 @@ static optionalt substitute_symbols_rec( substitute_symbols_rec(new_substitutions, binding_expr.where()); if(op_result.has_value()) { - new_let_expr.where() = op_result.value(); + new_let_expr.where() = *op_result; op_changed = true; } @@ -220,7 +217,7 @@ static optionalt substitute_symbols_rec( if(op_result.has_value()) { - op = op_result.value(); + op = *op_result; op_changed = true; } } @@ -256,7 +253,7 @@ exprt binding_exprt::instantiate(const operandst &values) const auto substitute_result = substitute_symbols_rec(substitutions, where()); if(substitute_result.has_value()) - return substitute_result.value(); + return *substitute_result; else return where(); // trivial case, variables not used } diff --git a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp index d2afe05f39b..e1e6c898d9d 100644 --- a/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp +++ b/unit/solvers/strings/string_format_builtin_function/length_of_decimal_int.cpp @@ -39,8 +39,7 @@ SCENARIO( THEN("length expression is " << oracle) { const int actual_int = - numeric_cast(to_constant_expr(simplify_expr(actual, ns))) - .value(); + *numeric_cast(to_constant_expr(simplify_expr(actual, ns))); REQUIRE(actual_int == oracle); } } diff --git a/unit/util/edit_distance.cpp b/unit/util/edit_distance.cpp index f24ee818517..f6a7097ba2a 100644 --- a/unit/util/edit_distance.cpp +++ b/unit/util/edit_distance.cpp @@ -11,7 +11,7 @@ TEST_CASE("edit distance 0", "[core][util][edit_distance]") // Distance 0 REQUIRE(hello.matches("hello")); - REQUIRE(hello.get_edit_distance("hello").value() == 0); + REQUIRE(*hello.get_edit_distance("hello") == 0); // Distance 1 REQUIRE_FALSE(hello.matches("hallo")); @@ -39,17 +39,17 @@ TEST_CASE("edit distance 1", "[core][util][edit_distance]") // Distance 0 REQUIRE(hello.matches("hello")); - REQUIRE(hello.get_edit_distance("hello").value() == 0); + REQUIRE(*hello.get_edit_distance("hello") == 0); // Distance 1 REQUIRE(hello.matches("hallo")); - REQUIRE(hello.get_edit_distance("hallo").value() == 1); + REQUIRE(*hello.get_edit_distance("hallo") == 1); REQUIRE(hello.matches("hell")); - REQUIRE(hello.get_edit_distance("hell").value() == 1); + REQUIRE(*hello.get_edit_distance("hell") == 1); REQUIRE(hello.matches("helloo")); - REQUIRE(hello.get_edit_distance("helloo").value() == 1); + REQUIRE(*hello.get_edit_distance("helloo") == 1); REQUIRE(hello.matches("chello")); - REQUIRE(hello.get_edit_distance("chello").value() == 1); + REQUIRE(*hello.get_edit_distance("chello") == 1); // Distance 2 REQUIRE_FALSE(hello.matches("helol")); @@ -71,25 +71,25 @@ TEST_CASE("edit distance 2", "[core][util][edit_distance]") // Distance 0 REQUIRE(hello.matches("hello")); - REQUIRE(hello.get_edit_distance("hello").value() == 0); + REQUIRE(*hello.get_edit_distance("hello") == 0); // Distance 1 REQUIRE(hello.matches("hallo")); - REQUIRE(hello.get_edit_distance("hallo").value() == 1); + REQUIRE(*hello.get_edit_distance("hallo") == 1); REQUIRE(hello.matches("hell")); - REQUIRE(hello.get_edit_distance("hell").value() == 1); + REQUIRE(*hello.get_edit_distance("hell") == 1); REQUIRE(hello.matches("helloo")); - REQUIRE(hello.get_edit_distance("helloo").value() == 1); + REQUIRE(*hello.get_edit_distance("helloo") == 1); REQUIRE(hello.matches("chello")); - REQUIRE(hello.get_edit_distance("chello").value() == 1); + REQUIRE(*hello.get_edit_distance("chello") == 1); // Distance 2 REQUIRE(hello.matches("helol")); - REQUIRE(hello.get_edit_distance("helol").value() == 2); + REQUIRE(*hello.get_edit_distance("helol") == 2); REQUIRE(hello.matches("help")); - REQUIRE(hello.get_edit_distance("help").value() == 2); + REQUIRE(*hello.get_edit_distance("help") == 2); REQUIRE(hello.matches("yohello")); - REQUIRE(hello.get_edit_distance("yohello").value() == 2); + REQUIRE(*hello.get_edit_distance("yohello") == 2); // Distance 3 REQUIRE_FALSE(hello.matches("kelp")); @@ -106,33 +106,33 @@ TEST_CASE("edit distance 3", "[core][util][edit_distance]") // Distance 0 REQUIRE(hello.matches("hello")); - REQUIRE(hello.get_edit_distance("hello").value() == 0); + REQUIRE(*hello.get_edit_distance("hello") == 0); // Distance 1 REQUIRE(hello.matches("hallo")); - REQUIRE(hello.get_edit_distance("hallo").value() == 1); + REQUIRE(*hello.get_edit_distance("hallo") == 1); REQUIRE(hello.matches("hell")); - REQUIRE(hello.get_edit_distance("hell").value() == 1); + REQUIRE(*hello.get_edit_distance("hell") == 1); REQUIRE(hello.matches("helloo")); - REQUIRE(hello.get_edit_distance("helloo").value() == 1); + REQUIRE(*hello.get_edit_distance("helloo") == 1); REQUIRE(hello.matches("chello")); - REQUIRE(hello.get_edit_distance("chello").value() == 1); + REQUIRE(*hello.get_edit_distance("chello") == 1); // Distance 2 REQUIRE(hello.matches("helol")); - REQUIRE(hello.get_edit_distance("helol").value() == 2); + REQUIRE(*hello.get_edit_distance("helol") == 2); REQUIRE(hello.matches("help")); - REQUIRE(hello.get_edit_distance("help").value() == 2); + REQUIRE(*hello.get_edit_distance("help") == 2); REQUIRE(hello.matches("yohello")); - REQUIRE(hello.get_edit_distance("yohello").value() == 2); + REQUIRE(*hello.get_edit_distance("yohello") == 2); // Distance 3 REQUIRE(hello.matches("kelp")); - REQUIRE(hello.get_edit_distance("kelp").value() == 3); + REQUIRE(*hello.get_edit_distance("kelp") == 3); REQUIRE(hello.matches("hilt")); - REQUIRE(hello.get_edit_distance("hilt").value() == 3); + REQUIRE(*hello.get_edit_distance("hilt") == 3); REQUIRE(hello.matches("wallow")); - REQUIRE(hello.get_edit_distance("wallow").value() == 3); + REQUIRE(*hello.get_edit_distance("wallow") == 3); // Distance > 3 REQUIRE_FALSE(hello.matches("unrelated")); diff --git a/unit/util/interval/eval.cpp b/unit/util/interval/eval.cpp index a2e0041e947..6c21764b44e 100644 --- a/unit/util/interval/eval.cpp +++ b/unit/util/interval/eval.cpp @@ -55,7 +55,7 @@ SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]") auto negated_val = numeric_cast(five.eval(ID_unary_minus).get_lower()); REQUIRE(negated_val.has_value()); - REQUIRE(negated_val.value() == -5); + REQUIRE(*negated_val == -5); // TODO: unary minus does not work on intervals that contain extremes // ADA-535 @@ -68,7 +68,7 @@ SCENARIO("Unary eval on intervals", "[core][analyses][interval][eval]") auto bitwise_negated_val = numeric_cast(five.eval(ID_bitnot).get_lower()); REQUIRE(bitwise_negated_val.has_value()); - REQUIRE(bitwise_negated_val.value() == (~5)); + REQUIRE(*bitwise_negated_val == (~5)); } } WHEN("Unary operations to an single element interval") diff --git a/unit/util/interval/subtract.cpp b/unit/util/interval/subtract.cpp index acb13c1d149..94395503338 100644 --- a/unit/util/interval/subtract.cpp +++ b/unit/util/interval/subtract.cpp @@ -113,7 +113,7 @@ SCENARIO( REQUIRE(result.is_single_value_interval()); auto maybe_lower = numeric_cast(result.get_lower()); REQUIRE(maybe_lower.has_value()); - REQUIRE(maybe_lower.value() == 7); + REQUIRE(*maybe_lower == 7); } } @@ -128,7 +128,7 @@ SCENARIO( REQUIRE(result.is_single_value_interval()); auto maybe_lower = numeric_cast(result.get_lower()); REQUIRE(maybe_lower.has_value()); - REQUIRE(maybe_lower.value() == 10); + REQUIRE(*maybe_lower == 10); } } @@ -141,10 +141,10 @@ SCENARIO( auto result = constant_interval_exprt::minus(lhs, rhs); auto maybe_lower = numeric_cast(result.get_lower()); REQUIRE(maybe_lower.has_value()); - REQUIRE(maybe_lower.value() == 9); + REQUIRE(*maybe_lower == 9); auto maybe_upper = numeric_cast(result.get_upper()); REQUIRE(maybe_upper.has_value()); - REQUIRE(maybe_upper.value() == 10); + REQUIRE(*maybe_upper == 10); } } } diff --git a/unit/util/interval_union.cpp b/unit/util/interval_union.cpp index b7f0148bda6..81ca158299b 100644 --- a/unit/util/interval_union.cpp +++ b/unit/util/interval_union.cpp @@ -35,7 +35,7 @@ TEST_CASE("interval_union", "[core][test-gen-util][interval_union]") REQUIRE_FALSE(first.is_empty()); REQUIRE(first.maximum().has_value()); - REQUIRE(first.maximum().value() == 10); + REQUIRE(*first.maximum() == 10); REQUIRE_FALSE(first.minimum().has_value()); REQUIRE_FALSE(second.is_empty()); @@ -45,7 +45,7 @@ TEST_CASE("interval_union", "[core][test-gen-util][interval_union]") REQUIRE_FALSE(third.is_empty()); REQUIRE_FALSE(third.maximum().has_value()); REQUIRE(third.minimum().has_value()); - REQUIRE(third.minimum().value() == 12); + REQUIRE(*third.minimum() == 12); REQUIRE(first.make_union(second).to_string() == "[:-10][-8:2][4:]"); REQUIRE(first.make_intersection(second).to_string() == "[:-15][5:5][8:10]"); diff --git a/unit/util/optional_utils.cpp b/unit/util/optional_utils.cpp index cbe306fbe9f..81bf7f8dc90 100644 --- a/unit/util/optional_utils.cpp +++ b/unit/util/optional_utils.cpp @@ -23,10 +23,10 @@ void do_optional_lookup_test(map_like_collectiont &map) map.insert({"pwd", "/home"}); auto const hello_result = optional_lookup(map, "hello"); REQUIRE(hello_result.has_value()); - REQUIRE(hello_result.value() == "world"); + REQUIRE(*hello_result == "world"); auto const pwd_result = optional_lookup(map, "pwd"); REQUIRE(pwd_result.has_value()); - REQUIRE(pwd_result.value() == "/home"); + REQUIRE(*pwd_result == "/home"); REQUIRE_FALSE(optional_lookup(map, "does not exit").has_value()); } } // namespace diff --git a/unit/util/pointer_offset_size.cpp b/unit/util/pointer_offset_size.cpp index a091f1c7f42..004021afd1f 100644 --- a/unit/util/pointer_offset_size.cpp +++ b/unit/util/pointer_offset_size.cpp @@ -35,34 +35,34 @@ TEST_CASE("Build subexpression to access element at offset into array") { const auto result = get_subexpression_at_offset(a, 0, t, ns); - REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type()))); + REQUIRE(*result == index_exprt(a, from_integer(0, c_index_type()))); } { const auto result = get_subexpression_at_offset(a, 32 / 8, t, ns); - REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type()))); + REQUIRE(*result == index_exprt(a, from_integer(1, c_index_type()))); } { const auto result = get_subexpression_at_offset(a, from_integer(0, size_type()), t, ns); - REQUIRE(result.value() == index_exprt(a, from_integer(0, c_index_type()))); + REQUIRE(*result == index_exprt(a, from_integer(0, c_index_type()))); } { const auto result = - get_subexpression_at_offset(a, size_of_expr(t, ns).value(), t, ns); - REQUIRE(result.value() == index_exprt(a, from_integer(1, c_index_type()))); + get_subexpression_at_offset(a, *size_of_expr(t, ns), t, ns); + REQUIRE(*result == index_exprt(a, from_integer(1, c_index_type()))); } { const signedbv_typet small_t(8); const auto result = get_subexpression_at_offset(a, 1, small_t, ns); REQUIRE( - result.value() == make_byte_extract( - index_exprt(a, from_integer(0, c_index_type())), - from_integer(1, c_index_type()), - small_t)); + *result == make_byte_extract( + index_exprt(a, from_integer(0, c_index_type())), + from_integer(1, c_index_type()), + small_t)); } { @@ -72,7 +72,7 @@ TEST_CASE("Build subexpression to access element at offset into array") // not enough to fill a 16 bit int, so this cannot be transformed in an // index_exprt. REQUIRE( - result.value() == + *result == make_byte_extract(a, from_integer(3, c_index_type()), int16_t)); } } @@ -95,31 +95,31 @@ TEST_CASE("Build subexpression to access element at offset into struct") { const auto result = get_subexpression_at_offset(s, 0, t, ns); - REQUIRE(result.value() == member_exprt(s, "foo", t)); + REQUIRE(*result == member_exprt(s, "foo", t)); } { const auto result = get_subexpression_at_offset(s, 32 / 8, t, ns); - REQUIRE(result.value() == member_exprt(s, "bar", t)); + REQUIRE(*result == member_exprt(s, "bar", t)); } { const auto result = get_subexpression_at_offset(s, from_integer(0, size_type()), t, ns); - REQUIRE(result.value() == member_exprt(s, "foo", t)); + REQUIRE(*result == member_exprt(s, "foo", t)); } { const auto result = - get_subexpression_at_offset(s, size_of_expr(t, ns).value(), t, ns); - REQUIRE(result.value() == member_exprt(s, "bar", t)); + get_subexpression_at_offset(s, *size_of_expr(t, ns), t, ns); + REQUIRE(*result == member_exprt(s, "bar", t)); } { const signedbv_typet small_t(8); const auto result = get_subexpression_at_offset(s, 1, small_t, ns); REQUIRE( - result.value() == + *result == make_byte_extract( member_exprt(s, "foo", t), from_integer(1, c_index_type()), small_t)); }