Skip to content

Commit 9ba2012

Browse files
committed
fixup! fixup! Do not use optionalt::value()
1 parent dd8a0fd commit 9ba2012

File tree

6 files changed

+11
-11
lines changed

6 files changed

+11
-11
lines changed

src/goto-cc/gcc_message_handler.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -69,9 +69,9 @@ void gcc_message_handlert::print(
6969
if(file_name.has_value() && !line.empty())
7070
{
7171
#ifdef _MSC_VER
72-
std::ifstream in(widen(file_name.value()));
72+
std::ifstream in(widen(*file_name));
7373
#else
74-
std::ifstream in(file_name.value());
74+
std::ifstream in(*file_name);
7575
#endif
7676
if(in)
7777
{

src/goto-harness/goto_harness_generator.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ std::size_t require_one_size_value(
4646
auto value = string2optional<std::size_t>(string_value, 10);
4747
if(value.has_value())
4848
{
49-
return value.value();
49+
return *value;
5050
}
5151
else
5252
{

src/goto-harness/goto_harness_parse_options.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ int goto_harness_parse_optionst::doit()
118118
throw deserialization_exceptiont{"failed to read goto program from file '" +
119119
got_harness_config.in_file + "'"};
120120
}
121-
auto goto_model = std::move(read_goto_binary_result.value());
121+
auto goto_model = std::move(*read_goto_binary_result);
122122
auto const goto_model_without_harness_symbols =
123123
get_symbol_names_from_goto_model(goto_model);
124124

src/goto-harness/recursive_initialization.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ bool recursive_initialization_configt::handle_option(
3939
string2optional<std::size_t>(value, 10);
4040
if(user_min_null_tree_depth.has_value())
4141
{
42-
min_null_tree_depth = user_min_null_tree_depth.value();
42+
min_null_tree_depth = *user_min_null_tree_depth;
4343
}
4444
else
4545
{
@@ -57,7 +57,7 @@ bool recursive_initialization_configt::handle_option(
5757
string2optional<std::size_t>(value, 10);
5858
if(user_max_nondet_tree_depth.has_value())
5959
{
60-
max_nondet_tree_depth = user_max_nondet_tree_depth.value();
60+
max_nondet_tree_depth = *user_max_nondet_tree_depth;
6161
}
6262
else
6363
{
@@ -203,7 +203,7 @@ void recursive_initializationt::initialize(
203203
if(size_var.has_value())
204204
{
205205
const symbol_exprt &size_symbol =
206-
goto_model.symbol_table.lookup_ref(size_var.value()).symbol_expr();
206+
goto_model.symbol_table.lookup_ref(*size_var).symbol_expr();
207207
body.add(code_function_callt{
208208
fun_symbol.symbol_expr(),
209209
{depth, address_of_exprt{lhs}, address_of_exprt{size_symbol}}});
@@ -304,7 +304,7 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr)
304304
{
305305
expr_name = to_symbol_expr(expr).get_identifier();
306306
is_nullable = initialization_config.potential_null_function_pointers.count(
307-
expr_name.value());
307+
*expr_name);
308308
if(should_be_treated_as_array(*expr_name))
309309
{
310310
size_var = get_associated_size_variable(*expr_name);

src/solvers/flattening/boolbv_quantifier.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -195,8 +195,8 @@ static optionalt<exprt> eager_quantifier_instantiation(
195195
if(!min_i.has_value() || !max_i.has_value())
196196
return {};
197197

198-
mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
199-
mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
198+
mp_integer lb = numeric_cast_v<mp_integer>(*min_i);
199+
mp_integer ub = numeric_cast_v<mp_integer>(*max_i);
200200

201201
if(lb > ub)
202202
return {};

src/solvers/flattening/pointer_logic.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ exprt pointer_logict::pointer_expr(
116116
auto deep_object_opt =
117117
get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
118118
CHECK_RETURN(deep_object_opt.has_value());
119-
exprt deep_object = deep_object_opt.value();
119+
exprt deep_object = *deep_object_opt;
120120
simplify(deep_object, ns);
121121
if(
122122
deep_object.id() != ID_byte_extract_little_endian &&

0 commit comments

Comments
 (0)