Skip to content

Commit

Permalink
Use the two-param code_typet constructor
Browse files Browse the repository at this point in the history
  • Loading branch information
@peterschrammel
peterschrammel committed Jun 5, 2018
1 parent 103c7b7 commit 05a5efb
Show file tree
Hide file tree
Showing 17 changed files with 82 additions and 111 deletions.
5 changes: 1 addition & 4 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -760,15 +760,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)

const irep_idt clone_name=
id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
code_typet clone_type;
clone_type.return_type()=
java_reference_type(symbol_typet("java::java.lang.Object"));
code_typet::parametert this_param;
this_param.set_identifier(id2string(clone_name)+"::this");
this_param.set_base_name("this");
this_param.set_this();
this_param.type()=java_reference_type(symbol_type);
clone_type.parameters().push_back(this_param);
code_typet clone_type({this_param}, java_lang_object_type());

parameter_symbolt this_symbol;
this_symbol.name=this_param.get_identifier();
Expand Down
6 changes: 2 additions & 4 deletions jbmc/src/java_bytecode/java_entry_point.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
initialize.base_name=INITIALIZE_FUNCTION;
initialize.mode=ID_java;

code_typet type;
type.return_type()=empty_typet();
code_typet type({}, empty_typet());
initialize.type=type;

code_blockt init_code;
Expand Down Expand Up @@ -688,8 +687,7 @@ bool generate_java_start_function(
// we just built and register it in the symbol table
symbolt new_symbol;

code_typet main_type;
main_type.return_type()=empty_typet();
code_typet main_type({}, empty_typet());

new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
Expand Down
6 changes: 2 additions & 4 deletions jbmc/src/java_bytecode/java_static_initializers.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -293,8 +293,7 @@ static void create_clinit_wrapper_symbols(

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

code_typet thunk_type;
thunk_type.return_type() = void_typet();
code_typet thunk_type({}, void_typet());

symbolt static_init_symbol;
static_init_symbol.name = static_init_name;
Expand Down
4 changes: 1 addition & 3 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1611,9 +1611,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
fun_call.lhs()=class1;
fun_call.arguments().push_back(string1);
code_typet fun_type;
fun_type.parameters().push_back(code_typet::parametert(string_ptr_type));
fun_type.return_type()=class_type;
code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
fun_call.function().type()=fun_type;
code.add(fun_call, loc);

Expand Down
13 changes: 5 additions & 8 deletions jbmc/src/java_bytecode/java_types.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -493,24 +493,21 @@ typet java_type_from_string(
if(e_pos==std::string::npos)
return nil_typet();

code_typet result;

result.return_type()=
java_type_from_string(
std::string(src, e_pos+1, std::string::npos),
class_name_prefix);
typet return_type = java_type_from_string(
std::string(src, e_pos + 1, std::string::npos), class_name_prefix);

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

// create parameters for each type
code_typet::parameterst parameters;
std::transform(
param_types.begin(),
param_types.end(),
std::back_inserter(result.parameters()),
std::back_inserter(parameters),
[](const typet &type) { return code_typet::parametert(type); });

return result;
return code_typet(std::move(parameters), std::move(return_type));
}

case '[': // array type
Expand Down
7 changes: 6 additions & 1 deletion jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,12 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
const symbol_exprt lhs("lhs", unsignedbv_typet(32));
const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
code_typet fun_type;
code_typet fun_type(
{code_typet::parametert(length_type()),
code_typet::parametert(pointer_type(java_char_type())),
code_typet::parametert(string_type),
code_typet::parametert(string_type)},
unsignedbv_typet(32));

// fun1 is s3 = s1.concat(s2)
function_application_exprt fun1(fun_type);
Expand Down
3 changes: 1 addition & 2 deletions src/ansi-c/ansi_c_entry_point.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -445,8 +445,7 @@ bool generate_ansi_c_start_function(
// add the entry point symbol
symbolt new_symbol;

code_typet main_type;
main_type.return_type()=empty_typet();
code_typet main_type({}, empty_typet());

new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
Expand Down
6 changes: 2 additions & 4 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -450,10 +450,8 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
typet arg_type=expr.type();
typecheck_type(arg_type);

code_typet new_type;
new_type.return_type().swap(arg_type);
new_type.parameters().resize(1);
new_type.parameters()[0].type()=pointer_type(void_type());
code_typet new_type(
{code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));

assert(expr.operands().size()==1);
exprt arg=expr.op0();
Expand Down
86 changes: 40 additions & 46 deletions src/cpp/cpp_typecheck_expr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1446,10 +1446,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
code_typet t(
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
t.make_ellipsis();
t.return_type()=ptr_arg.type().subtype();
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1480,10 +1479,10 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=ptr_arg.type().subtype();
code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(signed_int_type())},
ptr_arg.type().subtype());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1514,12 +1513,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(
code_typet::parametert(ptr_arg.type().subtype()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=empty_typet();
code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type().subtype()),
code_typet::parametert(signed_int_type())},
empty_typet());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1550,12 +1548,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(
code_typet::parametert(ptr_arg.type().subtype()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=ptr_arg.type().subtype();
code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type().subtype()),
code_typet::parametert(signed_int_type())},
ptr_arg.type().subtype());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1594,11 +1591,11 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=empty_typet();
code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
code_typet::parametert(signed_int_type())},
empty_typet());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1643,12 +1640,12 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=empty_typet();
code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
code_typet::parametert(signed_int_type())},
empty_typet());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1698,20 +1695,19 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
code_typet::parameterst parameters;
parameters.push_back(code_typet::parametert(ptr_arg.type()));
parameters.push_back(code_typet::parametert(ptr_arg.type()));

if(identifier=="__atomic_compare_exchange")
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
parameters.push_back(code_typet::parametert(ptr_arg.type()));
else
t.parameters().push_back(
code_typet::parametert(ptr_arg.type().subtype()));
parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));

t.parameters().push_back(code_typet::parametert(c_bool_type()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.parameters().push_back(code_typet::parametert(signed_int_type()));
t.return_type()=c_bool_type();
parameters.push_back(code_typet::parametert(c_bool_type()));
parameters.push_back(code_typet::parametert(signed_int_type()));
parameters.push_back(code_typet::parametert(signed_int_type()));
code_typet t(std::move(parameters), c_bool_type());
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1744,10 +1740,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
code_typet t(
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
t.make_ellipsis();
t.return_type()=ptr_arg.type().subtype();
result.type()=t;
expr.swap(result);
return;
Expand Down Expand Up @@ -1780,10 +1775,9 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t;
t.parameters().push_back(code_typet::parametert(ptr_arg.type()));
code_typet t(
{code_typet::parametert(ptr_arg.type())}, ptr_arg.type().subtype());
t.make_ellipsis();
t.return_type()=ptr_arg.type().subtype();
result.type()=t;
expr.swap(result);
return;
Expand Down
13 changes: 3 additions & 10 deletions src/cpp/cpp_typecheck_resolve.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -611,29 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(

// 1. no arguments, default initialization
{
code_typet t1;
t1.return_type()=it->type();
code_typet t1({}, it->type());
exprt pod_constructor1("pod_constructor", t1);
new_identifiers.push_back(pod_constructor1);
}

// 2. one argument, copy/conversion
{
code_typet t2;
t2.return_type()=it->type();
t2.parameters().resize(1);
t2.parameters()[0].type()=it->type();
code_typet t2({code_typet::parametert(it->type())}, it->type());
exprt pod_constructor2("pod_constructor", t2);
new_identifiers.push_back(pod_constructor2);
}

// enums, in addition, can also be constructed from int
if(symbol_type.id()==ID_c_enum_tag)
{
code_typet t3;
t3.return_type()=it->type();
t3.parameters().resize(1);
t3.parameters()[0].type()=signed_int_type();
code_typet t3({code_typet::parametert(signed_int_type())}, it->type());
exprt pod_constructor3("pod_constructor", t3);
new_identifiers.push_back(pod_constructor3);
}
Expand Down
6 changes: 2 additions & 4 deletions src/goto-cc/linker_script_merge.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -593,8 +593,7 @@ int linker_script_merget::ls_data2instructions(
for(const auto &d : data["regions"].array)
{
code_function_callt f;
code_typet void_t;
void_t.return_type()=empty_typet();
code_typet void_t({}, empty_typet());
f.function()=symbol_exprt(CPROVER_PREFIX "allocated_memory", void_t);
unsigned start=safe_string2unsigned(d["start"].value);
unsigned size=safe_string2unsigned(d["size"].value);
Expand All @@ -620,8 +619,7 @@ int linker_script_merget::ls_data2instructions(
sym.name=CPROVER_PREFIX "allocated_memory";
sym.pretty_name=CPROVER_PREFIX "allocated_memory";
sym.is_lvalue=sym.is_static_lifetime=true;
code_typet void_t;
void_t.return_type()=empty_typet();
code_typet void_t({}, empty_typet());
sym.type=void_t;
symbol_table.add(sym);
}
Expand Down
Loading

0 comments on commit 05a5efb

Please sign in to comment.