Skip to content

Commit 6e96333

Browse files
author
Matthias Güdemann
committed
Change from optional set to simply set
1 parent d2bc012 commit 6e96333

File tree

3 files changed

+4
-6
lines changed

3 files changed

+4
-6
lines changed

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -327,7 +327,7 @@ exprt::operandst java_build_arguments(
327327
const auto alternatives =
328328
pointer_type_selector.get_parameter_alternative_types(
329329
function.name, p.get_identifier(), ns);
330-
if(!alternatives.has_value())
330+
if(alternatives.empty())
331331
{
332332
main_arguments[param_number] = object_factory(
333333
p.type(),
@@ -344,7 +344,6 @@ exprt::operandst java_build_arguments(
344344
INVARIANT(!is_this, "We cannot have different types for `this` here");
345345
// create a non-deterministic switch between all possible values for the
346346
// type of the parameter.
347-
const auto alternative_object_types = alternatives.value();
348347
code_switcht code_switch;
349348

350349
// the idea is to get a new symbol for the parameter value `tmp`
@@ -374,7 +373,7 @@ exprt::operandst java_build_arguments(
374373

375374
std::vector<codet> cases;
376375
size_t alternative = 0;
377-
for(const auto &type : alternative_object_types)
376+
for(const auto &type : alternatives)
378377
{
379378
code_blockt init_code_for_type;
380379
exprt init_expr_for_parameter = object_factory(

jbmc/src/java_bytecode/select_pointer_type.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -224,8 +224,7 @@ select_pointer_typet::get_recursively_instantiated_type(
224224
return inst_val;
225225
}
226226

227-
optionalt<std::set<symbol_typet>>
228-
select_pointer_typet::get_parameter_alternative_types(
227+
std::set<symbol_typet> select_pointer_typet::get_parameter_alternative_types(
229228
const irep_idt &function_name,
230229
const irep_idt &parameter_name,
231230
const namespacet &ns) const

jbmc/src/java_bytecode/select_pointer_type.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ class select_pointer_typet
4242
&generic_parameter_specialization_map,
4343
const namespacet &ns) const;
4444

45-
virtual optionalt<std::set<symbol_typet>> get_parameter_alternative_types(
45+
virtual std::set<symbol_typet> get_parameter_alternative_types(
4646
const irep_idt &function_name,
4747
const irep_idt &parameter_name,
4848
const namespacet &ns) const;

0 commit comments

Comments
 (0)