Skip to content

Commit d0b503f

Browse files
peterschrammelpeterschrammel
committed
Use the two-param code_typet constructor
1 parent 7d3921c commit d0b503f

18 files changed

+88
-123
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -760,15 +760,14 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
760760

761761
const irep_idt clone_name=
762762
id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
763-
code_typet clone_type;
764-
clone_type.return_type()=
765-
java_reference_type(symbol_typet("java::java.lang.Object"));
766763
code_typet::parametert this_param;
767764
this_param.set_identifier(id2string(clone_name)+"::this");
768765
this_param.set_base_name("this");
769766
this_param.set_this();
770767
this_param.type()=java_reference_type(symbol_type);
771-
clone_type.parameters().push_back(this_param);
768+
code_typet clone_type(
769+
{this_param},
770+
java_reference_type(symbol_typet("java::java.lang.Object")));
772771

773772
parameter_symbolt this_symbol;
774773
this_symbol.name=this_param.get_identifier();

‎jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
3131
initialize.base_name=INITIALIZE_FUNCTION;
3232
initialize.mode=ID_java;
3333

34-
code_typet type;
35-
type.return_type()=empty_typet();
34+
code_typet type({}, empty_typet());
3635
initialize.type=type;
3736

3837
code_blockt init_code;
@@ -688,8 +687,7 @@ bool generate_java_start_function(
688687
// we just built and register it in the symbol table
689688
symbolt new_symbol;
690689

691-
code_typet main_type;
692-
main_type.return_type()=empty_typet();
690+
code_typet main_type({}, empty_typet());
693691

694692
new_symbol.name=goto_functionst::entry_point();
695693
new_symbol.type.swap(main_type);

‎jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -293,8 +293,7 @@ static void create_clinit_wrapper_symbols(
293293

294294
// Create symbol for the "clinit_wrapper"
295295
symbolt wrapper_method_symbol;
296-
code_typet wrapper_method_type;
297-
wrapper_method_type.return_type() = void_typet();
296+
code_typet wrapper_method_type({}, void_typet());
298297
wrapper_method_symbol.name = clinit_wrapper_name(class_name);
299298
wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
300299
wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -714,8 +713,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
714713
"a class cannot be both incomplete, and so have stub static fields, and "
715714
"also define a static initializer");
716715

717-
code_typet thunk_type;
718-
thunk_type.return_type() = void_typet();
716+
code_typet thunk_type({}, void_typet());
719717

720718
symbolt static_init_symbol;
721719
static_init_symbol.name = static_init_name;

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1611,9 +1611,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
16111611
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
16121612
fun_call.lhs()=class1;
16131613
fun_call.arguments().push_back(string1);
1614-
code_typet fun_type;
1615-
fun_type.parameters().push_back(code_typet::parametert(string_ptr_type));
1616-
fun_type.return_type()=class_type;
1614+
code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
16171615
fun_call.function().type()=fun_type;
16181616
code.add(fun_call, loc);
16191617

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -493,24 +493,21 @@ typet java_type_from_string(
493493
if(e_pos==std::string::npos)
494494
return nil_typet();
495495

496-
code_typet result;
497-
498-
result.return_type()=
499-
java_type_from_string(
500-
std::string(src, e_pos+1, std::string::npos),
501-
class_name_prefix);
496+
typet return_type = java_type_from_string(
497+
std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
502498

503499
std::vector<typet> param_types =
504500
parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
505501

506502
// create parameters for each type
503+
code_typet::parameterst parameters;
507504
std::transform(
508505
param_types.begin(),
509506
param_types.end(),
510-
std::back_inserter(result.parameters()),
507+
std::back_inserter(parameters),
511508
[](const typet &type) { return code_typet::parametert(type); });
512509

513-
return result;
510+
return code_typet(std::move(parameters), std::move(return_type));
514511
}
515512

516513
case '[': // array type

‎jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,9 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
5858
const symbol_exprt lhs("lhs", unsignedbv_typet(32));
5959
const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
6060
const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
61-
code_typet fun_type;
61+
code_typet fun_type(
62+
{length_type(), pointer_type(java_char_type()), string_type, string_type},
63+
unsignedbv_typet(32));
6264

6365
// fun1 is s3 = s1.concat(s2)
6466
function_application_exprt fun1(fun_type);

‎src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -445,8 +445,7 @@ bool generate_ansi_c_start_function(
445445
// add the entry point symbol
446446
symbolt new_symbol;
447447

448-
code_typet main_type;
449-
main_type.return_type()=empty_typet();
448+
code_typet main_type({}, empty_typet());
450449

451450
new_symbol.name=goto_functionst::entry_point();
452451
new_symbol.type.swap(main_type);

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -450,10 +450,8 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
450450
typet arg_type=expr.type();
451451
typecheck_type(arg_type);
452452

453-
code_typet new_type;
454-
new_type.return_type().swap(arg_type);
455-
new_type.parameters().resize(1);
456-
new_type.parameters()[0].type()=pointer_type(void_type());
453+
code_typet new_type(
454+
{code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
457455

458456
assert(expr.operands().size()==1);
459457
exprt arg=expr.op0();

‎src/cpp/cpp_typecheck_expr.cpp

Lines changed: 40 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -1446,10 +1446,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14461446
symbol_exprt result;
14471447
result.add_source_location()=source_location;
14481448
result.set_identifier(identifier);
1449-
code_typet t;
1450-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1449+
code_typet t(
1450+
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
14511451
t.make_ellipsis();
1452-
t.return_type()=ptr_arg.type().subtype();
14531452
result.type()=t;
14541453
expr.swap(result);
14551454
return;
@@ -1480,10 +1479,10 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
14801479
symbol_exprt result;
14811480
result.add_source_location()=source_location;
14821481
result.set_identifier(identifier);
1483-
code_typet t;
1484-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1485-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1486-
t.return_type()=ptr_arg.type().subtype();
1482+
code_typet t(
1483+
{code_typet::parametert(ptr_arg.type()),
1484+
code_typet::parametert(signed_int_type())},
1485+
ptr_arg.type().subtype());
14871486
result.type()=t;
14881487
expr.swap(result);
14891488
return;
@@ -1514,12 +1513,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15141513
symbol_exprt result;
15151514
result.add_source_location()=source_location;
15161515
result.set_identifier(identifier);
1517-
code_typet t;
1518-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1519-
t.parameters().push_back(
1520-
code_typet::parametert(ptr_arg.type().subtype()));
1521-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1522-
t.return_type()=empty_typet();
1516+
code_typet t(
1517+
{code_typet::parametert(ptr_arg.type()),
1518+
code_typet::parametert(ptr_arg.type().subtype()),
1519+
code_typet::parametert(signed_int_type())},
1520+
empty_typet());
15231521
result.type()=t;
15241522
expr.swap(result);
15251523
return;
@@ -1550,12 +1548,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15501548
symbol_exprt result;
15511549
result.add_source_location()=source_location;
15521550
result.set_identifier(identifier);
1553-
code_typet t;
1554-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1555-
t.parameters().push_back(
1556-
code_typet::parametert(ptr_arg.type().subtype()));
1557-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1558-
t.return_type()=ptr_arg.type().subtype();
1551+
code_typet t(
1552+
{code_typet::parametert(ptr_arg.type()),
1553+
code_typet::parametert(ptr_arg.type().subtype()),
1554+
code_typet::parametert(signed_int_type())},
1555+
ptr_arg.type().subtype());
15591556
result.type()=t;
15601557
expr.swap(result);
15611558
return;
@@ -1594,11 +1591,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
15941591
symbol_exprt result;
15951592
result.add_source_location()=source_location;
15961593
result.set_identifier(identifier);
1597-
code_typet t;
1598-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1599-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1600-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1601-
t.return_type()=empty_typet();
1594+
code_typet t(
1595+
{code_typet::parametert(ptr_arg.type()),
1596+
code_typet::parametert(ptr_arg.type()),
1597+
code_typet::parametert(signed_int_type())},
1598+
empty_typet());
16021599
result.type()=t;
16031600
expr.swap(result);
16041601
return;
@@ -1643,12 +1640,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
16431640
symbol_exprt result;
16441641
result.add_source_location()=source_location;
16451642
result.set_identifier(identifier);
1646-
code_typet t;
1647-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1648-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1649-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1650-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1651-
t.return_type()=empty_typet();
1643+
code_typet t(
1644+
{code_typet::parametert(ptr_arg.type()),
1645+
code_typet::parametert(ptr_arg.type()),
1646+
code_typet::parametert(ptr_arg.type()),
1647+
code_typet::parametert(signed_int_type())},
1648+
empty_typet());
16521649
result.type()=t;
16531650
expr.swap(result);
16541651
return;
@@ -1698,20 +1695,19 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
16981695
symbol_exprt result;
16991696
result.add_source_location()=source_location;
17001697
result.set_identifier(identifier);
1701-
code_typet t;
1702-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1703-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1698+
code_typet::parameterst parameters;
1699+
parameters.push_back(code_typet::parametert(ptr_arg.type()));
1700+
parameters.push_back(code_typet::parametert(ptr_arg.type()));
17041701

17051702
if(identifier=="__atomic_compare_exchange")
1706-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1703+
parameters.push_back(code_typet::parametert(ptr_arg.type()));
17071704
else
1708-
t.parameters().push_back(
1709-
code_typet::parametert(ptr_arg.type().subtype()));
1705+
parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));
17101706

1711-
t.parameters().push_back(code_typet::parametert(c_bool_type()));
1712-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1713-
t.parameters().push_back(code_typet::parametert(signed_int_type()));
1714-
t.return_type()=c_bool_type();
1707+
parameters.push_back(code_typet::parametert(c_bool_type()));
1708+
parameters.push_back(code_typet::parametert(signed_int_type()));
1709+
parameters.push_back(code_typet::parametert(signed_int_type()));
1710+
code_typet t(std::move(parameters), c_bool_type());
17151711
result.type()=t;
17161712
expr.swap(result);
17171713
return;
@@ -1744,10 +1740,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17441740
symbol_exprt result;
17451741
result.add_source_location()=source_location;
17461742
result.set_identifier(identifier);
1747-
code_typet t;
1748-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1743+
code_typet t(
1744+
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17491745
t.make_ellipsis();
1750-
t.return_type()=ptr_arg.type().subtype();
17511746
result.type()=t;
17521747
expr.swap(result);
17531748
return;
@@ -1780,10 +1775,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
17801775
symbol_exprt result;
17811776
result.add_source_location()=source_location;
17821777
result.set_identifier(identifier);
1783-
code_typet t;
1784-
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
1778+
code_typet t(
1779+
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
17851780
t.make_ellipsis();
1786-
t.return_type()=ptr_arg.type().subtype();
17871781
result.type()=t;
17881782
expr.swap(result);
17891783
return;

‎src/cpp/cpp_typecheck_resolve.cpp

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -611,29 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(
611611

612612
// 1. no arguments, default initialization
613613
{
614-
code_typet t1;
615-
t1.return_type()=it->type();
614+
code_typet t1({}, it->type());
616615
exprt pod_constructor1("pod_constructor", t1);
617616
new_identifiers.push_back(pod_constructor1);
618617
}
619618

620619
// 2. one argument, copy/conversion
621620
{
622-
code_typet t2;
623-
t2.return_type()=it->type();
624-
t2.parameters().resize(1);
625-
t2.parameters()[0].type()=it->type();
621+
code_typet t2({code_typet::parametert(it->type())}, it->type());
626622
exprt pod_constructor2("pod_constructor", t2);
627623
new_identifiers.push_back(pod_constructor2);
628624
}
629625

630626
// enums, in addition, can also be constructed from int
631627
if(symbol_type.id()==ID_c_enum_tag)
632628
{
633-
code_typet t3;
634-
t3.return_type()=it->type();
635-
t3.parameters().resize(1);
636-
t3.parameters()[0].type()=signed_int_type();
629+
code_typet t3({code_typet::parametert(it->type())}, signed_int_type());
637630
exprt pod_constructor3("pod_constructor", t3);
638631
new_identifiers.push_back(pod_constructor3);
639632
}

‎src/goto-cc/linker_script_merge.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -593,8 +593,7 @@ int linker_script_merget::ls_data2instructions(
593593
for(const auto &d : data["regions"].array)
594594
{
595595
code_function_callt f;
596-
code_typet void_t;
597-
void_t.return_type()=empty_typet();
596+
code_typet void_t({}, empty_typet());
598597
f.function()=symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t);
599598
unsigned start=safe_string2unsigned(d["start"].value);
600599
unsigned size=safe_string2unsigned(d["size"].value);
@@ -620,8 +619,7 @@ int linker_script_merget::ls_data2instructions(
620619
sym.name=CPROVER_PREFIX "allocated_memory";
621620
sym.pretty_name=CPROVER_PREFIX "allocated_memory";
622621
sym.is_lvalue=sym.is_static_lifetime=true;
623-
code_typet void_t;
624-
void_t.return_type()=empty_typet();
622+
code_typet void_t({}, empty_typet());
625623
sym.type=void_t;
626624
symbol_table.add(sym);
627625
}

0 commit comments

Comments
 (0)