Skip to content

Commit

Permalink
Make code_typet declarations const
Browse files Browse the repository at this point in the history
  • Loading branch information
peterschrammel committed Jun 6, 2018
1 parent b618d94 commit 64cd733
Show file tree
Hide file tree
Showing 14 changed files with 26 additions and 36 deletions.
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -765,7 +765,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
this_param.set_base_name("this");
this_param.set_this();
this_param.type()=java_reference_type(symbol_type);
code_typet clone_type({this_param}, java_lang_object_type());
const code_typet clone_type({this_param}, java_lang_object_type());

parameter_symbolt this_symbol;
this_symbol.name=this_param.get_identifier();
Expand Down
7 changes: 2 additions & 5 deletions jbmc/src/java_bytecode/java_entry_point.cpp
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({}, empty_typet());
initialize.type=type;
initialize.type = code_typet({}, empty_typet());

code_blockt init_code;

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

code_typet main_type({}, empty_typet());

new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
new_symbol.type = code_typet({}, empty_typet());
new_symbol.value.swap(init_code);
new_symbol.mode=ID_java;

Expand Down
4 changes: 2 additions & 2 deletions jbmc/src/java_bytecode/java_static_initializers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -293,7 +293,7 @@ static void create_clinit_wrapper_symbols(

// Create symbol for the "clinit_wrapper"
symbolt wrapper_method_symbol;
code_typet wrapper_method_type({}, void_typet());
const 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 @@ -713,7 +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({}, void_typet());
const code_typet thunk_type({}, void_typet());

symbolt static_init_symbol;
static_init_symbol.name = static_init_name;
Expand Down
2 changes: 1 addition & 1 deletion jbmc/src/java_bytecode/java_string_library_preprocess.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1611,7 +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({code_typet::parametert(string_ptr_type)}, class_type);
const 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
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ 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(
const code_typet fun_type(
{code_typet::parametert(length_type()),
code_typet::parametert(pointer_type(java_char_type())),
code_typet::parametert(string_type),
Expand Down
4 changes: 1 addition & 3 deletions src/ansi-c/ansi_c_entry_point.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -445,10 +445,8 @@ bool generate_ansi_c_start_function(
// add the entry point symbol
symbolt new_symbol;

code_typet main_type({}, empty_typet());

new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
new_symbol.type = code_typet({}, empty_typet());
new_symbol.value.swap(init_code);
new_symbol.mode=symbol.mode;

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/c_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
typet arg_type=expr.type();
typecheck_type(arg_type);

code_typet new_type(
const code_typet new_type(
{code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));

assert(expr.operands().size()==1);
Expand Down
10 changes: 5 additions & 5 deletions src/cpp/cpp_typecheck_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1479,7 +1479,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t(
const code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(signed_int_type())},
ptr_arg.type().subtype());
Expand Down Expand Up @@ -1513,7 +1513,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t(
const code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type().subtype()),
code_typet::parametert(signed_int_type())},
Expand Down Expand Up @@ -1548,7 +1548,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t(
const code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type().subtype()),
code_typet::parametert(signed_int_type())},
Expand Down Expand Up @@ -1591,7 +1591,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t(
const code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
code_typet::parametert(signed_int_type())},
Expand Down Expand Up @@ -1640,7 +1640,7 @@ void cpp_typecheckt::typecheck_expr_cpp_name(
symbol_exprt result;
result.add_source_location()=source_location;
result.set_identifier(identifier);
code_typet t(
const code_typet t(
{code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
code_typet::parametert(ptr_arg.type()),
Expand Down
6 changes: 3 additions & 3 deletions src/cpp/cpp_typecheck_resolve.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -611,22 +611,22 @@ void cpp_typecheck_resolvet::make_constructors(

// 1. no arguments, default initialization
{
code_typet t1({}, it->type());
const 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({code_typet::parametert(it->type())}, it->type());
const 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({code_typet::parametert(signed_int_type())}, it->type());
const 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
4 changes: 2 additions & 2 deletions src/goto-cc/linker_script_merge.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -593,7 +593,7 @@ int linker_script_merget::ls_data2instructions(
for(const auto &d : data["regions"].array)
{
code_function_callt f;
code_typet void_t({}, empty_typet());
const 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 @@ -619,7 +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({}, empty_typet());
const code_typet void_t({}, empty_typet());
sym.type=void_t;
symbol_table.add(sym);
}
Expand Down
6 changes: 2 additions & 4 deletions src/goto-instrument/goto_program2code.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction(
case ATOMIC_END:
{
code_function_callt f;
code_typet void_t({}, empty_typet());
const code_typet void_t({}, empty_typet());
f.function()=symbol_exprt(
target->is_atomic_begin() ?
"__CPROVER_atomic_begin" :
Expand Down Expand Up @@ -1948,12 +1948,10 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
base_name="nondet_"+std::to_string(count);
}

code_typet code_type({}, expr.type());

symbolt symbol;
symbol.base_name=base_name;
symbol.name=base_name;
symbol.type=code_type;
symbol.type = code_typet({}, expr.type());
id=symbol.name;

symbol_table.insert(std::move(symbol));
Expand Down
7 changes: 2 additions & 5 deletions src/jsil/jsil_entry_point.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,7 @@ static void create_initialize(symbol_tablet &symbol_table)
initialize.base_name = INITIALIZE_FUNCTION;
initialize.mode="jsil";

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

code_blockt init_code;

Expand Down Expand Up @@ -151,10 +150,8 @@ bool jsil_entry_point(
// add "main"
symbolt new_symbol;

code_typet main_type({}, empty_typet());

new_symbol.name=goto_functionst::entry_point();
new_symbol.type.swap(main_type);
new_symbol.type = code_typet({}, empty_typet());
new_symbol.value.swap(init_code);

if(!symbol_table.insert(std::move(new_symbol)).second)
Expand Down
2 changes: 1 addition & 1 deletion unit/analyses/call_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ static symbolt create_void_function_symbol(
const irep_idt &name,
const codet &code)
{
code_typet void_function_type({}, empty_typet());
const code_typet void_function_type({}, empty_typet());
symbolt function;
function.name=name;
function.type=void_function_type;
Expand Down
4 changes: 2 additions & 2 deletions unit/analyses/dependence_graph.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ static symbolt create_void_function_symbol(
const irep_idt &name,
const codet &code)
{
code_typet void_function_type({}, empty_typet());
const code_typet void_function_type({}, empty_typet());
symbolt function;
function.name = name;
function.type = void_function_type;
Expand Down Expand Up @@ -74,7 +74,7 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]")
x_symbol.is_file_local = true;
goto_model.symbol_table.add(x_symbol);

code_typet void_function_type({}, empty_typet());
const code_typet void_function_type({}, empty_typet());

code_blockt a_body;
code_declt declare_x(x_symbol.symbol_expr());
Expand Down

0 comments on commit 64cd733

Please sign in to comment.