diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 46e220e6436..69758351b3f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -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(); diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 1258ffae4c9..e6e08371a6e 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -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; @@ -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; diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 61c0fcfaeed..9cc276f6400 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -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"; @@ -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; diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index a610681b504..87f303e6ec7 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -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); diff --git a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp index 10abe9a6184..1e7b9461e26 100644 --- a/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp +++ b/jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp @@ -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), diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 0942b4ca658..7b6b6cbbeee 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -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; diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index bfd7ec0f94a..5d00e411b38 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -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); diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp index cb1d28fbeb0..75aebd7f4b4 100644 --- a/src/cpp/cpp_typecheck_expr.cpp +++ b/src/cpp/cpp_typecheck_expr.cpp @@ -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()); @@ -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())}, @@ -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())}, @@ -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())}, @@ -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()), diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index c9b830be888..80bb234f3bb 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -611,14 +611,14 @@ 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); } @@ -626,7 +626,7 @@ void cpp_typecheck_resolvet::make_constructors( // 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); } diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index fd0da16dbe3..e530536a892 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -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); @@ -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); } diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 2a485e1ca00..2480dea2729 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -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" : @@ -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)); diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 80f787ca9c2..25d390c3dc8 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -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; @@ -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) diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp index 67f6fa68a82..c6e626af8b5 100644 --- a/unit/analyses/call_graph.cpp +++ b/unit/analyses/call_graph.cpp @@ -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; diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index 84f9535bbf7..be82c2700c5 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -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; @@ -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());