diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index d62c0b53d32..29fe4083429 100644 --- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -47,17 +47,14 @@ static symbolt add_or_get_symbol( ns.lookup(name, psymbol); if(psymbol != nullptr) return *psymbol; - symbolt new_symbol; - new_symbol.name = name; + symbolt new_symbol{name, type, ID_java}; new_symbol.pretty_name = name; new_symbol.base_name = base_name; - new_symbol.type = type; new_symbol.value = value; new_symbol.is_lvalue = true; new_symbol.is_state_var = true; new_symbol.is_static_lifetime = is_static_lifetime; new_symbol.is_thread_local = is_thread_local; - new_symbol.mode = ID_java; symbol_table.add(new_symbol); return new_symbol; } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 2c1fbca5a83..3efd1c6e667 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -449,14 +449,10 @@ void java_bytecode_convert_classt::convert( }(id2string(c.name)); // produce class symbol - symbolt new_symbol; + class_type.set_name(qualified_classname); + type_symbolt new_symbol{qualified_classname, class_type, ID_java}; new_symbol.base_name = base_name; new_symbol.pretty_name=c.name; - new_symbol.name=qualified_classname; - class_type.set_name(new_symbol.name); - new_symbol.type=class_type; - new_symbol.mode=ID_java; - new_symbol.is_type=true; symbolt *class_symbol; @@ -714,14 +710,15 @@ void java_bytecode_convert_classt::convert( component.type() = field_type; // Create the symbol - symbolt new_symbol; + symbolt new_symbol{ + id2string(class_symbol.name) + "." + id2string(f.name), + field_type, + ID_java}; new_symbol.is_static_lifetime=true; new_symbol.is_lvalue=true; new_symbol.is_state_var=true; - new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name); new_symbol.base_name=f.name; - new_symbol.type=field_type; // Provide a static field -> class link, like // java_bytecode_convert_method::convert does for method -> class. set_declaring_class(new_symbol, class_symbol.name); @@ -729,8 +726,6 @@ void java_bytecode_convert_classt::convert( new_symbol.type.set(ID_C_constant, f.is_final); new_symbol.pretty_name=id2string(class_symbol.pretty_name)+ "."+id2string(f.name); - new_symbol.mode=ID_java; - new_symbol.is_type=false; // These annotations use `ID_C_access` instead of `ID_access` like methods // to avoid type clashes in expressions like `some_static_field = 0`, where @@ -862,12 +857,8 @@ void add_java_array_types(symbol_table_baset &symbol_table) "Constructed a new type representing a Java Array " "object that doesn't match expectations"); - symbolt symbol; - symbol.name = struct_tag_type_identifier; + type_symbolt symbol{struct_tag_type_identifier, class_type, ID_java}; symbol.base_name = struct_tag_type.get(ID_C_base_name); - symbol.is_type=true; - symbol.type = class_type; - symbol.mode = ID_java; symbol_table.add(symbol); // Also provide a clone method: @@ -992,14 +983,11 @@ void add_java_array_types(symbol_table_baset &symbol_table) copy_loop, return_inst}); - symbolt clone_symbol; - clone_symbol.name=clone_name; + symbolt clone_symbol{clone_name, clone_type, ID_java}; clone_symbol.pretty_name = id2string(struct_tag_type_identifier) + ".clone:()"; clone_symbol.base_name="clone"; - clone_symbol.type=clone_type; clone_symbol.value=clone_body; - clone_symbol.mode=ID_java; symbol_table.add(clone_symbol); } } diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 037095bb366..be1b0d61aa6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -102,15 +102,11 @@ void create_method_stub_symbol( { messaget log(message_handler); - symbolt symbol; - symbol.name = identifier; + symbolt symbol{identifier, type, ID_java}; symbol.base_name = base_name; symbol.pretty_name = pretty_name; - symbol.type = type; symbol.type.set(ID_access, ID_private); to_java_method_type(symbol.type).set_is_final(true); - symbol.value.make_nil(); - symbol.mode = ID_java; assign_parameter_names( to_java_method_type(symbol.type), symbol.name, symbol_table); set_declaring_class(symbol, declaring_class); @@ -307,8 +303,6 @@ void java_bytecode_convert_method_lazy( symbol_table_baset &symbol_table, message_handlert &message_handler) { - symbolt method_symbol; - java_method_typet member_type = member_type_lazy( m.descriptor, m.signature, @@ -316,9 +310,8 @@ void java_bytecode_convert_method_lazy( id2string(m.base_name), message_handler); - method_symbol.name=method_identifier; + symbolt method_symbol{method_identifier, typet{}, ID_java}; method_symbol.base_name=m.base_name; - method_symbol.mode=ID_java; method_symbol.location=m.source_location; method_symbol.location.set_function(method_identifier); @@ -1900,13 +1893,9 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) // Add anonymous locals to the symtab: for(const auto &var : used_local_names) { - symbolt new_symbol; - new_symbol.name=var.get_identifier(); - new_symbol.type=var.type(); + symbolt new_symbol{var.get_identifier(), var.type(), ID_java}; new_symbol.base_name=var.get(ID_C_base_name); new_symbol.pretty_name=strip_java_namespace_prefix(var.get_identifier()); - new_symbol.mode=ID_java; - new_symbol.is_type=false; new_symbol.is_file_local=true; new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp index a617e12e2a6..84f9a4c7da9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp @@ -24,11 +24,8 @@ void java_internal_additions(symbol_table_baset &dest) // add __CPROVER_rounding_mode { - symbolt symbol; - symbol.name = rounding_mode_identifier(); + symbolt symbol{rounding_mode_identifier(), signed_int_type(), ID_C}; symbol.base_name = symbol.name; - symbol.type=signed_int_type(); - symbol.mode=ID_C; symbol.is_lvalue=true; symbol.is_state_var=true; symbol.is_thread_local=true; @@ -36,14 +33,13 @@ void java_internal_additions(symbol_table_baset &dest) } { - auxiliary_symbolt symbol; + auxiliary_symbolt symbol{ + INFLIGHT_EXCEPTION_VARIABLE_NAME, + pointer_type(java_void_type()), + ID_java}; symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME; - symbol.name = INFLIGHT_EXCEPTION_VARIABLE_NAME; - symbol.mode = ID_java; - symbol.type = pointer_type(java_void_type()); symbol.type.set(ID_C_no_nondet_initialization, true); symbol.value = null_pointer_exprt(to_pointer_type(symbol.type)); - symbol.is_file_local = false; symbol.is_static_lifetime = true; dest.add(symbol); } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index a87fe77ac83..2a0395dd6d9 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -528,15 +528,13 @@ static symbol_exprt get_or_create_class_literal_symbol( java_lang_Class); if(!symbol_table.has_symbol(symbol_expr.get_identifier())) { - symbolt new_class_symbol; - new_class_symbol.name = symbol_expr.get_identifier(); - new_class_symbol.type = symbol_expr.type(); + symbolt new_class_symbol{ + symbol_expr.get_identifier(), symbol_expr.type(), ID_java}; INVARIANT( has_prefix(id2string(new_class_symbol.name), "java::"), "class identifier should have 'java::' prefix"); new_class_symbol.base_name = id2string(new_class_symbol.name).substr(6); - new_class_symbol.mode = ID_java; new_class_symbol.is_lvalue = true; new_class_symbol.is_state_var = true; new_class_symbol.is_static_lifetime = true; @@ -651,13 +649,11 @@ static void create_stub_global_symbol( const irep_idt &class_id, bool force_nondet_init) { - symbolt new_symbol; + symbolt new_symbol{symbol_id, symbol_type, ID_java}; new_symbol.is_static_lifetime = true; new_symbol.is_lvalue = true; new_symbol.is_state_var = true; - new_symbol.name = symbol_id; new_symbol.base_name = symbol_basename; - new_symbol.type = symbol_type; set_declaring_class(new_symbol, class_id); // Public access is a guess; it encourages merging like-typed static fields, // whereas a more restricted visbility would encourage separating them. @@ -666,8 +662,6 @@ static void create_stub_global_symbol( // We set the field as final to avoid assuming they can be overridden. new_symbol.type.set(ID_C_constant, true); new_symbol.pretty_name = new_symbol.name; - new_symbol.mode = ID_java; - new_symbol.is_type = false; // If pointer-typed, initialise to null and a static initialiser will be // created to initialise on first reference. If primitive-typed, specify // nondeterministic initialisation by setting a nil value. diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 27628afeabd..1f8bc5e3349 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -50,12 +50,10 @@ void create_java_initialize(symbol_table_baset &symbol_table) // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend. symbol_table.remove(INITIALIZE_FUNCTION); - symbolt initialize; - initialize.name=INITIALIZE_FUNCTION; + symbolt initialize{ + INITIALIZE_FUNCTION, java_method_typet({}, java_void_type()), ID_java}; initialize.base_name=INITIALIZE_FUNCTION; - initialize.mode=ID_java; - initialize.type = java_method_typet({}, java_void_type()); symbol_table.add(initialize); } @@ -764,13 +762,12 @@ bool generate_java_start_function( // create a symbol for the __CPROVER__start function, associate the code that // we just built and register it in the symbol table - symbolt new_symbol; - - new_symbol.name=goto_functionst::entry_point(); + symbolt new_symbol{ + goto_functionst::entry_point(), + java_method_typet{{}, java_void_type()}, + ID_java}; new_symbol.base_name = goto_functionst::entry_point(); - new_symbol.type = java_method_typet({}, java_void_type()); new_symbol.value.swap(init_code); - new_symbol.mode=ID_java; if(!symbol_table.insert(std::move(new_symbol)).second) { diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 9ac430d1b05..977a336ae22 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -832,13 +832,9 @@ void java_bytecode_convert_methodt::setup_local_variables( result, v.var.start_pc, v.var.length, false, std::move(v.holes)); // Register the local variable in the symbol table - symbolt new_symbol; - new_symbol.name=identifier; - new_symbol.type=t; + symbolt new_symbol{identifier, t, ID_java}; new_symbol.base_name=v.var.name; new_symbol.pretty_name=id2string(identifier).substr(6, std::string::npos); - new_symbol.mode=ID_java; - new_symbol.is_type=false; new_symbol.is_file_local=true; new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 6634523c15a..e107ea9e4d5 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -120,18 +120,15 @@ static symbolt add_new_variable_symbol( const bool is_thread_local, const bool is_static_lifetime) { - symbolt new_symbol; - new_symbol.name = name; + symbolt new_symbol{name, type, ID_java}; new_symbol.pretty_name = name; new_symbol.base_name = name; - new_symbol.type = type; new_symbol.type.set(ID_C_no_nondet_initialization, true); new_symbol.value = value; new_symbol.is_lvalue = true; new_symbol.is_state_var = true; new_symbol.is_static_lifetime = is_static_lifetime; new_symbol.is_thread_local = is_thread_local; - new_symbol.mode = ID_java; symbol_table.add(new_symbol); return new_symbol; } @@ -336,16 +333,14 @@ static void create_function_symbol( symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods) { - symbolt function_symbol; - const java_method_typet function_type({}, java_void_type()); + symbolt function_symbol{ + function_name, java_method_typet({}, java_void_type()), ID_java}; function_symbol.name = function_name; function_symbol.pretty_name = function_symbol.name; function_symbol.base_name = function_base_name; - function_symbol.type = function_type; // This provides a back-link from a method to its associated class, as is done // for java_bytecode_convert_methodt::convert. set_declaring_class(function_symbol, class_name); - function_symbol.mode = ID_java; bool failed = symbol_table.add(function_symbol); INVARIANT(!failed, id2string(function_base_name) + " symbol should be fresh"); @@ -969,14 +964,10 @@ 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"); - const java_method_typet thunk_type({}, java_void_type()); - - symbolt static_init_symbol; - static_init_symbol.name = static_init_name; + symbolt static_init_symbol{ + static_init_name, java_method_typet({}, java_void_type()), ID_java}; static_init_symbol.pretty_name = static_init_name; static_init_symbol.base_name = "clinit():V"; - static_init_symbol.mode = ID_java; - static_init_symbol.type = thunk_type; // This provides a back-link from a method to its associated class, as is // done for java_bytecode_convert_methodt::convert. set_declaring_class(static_init_symbol, it->first); diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index e5ea1b6a645..3fed7144ed6 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -221,8 +221,7 @@ void java_string_library_preprocesst::add_string_type( symbol_table_baset &symbol_table) { irep_idt class_symbol_name = "java::" + id2string(class_name); - symbolt tmp_string_symbol; - tmp_string_symbol.name = class_symbol_name; + type_symbolt tmp_string_symbol{class_symbol_name, typet{}, ID_java}; symbolt *string_symbol = nullptr; bool already_exists = symbol_table.move(tmp_string_symbol, string_symbol); @@ -250,8 +249,6 @@ void java_string_library_preprocesst::add_string_type( string_symbol->base_name = id2string(class_name); string_symbol->pretty_name = id2string(class_name); string_symbol->type = new_string_type; - string_symbol->is_type = true; - string_symbol->mode = ID_java; } auto &string_type = to_java_class_type(string_symbol->type); diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index f153e692e20..d22899f77e3 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -57,14 +57,10 @@ symbol_exprt get_or_create_string_literal_symbol( #endif // Create a new symbol: - symbolt new_symbol; - new_symbol.name = escaped_symbol_name_with_prefix; - new_symbol.type = string_type; + symbolt new_symbol{escaped_symbol_name_with_prefix, string_type, ID_java}; new_symbol.type.set(ID_C_constant, true); new_symbol.base_name = escaped_symbol_name; new_symbol.pretty_name = value; - new_symbol.mode = ID_java; - new_symbol.is_type = false; new_symbol.is_lvalue = true; new_symbol.is_state_var = true; new_symbol.is_static_lifetime = true; @@ -97,18 +93,15 @@ symbol_exprt get_or_create_string_literal_symbol( literal_init.operands()[length_nb] = length; // Initialize the string with a constant utf-16 array: - symbolt array_symbol; - array_symbol.name = escaped_symbol_name_with_prefix + "_constarray"; + symbolt array_symbol{ + escaped_symbol_name_with_prefix + "_constarray", data.type(), ID_java}; array_symbol.base_name = escaped_symbol_name + "_constarray"; array_symbol.pretty_name = value; - array_symbol.mode = ID_java; - array_symbol.is_type = false; array_symbol.is_lvalue = true; // These are basically const global data: array_symbol.is_static_lifetime = true; array_symbol.is_state_var = true; array_symbol.value = data; - array_symbol.type = array_symbol.value.type(); array_symbol.type.set(ID_C_constant, true); if(symbol_table.add(array_symbol)) @@ -122,15 +115,13 @@ symbol_exprt get_or_create_string_literal_symbol( literal_init.operands()[data_nb] = array_pointer; // Associate array with pointer - symbolt return_symbol; - return_symbol.name = escaped_symbol_name_with_prefix + "_return_value"; + symbolt return_symbol{ + escaped_symbol_name_with_prefix + "_return_value", typet{}, ID_java}; return_symbol.base_name = escaped_symbol_name + "_return_value"; return_symbol.pretty_name = escaped_symbol_name.length() > 10 ? escaped_symbol_name.substr(0, 10) + "..._return_value" : escaped_symbol_name + "_return_value"; - return_symbol.mode = ID_java; - return_symbol.is_type = false; return_symbol.is_lvalue = true; return_symbol.is_static_lifetime = true; return_symbol.is_state_var = true; diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index be1c4d09ba2..1112df70a87 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -171,14 +171,11 @@ void generate_class_stub( class_type.set_is_stub(true); // produce class symbol - symbolt new_symbol; + irep_idt qualified_class_name = "java::" + id2string(class_name); + class_type.set_name(qualified_class_name); + type_symbolt new_symbol{qualified_class_name, std::move(class_type), ID_java}; new_symbol.base_name=class_name; new_symbol.pretty_name=class_name; - new_symbol.name="java::"+id2string(class_name); - class_type.set_name(new_symbol.name); - new_symbol.type=class_type; - new_symbol.mode=ID_java; - new_symbol.is_type=true; std::pair res=symbol_table.insert(std::move(new_symbol)); diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp index fbc45700e25..17975e12ff6 100644 --- a/jbmc/src/java_bytecode/lambda_synthesis.cpp +++ b/jbmc/src/java_bytecode/lambda_synthesis.cpp @@ -292,10 +292,7 @@ symbolt synthetic_class_symbol( } } - symbolt synthetic_class_symbol = type_symbolt{synthetic_class_type}; - synthetic_class_symbol.name = synthetic_class_name; - synthetic_class_symbol.mode = ID_java; - return synthetic_class_symbol; + return type_symbolt{synthetic_class_name, synthetic_class_type, ID_java}; } static symbolt constructor_symbol( @@ -303,12 +300,10 @@ static symbolt constructor_symbol( const irep_idt &synthetic_class_name, java_method_typet constructor_type) // dynamic_method_type { - symbolt constructor_symbol; irep_idt constructor_name = id2string(synthetic_class_name) + "."; - constructor_symbol.name = constructor_name; + symbolt constructor_symbol{constructor_name, typet{}, ID_java}; constructor_symbol.pretty_name = constructor_symbol.name; constructor_symbol.base_name = ""; - constructor_symbol.mode = ID_java; synthetic_methods[constructor_name] = synthetic_method_typet::INVOKEDYNAMIC_CAPTURE_CONSTRUCTOR; @@ -349,14 +344,12 @@ static symbolt implemented_method_symbol( id2string(method_to_implement.get_base_name()) + ":" + id2string(method_to_implement.get_descriptor()); - symbolt implemented_method_symbol; - implemented_method_symbol.name = implemented_method_name; + symbolt implemented_method_symbol{ + implemented_method_name, method_to_implement.type(), ID_java}; synthetic_methods[implemented_method_symbol.name] = synthetic_method_typet::INVOKEDYNAMIC_METHOD; implemented_method_symbol.pretty_name = implemented_method_symbol.name; implemented_method_symbol.base_name = method_to_implement.get_base_name(); - implemented_method_symbol.mode = ID_java; - implemented_method_symbol.type = method_to_implement.type(); auto &implemented_method_type = to_code_type(implemented_method_symbol.type); implemented_method_type.parameters()[0].type() = java_reference_type(struct_tag_typet(synthetic_class_name)); diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 8acdeca6b3a..547ae2f148f 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -36,10 +36,7 @@ SCENARIO( java_class_typet jlo_class_type; jlo_class_type.set_tag("java.lang.Object"); jlo_class_type.set_name("java::java.lang.Object"); - symbolt jlo_sym; - jlo_sym.name = "java::java.lang.Object"; - jlo_sym.type = jlo_class_type; - jlo_sym.is_type = true; + type_symbolt jlo_sym{"java::java.lang.Object", jlo_class_type, ID_java}; java_root_class(jlo_sym); bool failed = symbol_table.add(jlo_sym); CHECK_RETURN(!failed); diff --git a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp index 3c7b3d306b3..55afffa9084 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp @@ -26,8 +26,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com static irep_idt add_clinit(symbol_tablet &symbol_table, const std::string &class_name) { - symbolt clinit_symbol; - clinit_symbol.name = "java::" + class_name + ".:()V"; + symbolt clinit_symbol{ + "java::" + class_name + ".:()V", typet{}, ID_java}; set_declaring_class(clinit_symbol, "java::" + class_name); symbol_table.insert(clinit_symbol); return clinit_symbol.name; @@ -38,18 +38,19 @@ static void add_class_with_components( const std::string &class_name, const std::vector> &components) { - symbolt test_class_symbol; - test_class_symbol.name = "java::" + class_name; - test_class_symbol.is_type = true; - test_class_symbol.type = [&] { - java_class_typet type; - // TODO java_class_typet constructors should ensure there is always a - // @class_identifier field, and that name is always set - type.set_name(test_class_symbol.name); - for(const auto &pair : components) - type.components().emplace_back(pair.first, pair.second); - return type; - }(); + irep_idt type_name = "java::" + class_name; + type_symbolt test_class_symbol{ + type_name, + [&] { + java_class_typet type; + // TODO java_class_typet constructors should ensure there is always a + // @class_identifier field, and that name is always set + type.set_name(type_name); + for(const auto &pair : components) + type.components().emplace_back(pair.first, pair.second); + return type; + }(), + ID_java}; symbol_table.insert(test_class_symbol); } @@ -76,10 +77,8 @@ SCENARIO( return entry; }(); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "field_name"; - field_symbol.name = "field_name_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); @@ -165,10 +164,8 @@ SCENARIO( return entry; }(); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "array_field"; - field_symbol.name = "field_name_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); @@ -290,10 +287,8 @@ SCENARIO( return entry; }(); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "array_field"; - field_symbol.name = "field_name_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); @@ -449,18 +444,14 @@ SCENARIO( return entry; }(); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_1_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "array_field_1"; - field_symbol.name = "field_name_1_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_2_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "array_field_2"; - field_symbol.name = "field_name_2_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); diff --git a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp index 4f58f4c5c5b..70849a02558 100644 --- a/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp +++ b/jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp @@ -76,8 +76,7 @@ SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]") "A class which has no entry in the JSON object but a clinit defined " "in the symbol table") { - symbolt clinit_symbol; - clinit_symbol.name = "java::TestClass.:()V"; + symbolt clinit_symbol{"java::TestClass.:()V", typet{}, ID_java}; symbol_table.insert(clinit_symbol); const code_blockt clinit_body = get_user_specified_clinit_body( @@ -146,29 +145,24 @@ SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]") return entry; }(); class_to_declared_symbols.emplace("java::TestClass", [] { - symbolt field_symbol; + symbolt field_symbol{"field_name_for_codet", java_int_type(), ID_java}; field_symbol.base_name = "field_name"; - field_symbol.name = "field_name_for_codet"; - field_symbol.type = java_int_type(); field_symbol.is_static_lifetime = true; return field_symbol; }()); symbol_table.insert([] { - symbolt clinit_symbol; - clinit_symbol.name = "java::TestClass.:()V"; + symbolt clinit_symbol{"java::TestClass.:()V", typet{}, ID_java}; set_declaring_class(clinit_symbol, "java::TestClass"); return clinit_symbol; }()); - symbol_table.insert([] { - symbolt test_class_symbol; - test_class_symbol.name = "java::TestClass"; - test_class_symbol.type = [] { + symbol_table.insert(symbolt{ + "java::TestClass", + [] { java_class_typet type; type.components().emplace_back("field_name", java_int_type()); return type; - }(); - return test_class_symbol; - }()); + }(), + ID_java}); const auto clinit_body = get_user_specified_clinit_body( "java::TestClass", static_values_json, diff --git a/jbmc/unit/java_bytecode/load_method_by_regex.cpp b/jbmc/unit/java_bytecode/load_method_by_regex.cpp index a694051383e..f4245254100 100644 --- a/jbmc/unit/java_bytecode/load_method_by_regex.cpp +++ b/jbmc/unit/java_bytecode/load_method_by_regex.cpp @@ -94,10 +94,7 @@ SCENARIO( static symbolt create_method_symbol(const std::string &method_name) { - symbolt new_symbol; - new_symbol.name = method_name; - new_symbol.type = java_method_typet{{}, typet{}}; - return new_symbol; + return symbolt{method_name, java_method_typet{{}, typet{}}, ID_java}; } static void require_result_for_pattern( diff --git a/jbmc/unit/util/has_subtype.cpp b/jbmc/unit/util/has_subtype.cpp index 45dea2cec76..3be9c6aad7a 100644 --- a/jbmc/unit/util/has_subtype.cpp +++ b/jbmc/unit/util/has_subtype.cpp @@ -68,10 +68,7 @@ SCENARIO("has_subtype", "[core][utils][has_subtype]") struct_tag_typet struct_tag("A-struct"); struct_typet struct_type({{"ptr", pointer_type(struct_tag)}}); - symbolt s; - s.type = struct_type; - s.name = "A-struct"; - s.is_type = true; + type_symbolt s{"A-struct", struct_type, ID_java}; symbol_table.add(s); THEN("has_subtype terminates") diff --git a/regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c b/regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c index 0a213243b5e..3f7eac6e969 100644 --- a/regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c +++ b/regression/goto-instrument/dump-type-header-exclude-non-module-var/main.c @@ -8,11 +8,13 @@ struct B #define temperature(x) x.t +int __VERIFIER_nondet_int(); + int main() { struct B aStruct = {3, 8}; __CPROVER_assert(my_config.a == 7, "Should be valid"); - my_config.a = nondet_int(); + my_config.a = __VERIFIER_nondet_int(); __CPROVER_assert(!(my_config.a == 4), "Should be nondet now"); __CPROVER_assert(aStruct.t, "Should not be null"); diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 70c35cf108f..f3c18659880 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -255,14 +255,10 @@ bool generate_ansi_c_start_function( namespacet ns(symbol_table); { - symbolt argc_symbol; - + symbolt argc_symbol{"argc'", signed_int_type(), ID_C}; argc_symbol.base_name = "argc'"; - argc_symbol.name = "argc'"; - argc_symbol.type = signed_int_type(); argc_symbol.is_static_lifetime = true; argc_symbol.is_lvalue = true; - argc_symbol.mode = ID_C; auto r = symbol_table.insert(argc_symbol); if(!r.second && r.first != argc_symbol) @@ -284,14 +280,10 @@ bool generate_ansi_c_start_function( const plus_exprt size_expr(argc_symbol.symbol_expr(), one_expr); const array_typet argv_type(pointer_type(char_type()), size_expr); - symbolt argv_symbol; - + symbolt argv_symbol{"argv'", argv_type, ID_C}; argv_symbol.base_name = "argv'"; - argv_symbol.name = "argv'"; - argv_symbol.type = argv_type; argv_symbol.is_static_lifetime = true; argv_symbol.is_lvalue = true; - argv_symbol.mode = ID_C; auto r = symbol_table.insert(argv_symbol); if(!r.second && r.first != argv_symbol) @@ -337,12 +329,9 @@ bool generate_ansi_c_start_function( if(parameters.size()==3) { { - symbolt envp_size_symbol; + symbolt envp_size_symbol{"envp_size'", size_type(), ID_C}; envp_size_symbol.base_name = "envp_size'"; - envp_size_symbol.name = "envp_size'"; - envp_size_symbol.type = size_type(); envp_size_symbol.is_static_lifetime = true; - envp_size_symbol.mode = ID_C; if(!symbol_table.insert(std::move(envp_size_symbol)).second) { @@ -356,13 +345,13 @@ bool generate_ansi_c_start_function( const symbolt &envp_size_symbol=ns.lookup("envp_size'"); { - symbolt envp_symbol; + symbolt envp_symbol{ + "envp'", + array_typet( + pointer_type(char_type()), envp_size_symbol.symbol_expr()), + ID_C}; envp_symbol.base_name = "envp'"; - envp_symbol.name = "envp'"; - envp_symbol.type = array_typet( - pointer_type(char_type()), envp_size_symbol.symbol_expr()); envp_symbol.is_static_lifetime = true; - envp_symbol.mode = ID_C; if(!symbol_table.insert(std::move(envp_symbol)).second) { @@ -543,13 +532,10 @@ bool generate_ansi_c_start_function( } // add the entry point symbol - symbolt new_symbol; - - new_symbol.name=goto_functionst::entry_point(); + symbolt new_symbol{ + goto_functionst::entry_point(), code_typet{{}, void_type()}, symbol.mode}; new_symbol.base_name = goto_functionst::entry_point(); - new_symbol.type = code_typet({}, void_type()); new_symbol.value.swap(init_code); - new_symbol.mode=symbol.mode; if(!symbol_table.insert(std::move(new_symbol)).second) { diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index bf00f4f8d62..9a8609d1a48 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -547,11 +547,8 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) code_typet symbol_type=new_type; symbol_type.return_type()=void_type(); - symbolt symbol; + symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C}; symbol.base_name=ID_gcc_builtin_va_arg; - symbol.name=ID_gcc_builtin_va_arg; - symbol.type=symbol_type; - symbol.mode = ID_C; symbol_table.insert(std::move(symbol)); } @@ -2175,13 +2172,10 @@ void c_typecheck_baset::typecheck_side_effect_function_call( symbol_table.add(new_symbol); } - symbolt new_symbol; - - new_symbol.name = identifier_with_type; + symbolt new_symbol{ + identifier_with_type, gcc_polymorphic->type(), ID_C}; new_symbol.base_name = identifier_with_type; new_symbol.location = f_op.source_location(); - new_symbol.type = gcc_polymorphic->type(); - new_symbol.mode = ID_C; code_blockt implementation = instantiate_gcc_polymorphic_builtin(identifier, *gcc_polymorphic); typet parent_return_type = return_type; @@ -2213,12 +2207,10 @@ void c_typecheck_baset::typecheck_side_effect_function_call( guessed_return_type = pointer_type(void_type()); // void * } - symbolt new_symbol; - - new_symbol.name=identifier; + symbolt new_symbol{ + identifier, code_typet({}, guessed_return_type), mode}; new_symbol.base_name=identifier; new_symbol.location=expr.source_location(); - new_symbol.type = code_typet({}, guessed_return_type); new_symbol.type.set(ID_C_incomplete, true); // TODO: should also guess some argument types diff --git a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp index 2cbc4f0c7e7..40bb18332f6 100644 --- a/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp +++ b/src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp @@ -612,11 +612,8 @@ static symbolt result_symbol( const source_locationt &source_location, symbol_table_baset &symbol_table) { - symbolt symbol; - symbol.name = id2string(identifier) + "::1::result"; + symbolt symbol{id2string(identifier) + "::1::result", type, ID_C}; symbol.base_name = "result"; - symbol.type = type; - symbol.mode = ID_C; symbol.location = source_location; symbol.is_file_local = true; symbol.is_lvalue = true; diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp index 9204f3ff5cc..732fd11ca73 100644 --- a/src/ansi-c/c_typecheck_initializer.cpp +++ b/src/ansi-c/c_typecheck_initializer.cpp @@ -1039,13 +1039,11 @@ exprt c_typecheck_baset::do_initializer_list( // mimic bits of typecheck_compound_type to produce a new struct tag actual_struct_type.remove(ID_tag); - type_symbolt compound_symbol{actual_struct_type}; - compound_symbol.mode = mode; - compound_symbol.location = value.source_location(); - std::string typestr = type2name(compound_symbol.type, *this); + std::string typestr = type2name(actual_struct_type, *this); + irep_idt tag_identifier = "tag-#anon#" + typestr; + type_symbolt compound_symbol{tag_identifier, actual_struct_type, mode}; compound_symbol.base_name = "#anon#" + typestr; - compound_symbol.name = "tag-#anon#" + typestr; - irep_idt tag_identifier = compound_symbol.name; + compound_symbol.location = value.source_location(); // We might already have the same anonymous struct, which is fine as it // will be exactly the same type. diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index ca17a7746ea..9323b34841d 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -785,9 +785,7 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) assert(have_body); // produce symbol - symbolt compound_symbol; - compound_symbol.is_type=true; - compound_symbol.type=type; + type_symbolt compound_symbol{irep_idt{}, type, mode}; compound_symbol.location=type.source_location(); typecheck_compound_body(to_struct_union_type(compound_symbol.type)); @@ -821,11 +819,8 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type) type.remove(ID_tag); type.set(ID_tag, base_name); - symbolt compound_symbol; - compound_symbol.is_type=true; - compound_symbol.name=identifier; + type_symbolt compound_symbol{identifier, type, mode}; compound_symbol.base_name=base_name; - compound_symbol.type=type; compound_symbol.location=type.source_location(); compound_symbol.pretty_name=id2string(type.id())+" "+id2string(base_name); @@ -1368,14 +1363,10 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type) irep_idt identifier=tag.get(ID_identifier); // Put into symbol table - symbolt enum_tag_symbol; - - enum_tag_symbol.is_type=true; - enum_tag_symbol.type=type; + type_symbolt enum_tag_symbol{identifier, type, mode}; enum_tag_symbol.location=source_location; enum_tag_symbol.is_file_local=true; enum_tag_symbol.base_name=base_name; - enum_tag_symbol.name=identifier; // throw in the enum members as 'body' irept::subt &body=enum_tag_symbol.type.add(ID_body).get_sub(); @@ -1478,14 +1469,10 @@ void c_typecheck_baset::typecheck_c_enum_tag_type(c_enum_tag_typet &type) new_type.add(ID_tag)=tag; new_type.make_incomplete(); - symbolt enum_tag_symbol; - - enum_tag_symbol.is_type=true; - enum_tag_symbol.type=new_type; + type_symbolt enum_tag_symbol{identifier, new_type, mode}; enum_tag_symbol.location=source_location; enum_tag_symbol.is_file_local=true; enum_tag_symbol.base_name=base_name; - enum_tag_symbol.name=identifier; symbolt *new_symbol; move_symbol(enum_tag_symbol, new_symbol); diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 0d2bab1473c..9374b3d41e9 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -124,13 +124,8 @@ void remove_asmt::gcc_asm_function_call( // do we have it? if(!symbol_table.has_symbol(function_identifier)) { - symbolt symbol; - - symbol.name = function_identifier; - symbol.type = fkt_type; + symbolt symbol{function_identifier, fkt_type, ID_C}; symbol.base_name = function_base_name; - symbol.value = nil_exprt(); - symbol.mode = ID_C; symbol_table.add(symbol); @@ -182,13 +177,8 @@ void remove_asmt::msc_asm_function_call( // do we have it? if(!symbol_table.has_symbol(function_identifier)) { - symbolt symbol; - - symbol.name = function_identifier; - symbol.type = fkt_type; + symbolt symbol{function_identifier, fkt_type, ID_C}; symbol.base_name = function_base_name; - symbol.value = nil_exprt(); - symbol.mode = ID_C; symbol_table.add(symbol); diff --git a/src/cpp/cpp_declarator_converter.cpp b/src/cpp/cpp_declarator_converter.cpp index bba2ded6409..d65fdebf948 100644 --- a/src/cpp/cpp_declarator_converter.cpp +++ b/src/cpp/cpp_declarator_converter.cpp @@ -443,18 +443,17 @@ symbolt &cpp_declarator_convertert::convert_new_symbol( { irep_idt pretty_name=get_pretty_name(); - symbolt symbol; - - symbol.name=final_identifier; + symbolt symbol{ + final_identifier, + final_type, + linkage_spec == ID_auto ? ID_cpp : linkage_spec}; symbol.base_name=base_name; symbol.value=declarator.value(); symbol.location=declarator.name().source_location(); symbol.is_extern = storage_spec.is_extern(); symbol.is_parameter = declarator.get_is_parameter(); symbol.is_weak = storage_spec.is_weak(); - symbol.mode=linkage_spec==ID_auto?ID_cpp:linkage_spec; symbol.module=cpp_typecheck.module; - symbol.type=final_type; symbol.is_type=is_typedef; symbol.is_macro=is_typedef && !is_template_parameter; symbol.pretty_name=pretty_name; diff --git a/src/cpp/cpp_instantiate_template.cpp b/src/cpp/cpp_instantiate_template.cpp index b9cbc7646b7..837e9b8c8dc 100644 --- a/src/cpp/cpp_instantiate_template.cpp +++ b/src/cpp/cpp_instantiate_template.cpp @@ -183,11 +183,9 @@ const symbolt &cpp_typecheckt::class_template_symbol( // Create as incomplete struct, but mark as // "template_class_instance", to be elaborated later. - symbolt new_symbol; - new_symbol.name=identifier; + type_symbolt new_symbol{identifier, struct_typet(), template_symbol.mode}; new_symbol.pretty_name=template_symbol.pretty_name; new_symbol.location=template_symbol.location; - new_symbol.type = struct_typet(); to_struct_type(new_symbol.type).make_incomplete(); new_symbol.type.set(ID_tag, template_symbol.type.find(ID_tag)); if(template_symbol.type.get_bool(ID_C_class)) @@ -198,9 +196,7 @@ const symbolt &cpp_typecheckt::class_template_symbol( ID_specialization_template_args, specialization_template_args); new_symbol.type.set(ID_full_template_args, full_template_args); new_symbol.type.set(ID_identifier, template_symbol.name); - new_symbol.mode=template_symbol.mode; new_symbol.base_name=template_symbol.base_name; - new_symbol.is_type=true; symbolt *s_ptr; symbol_table.move(new_symbol, s_ptr); diff --git a/src/cpp/cpp_typecheck.cpp b/src/cpp/cpp_typecheck.cpp index aa03044204e..166d036c1b3 100644 --- a/src/cpp/cpp_typecheck.cpp +++ b/src/cpp/cpp_typecheck.cpp @@ -199,16 +199,13 @@ void cpp_typecheckt::static_and_dynamic_initialization() dynamic_initializations.clear(); // Create the dynamic initialization procedure - symbolt init_symbol; - - init_symbol.name="#cpp_dynamic_initialization#"+id2string(module); + symbolt init_symbol{ + "#cpp_dynamic_initialization#" + id2string(module), + code_typet({}, typet(ID_constructor)), + ID_cpp}; init_symbol.base_name="#cpp_dynamic_initialization#"+id2string(module); init_symbol.value.swap(init_block); - init_symbol.mode=ID_cpp; init_symbol.module=module; - init_symbol.type = code_typet({}, typet(ID_constructor)); - init_symbol.is_type=false; - init_symbol.is_macro=false; symbol_table.insert(std::move(init_symbol)); diff --git a/src/cpp/cpp_typecheck_compound_type.cpp b/src/cpp/cpp_typecheck_compound_type.cpp index 5f09a33edb8..603c5de70cf 100644 --- a/src/cpp/cpp_typecheck_compound_type.cpp +++ b/src/cpp/cpp_typecheck_compound_type.cpp @@ -229,17 +229,10 @@ void cpp_typecheckt::typecheck_compound_type( else { // produce new symbol - symbolt symbol; - - symbol.name=symbol_name; + type_symbolt symbol{symbol_name, type, ID_cpp}; symbol.base_name=base_name; - symbol.value.make_nil(); symbol.location=type.source_location(); - symbol.mode=ID_cpp; symbol.module=module; - symbol.type.swap(type); - symbol.is_type=true; - symbol.is_macro=false; symbol.pretty_name= cpp_scopes.current_scope().prefix+ id2string(symbol.base_name)+ @@ -577,16 +570,12 @@ void cpp_typecheckt::typecheck_compound_declarator( if(!symbol_table.has_symbol(vt_name)) { // first time: create a virtual-table symbol type - symbolt vt_symb_type; - vt_symb_type.name= vt_name; + type_symbolt vt_symb_type{vt_name, struct_typet(), ID_cpp}; vt_symb_type.base_name="virtual_table::"+id2string(symbol.base_name); vt_symb_type.pretty_name=vt_symb_type.base_name; - vt_symb_type.mode=ID_cpp; vt_symb_type.module=module; vt_symb_type.location=symbol.location; - vt_symb_type.type=struct_typet(); vt_symb_type.type.set(ID_name, vt_symb_type.name); - vt_symb_type.is_type=true; const bool failed=!symbol_table.insert(std::move(vt_symb_type)).second; CHECK_RETURN(!failed); @@ -626,15 +615,14 @@ void cpp_typecheckt::typecheck_compound_declarator( irep_idt virtual_base=*virtual_bases.begin(); // a new function that does 'late casting' of the 'this' parameter - symbolt func_symb; - func_symb.name= - id2string(component.get_name())+"::"+id2string(virtual_base); + symbolt func_symb{ + id2string(component.get_name()) + "::" + id2string(virtual_base), + component.type(), + symbol.mode}; func_symb.base_name = component.get_base_name(); func_symb.pretty_name = component.get_base_name(); - func_symb.mode = symbol.mode; func_symb.module=module; func_symb.location=component.source_location(); - func_symb.type=component.type(); // change the type of the 'this' pointer code_typet &code_type=to_code_type(func_symb.type); @@ -653,14 +641,13 @@ void cpp_typecheckt::typecheck_compound_declarator( if(param_base_name.empty()) param_base_name = "arg" + std::to_string(i++); - symbolt arg_symb; - arg_symb.name = - id2string(func_symb.name) + "::" + id2string(param_base_name); + symbolt arg_symb{ + id2string(func_symb.name) + "::" + id2string(param_base_name), + arg.type(), + symbol.mode}; arg_symb.base_name = param_base_name; arg_symb.pretty_name = param_base_name; - arg_symb.mode = symbol.mode; arg_symb.location=func_symb.location; - arg_symb.type=arg.type(); arg.set_identifier(arg_symb.name); @@ -725,10 +712,7 @@ void cpp_typecheckt::typecheck_compound_declarator( if(is_static && !is_method) // static non-method member { // add as global variable to symbol_table - symbolt static_symbol; - static_symbol.mode=symbol.mode; - static_symbol.name=identifier; - static_symbol.type=component.type(); + symbolt static_symbol{identifier, component.type(), symbol.mode}; static_symbol.base_name = component.get_base_name(); static_symbol.is_lvalue=true; static_symbol.is_static_lifetime=true; @@ -1282,8 +1266,6 @@ void cpp_typecheckt::typecheck_member_function( const typet &method_qualifier, exprt &value) { - symbolt symbol; - code_typet &type = to_code_type(component.type()); if(component.get_bool(ID_is_static)) @@ -1322,14 +1304,10 @@ void cpp_typecheckt::typecheck_member_function( if(value.is_not_nil()) to_code_type(type).set_inlined(true); - symbol.name=identifier; + symbolt symbol{identifier, type, compound_symbol.mode}; symbol.base_name=component.get_base_name(); symbol.value.swap(value); - symbol.mode = compound_symbol.mode; symbol.module=module; - symbol.type=type; - symbol.is_type=false; - symbol.is_macro=false; symbol.location=component.source_location(); // move early, it must be visible before doing any value diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/src/cpp/cpp_typecheck_enum_type.cpp index 72f53e159e1..d01c4e55a36 100644 --- a/src/cpp/cpp_typecheck_enum_type.cpp +++ b/src/cpp/cpp_typecheck_enum_type.cpp @@ -51,17 +51,15 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol) exprt value_expr = from_integer(i, c_enum_type.underlying_type()); value_expr.type()=enum_tag_type; // override type - symbolt symbol; - - symbol.name=id2string(enum_symbol.name)+"::"+id2string(name); + symbolt symbol{ + id2string(enum_symbol.name) + "::" + id2string(name), + enum_tag_type, + enum_symbol.mode}; symbol.base_name=name; symbol.value=value_expr; symbol.location = static_cast( component.find(ID_C_source_location)); - symbol.mode = enum_symbol.mode; symbol.module=module; - symbol.type=enum_tag_type; - symbol.is_type=false; symbol.is_macro=true; symbol.is_file_local = true; symbol.is_thread_local = true; @@ -167,17 +165,11 @@ void cpp_typecheckt::typecheck_enum_type(typet &type) } } - symbolt symbol; - - symbol.name=symbol_name; + type_symbolt symbol{symbol_name, type, ID_cpp}; symbol.base_name=base_name; symbol.value.make_nil(); symbol.location=type.source_location(); - symbol.mode=ID_cpp; symbol.module=module; - symbol.type.swap(type); - symbol.is_type=true; - symbol.is_macro=false; symbol.pretty_name=pretty_name; // move early, must be visible before doing body diff --git a/src/cpp/cpp_typecheck_namespace.cpp b/src/cpp/cpp_typecheck_namespace.cpp index 618ab1ef4de..507024357e3 100644 --- a/src/cpp/cpp_typecheck_namespace.cpp +++ b/src/cpp/cpp_typecheck_namespace.cpp @@ -62,15 +62,10 @@ void cpp_typecheckt::convert(cpp_namespace_spect &namespace_spec) } else { - symbolt symbol; - - symbol.name=identifier; + symbolt symbol{identifier, typet(ID_namespace), ID_cpp}; symbol.base_name=final_name; - symbol.value.make_nil(); symbol.location=namespace_spec.source_location(); - symbol.mode=ID_cpp; symbol.module=module; - symbol.type=typet(ID_namespace); if(!symbol_table.insert(std::move(symbol)).second) { diff --git a/src/cpp/cpp_typecheck_template.cpp b/src/cpp/cpp_typecheck_template.cpp index fe42ae549a7..3ade4c59235 100644 --- a/src/cpp/cpp_typecheck_template.cpp +++ b/src/cpp/cpp_typecheck_template.cpp @@ -166,15 +166,11 @@ void cpp_typecheckt::typecheck_class_template( // it's not there yet - symbolt symbol; - - symbol.name=symbol_name; + symbolt symbol{symbol_name, typet{}, ID_cpp}; symbol.base_name=base_name; symbol.location=cpp_name.source_location(); - symbol.mode=ID_cpp; symbol.module=module; symbol.type.swap(declaration); - symbol.is_macro=false; symbol.value = exprt(ID_template_decls); symbol.pretty_name= @@ -274,14 +270,10 @@ void cpp_typecheckt::typecheck_function_template( return; } - symbolt symbol; - symbol.name=symbol_name; + symbolt symbol{symbol_name, typet{}, ID_cpp}; symbol.base_name=base_name; symbol.location=cpp_name.source_location(); - symbol.mode=ID_cpp; symbol.module=module; - symbol.value.make_nil(); - symbol.type.swap(declaration); symbol.pretty_name= cpp_scopes.current_scope().prefix+id2string(symbol.base_name); diff --git a/src/cpp/cpp_typecheck_virtual_table.cpp b/src/cpp/cpp_typecheck_virtual_table.cpp index 58c5f79056e..7d01484afae 100644 --- a/src/cpp/cpp_typecheck_virtual_table.cpp +++ b/src/cpp/cpp_typecheck_virtual_table.cpp @@ -68,15 +68,14 @@ void cpp_typecheckt::do_virtual_table(const symbolt &symbol) const symbolt &vt_symb_type = lookup("virtual_table::" + id2string(late_cast_symb.name)); - symbolt vt_symb_var; - vt_symb_var.name= - id2string(vt_symb_type.name) + "@"+ id2string(symbol.name); + symbolt vt_symb_var{ + id2string(vt_symb_type.name) + "@" + id2string(symbol.name), + struct_tag_typet(vt_symb_type.name), + symbol.mode}; vt_symb_var.base_name= id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name); - vt_symb_var.mode = symbol.mode; vt_symb_var.module=module; vt_symb_var.location=vt_symb_type.location; - vt_symb_var.type = struct_tag_typet(vt_symb_type.name); vt_symb_var.is_lvalue=true; vt_symb_var.is_static_lifetime=true; diff --git a/src/goto-cc/linker_script_merge.cpp b/src/goto-cc/linker_script_merge.cpp index 102ce688d3c..538c9aab0eb 100644 --- a/src/goto-cc/linker_script_merge.cpp +++ b/src/goto-cc/linker_script_merge.cpp @@ -461,12 +461,10 @@ int linker_script_merget::ls_data2instructions( CHECK_RETURN(zi.has_value()); // Add the array to the symbol table. - symbolt array_sym; + symbolt array_sym{array_name.str(), array_type, ID_C}; array_sym.is_static_lifetime = true; array_sym.is_lvalue = true; array_sym.is_state_var = true; - array_sym.name = array_name.str(); - array_sym.type = array_type; array_sym.value = *zi; array_sym.location = array_loc; @@ -478,12 +476,10 @@ int linker_script_merget::ls_data2instructions( address_of_exprt array_start(zero_idx); // Linker-defined symbol_exprt pointing to start address - symbolt start_sym; + symbolt start_sym{d["start-symbol"].value, pointer_type(char_type()), ID_C}; start_sym.is_static_lifetime = true; start_sym.is_lvalue = true; start_sym.is_state_var = true; - start_sym.name = d["start-symbol"].value; - start_sym.type = pointer_type(char_type()); start_sym.value = array_start; linker_values.emplace( d["start-symbol"].value, @@ -521,12 +517,10 @@ int linker_script_merget::ls_data2instructions( { plus_exprt array_end(array_start, array_size_expr); - symbolt end_sym; + symbolt end_sym{d["end-symbol"].value, pointer_type(char_type()), ID_C}; end_sym.is_static_lifetime = true; end_sym.is_lvalue = true; end_sym.is_state_var = true; - end_sym.name = d["end-symbol"].value; - end_sym.type = pointer_type(char_type()); end_sym.value = array_end; linker_values.emplace( d["end-symbol"].value, @@ -639,12 +633,11 @@ int linker_script_merget::ls_data2instructions( if(!symbol_table.has_symbol(CPROVER_PREFIX "allocated_memory")) { - symbolt sym; - sym.name=CPROVER_PREFIX "allocated_memory"; - sym.pretty_name=CPROVER_PREFIX "allocated_memory"; + symbolt sym{ + CPROVER_PREFIX "allocated_memory", + code_typet({}, empty_typet()), + ID_C} sym.pretty_name = CPROVER_PREFIX "allocated_memory"; sym.is_lvalue=sym.is_static_lifetime=true; - const code_typet void_t({}, empty_typet()); - sym.type=void_t; symbol_table.add(sym); } diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index 3c7105eca09..e45f5c5856f 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -405,14 +405,13 @@ void memory_snapshot_harness_generatort::generate( // Create harness function symbol - symbolt harness_function_symbol; - harness_function_symbol.name = harness_function_name; + symbolt harness_function_symbol{ + harness_function_name, + code_typet({}, empty_typet()), + called_function_symbol->mode}; harness_function_symbol.base_name = harness_function_name; harness_function_symbol.pretty_name = harness_function_name; - harness_function_symbol.is_lvalue = true; - harness_function_symbol.mode = called_function_symbol->mode; - harness_function_symbol.type = code_typet({}, empty_typet()); harness_function_symbol.value = harness_function_body; // Add harness function to goto model and symbol table diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 32deef9090f..28e86da5832 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -377,12 +377,13 @@ symbol_exprt recursive_initializationt::get_malloc_function() auto malloc_sym = goto_model.symbol_table.lookup("malloc"); if(malloc_sym == nullptr) { - symbolt new_malloc_sym; - new_malloc_sym.type = code_typet{code_typet{ - {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}}; - new_malloc_sym.name = new_malloc_sym.pretty_name = - new_malloc_sym.base_name = "malloc"; - new_malloc_sym.mode = initialization_config.mode; + symbolt new_malloc_sym{ + "malloc", + code_typet{ + {code_typet::parametert{size_type()}}, pointer_type(empty_typet{})}, + initialization_config.mode}; + new_malloc_sym.pretty_name = "malloc"; + new_malloc_sym.base_name = "malloc"; goto_model.symbol_table.insert(new_malloc_sym); return new_malloc_sym.symbol_expr(); } @@ -634,12 +635,13 @@ symbol_exprt recursive_initializationt::get_free_function() auto free_sym = goto_model.symbol_table.lookup("free"); if(free_sym == nullptr) { - symbolt new_free_sym; - new_free_sym.type = code_typet{code_typet{ - {code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}}}; - new_free_sym.name = new_free_sym.pretty_name = new_free_sym.base_name = - "free"; - new_free_sym.mode = initialization_config.mode; + symbolt new_free_sym{ + "free", + code_typet{ + {code_typet::parametert{pointer_type(empty_typet{})}}, empty_typet{}}, + initialization_config.mode}; + new_free_sym.pretty_name = "free"; + new_free_sym.base_name = "free"; goto_model.symbol_table.insert(new_free_sym); return new_free_sym.symbol_expr(); } diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index fd36f38002f..9fbeaa5875b 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -435,12 +435,10 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator) symbolt acceleratet::make_symbol(std::string name, typet type) { - symbolt ret; + symbolt ret{name, std::move(type), irep_idt{}}; ret.module="accelerate"; - ret.name=name; ret.base_name=name; ret.pretty_name=name; - ret.type=type; symbol_table.add(ret); diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 4e259682646..95353a09ca8 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -1248,12 +1248,10 @@ symbolt acceleration_utilst::fresh_symbol(std::string base, typet type) static int num_symbols=0; std::string name=base + "_" + std::to_string(num_symbols++); - symbolt ret; + symbolt ret{name, std::move(type), irep_idt{}}; ret.module="scratch"; - ret.name=name; ret.base_name=name; ret.pretty_name=name; - ret.type=type; symbol_table.add(ret); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index d7155de2e44..2268f74b90b 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1159,12 +1159,14 @@ void code_contractst::enforce_contract(const irep_idt &function) goto_functions.function_map.erase(old_function); // Place a new symbol with the mangled name into the symbol table - symbolt mangled_sym; + source_locationt sl; + sl.set_file("instrumented for code contracts"); + sl.set_line("0"); const symbolt *original_sym = symbol_table.lookup(original); - mangled_sym = *original_sym; + symbolt mangled_sym = *original_sym; mangled_sym.name = mangled; mangled_sym.base_name = mangled; - mangled_sym.location = original_sym->location; + mangled_sym.location = sl; const auto mangled_found = symbol_table.insert(std::move(mangled_sym)); INVARIANT( mangled_found.second, diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 1c5f7f61d0e..bcb3d40e728 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -91,14 +91,14 @@ void dump_ct::operator()(std::ostream &os) (symbol.type.id() == ID_union || symbol.type.id() == ID_struct) && !symbol.is_type) { - type_symbolt ts{symbol.type}; - ts.mode = symbol.mode; + std::string tag_name; if(mode == ID_C) - ts.name = "tag-" + type2name(symbol.type, ns); + tag_name = "tag-" + type2name(symbol.type, ns); else if(mode == ID_cpp) - ts.name = "tag-" + cpp_type2name(symbol.type); + tag_name = "tag-" + cpp_type2name(symbol.type); else UNREACHABLE; + type_symbolt ts{tag_name, symbol.type, symbol.mode}; typet &type = copied_symbol_table.get_writeable_ref(named_symbol.first).type; if(ts.type.id() == ID_union) diff --git a/src/goto-instrument/function.cpp b/src/goto-instrument/function.cpp index b47523913da..575c7a5c3de 100644 --- a/src/goto-instrument/function.cpp +++ b/src/goto-instrument/function.cpp @@ -32,21 +32,25 @@ code_function_callt function_to_call( if(s_it==symbol_table.symbols.end()) { + // This has to be dead code: a symbol table must contain all functions that + // appear in goto_functions. + UNREACHABLE; +#if 0 + // not there auto p = pointer_type(char_type()); p.base_type().set(ID_C_constant, true); const code_typet function_type({code_typet::parametert(p)}, empty_typet()); - symbolt new_symbol; - new_symbol.name=id; + symbolt new_symbol{id, function_type, irep_idt{}}; new_symbol.base_name=id; - new_symbol.type=function_type; symbol_table.insert(std::move(new_symbol)); s_it=symbol_table.symbols.find(id); assert(s_it!=symbol_table.symbols.end()); +#endif } // signature is expected to be diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 7abbaa56c0b..1e579669da8 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -1868,10 +1868,8 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast) base_name="nondet_"+std::to_string(count); } - symbolt symbol; + symbolt symbol{base_name, code_typet({}, expr.type()), ID_C}; symbol.base_name=base_name; - symbol.name=base_name; - symbol.type = code_typet({}, expr.type()); id=symbol.name; symbol_table.insert(std::move(symbol)); diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 570e41eddf5..85bc08ff0f1 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -76,10 +76,9 @@ const symbolt &w_guardst::get_guard_symbol(const irep_idt &object) w_guards.push_back(identifier); - symbolt new_symbol; - new_symbol.name=identifier; + symbolt new_symbol{ + identifier, bool_typet(), symbol_table.lookup_ref(object).mode}; new_symbol.base_name=identifier; - new_symbol.type=bool_typet(); new_symbol.is_static_lifetime=true; new_symbol.value=false_exprt(); diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp index 694792a4d47..05535c6fae2 100644 --- a/src/goto-instrument/stack_depth.cpp +++ b/src/goto-instrument/stack_depth.cpp @@ -29,14 +29,11 @@ static symbol_exprt add_stack_depth_symbol( const irep_idt identifier="$stack_depth"; typet type = size_type(); - symbolt new_symbol; - new_symbol.name=identifier; + symbolt new_symbol{identifier, type, ID_C}; new_symbol.base_name=identifier; new_symbol.pretty_name=identifier; - new_symbol.type=type; new_symbol.is_static_lifetime=true; new_symbol.value=from_integer(0, type); - new_symbol.mode=ID_C; new_symbol.is_thread_local=true; new_symbol.is_lvalue=true; diff --git a/src/goto-instrument/uninitialized.cpp b/src/goto-instrument/uninitialized.cpp index 2d4cb16f675..6764aba1bee 100644 --- a/src/goto-instrument/uninitialized.cpp +++ b/src/goto-instrument/uninitialized.cpp @@ -80,15 +80,12 @@ void uninitializedt::add_assertions( { const symbolt &symbol=ns.lookup(*it); - symbolt new_symbol; - new_symbol.name=id2string(symbol.name)+"#initialized"; - new_symbol.type=bool_typet(); + symbolt new_symbol{ + id2string(symbol.name) + "#initialized", bool_typet(), symbol.mode}; new_symbol.base_name=id2string(symbol.base_name)+"#initialized"; new_symbol.location=symbol.location; - new_symbol.mode=symbol.mode; new_symbol.module=symbol.module; new_symbol.is_thread_local=true; - new_symbol.is_static_lifetime=false; new_symbol.is_file_local=true; new_symbol.is_lvalue=true; diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 6d97ef14ad0..7e3c5ff5dd4 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -1480,10 +1480,8 @@ void goto_convertt::do_function_call_symbol( if(!symbol_table.has_symbol(name)) { - symbolt new_symbol; + symbolt new_symbol{name, f_type, mode}; new_symbol.base_name=name; - new_symbol.name=name; - new_symbol.type=f_type; new_symbol.location=function.source_location(); symbol_table.add(new_symbol); } diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index c1d86ba1367..f6b0a7a3608 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -242,14 +242,10 @@ symbol_exprt goto_convertt::exception_flag(const irep_idt &mode) if(s_it==symbol_table.symbols.end()) { - symbolt new_symbol; + symbolt new_symbol{id, bool_typet{}, mode}; new_symbol.base_name="$exception_flag"; - new_symbol.name=id; new_symbol.is_lvalue=true; new_symbol.is_thread_local=true; - new_symbol.is_file_local=false; - new_symbol.type=bool_typet(); - new_symbol.mode = mode; symbol_table.insert(std::move(new_symbol)); } diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h index df206bfbb63..ff278d7e5cf 100644 --- a/src/goto-programs/name_mangler.h +++ b/src/goto-programs/name_mangler.h @@ -67,8 +67,7 @@ class function_name_manglert continue; const irep_idt mangled = mangle_fun(sym, extra_info); - symbolt new_sym; - new_sym = sym; + symbolt new_sym = sym; new_sym.name = mangled; new_sym.base_name = mangled; if(new_sym.pretty_name.empty()) diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 686885fc47c..fdf55651e30 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -732,26 +732,20 @@ void string_instrumentationt::do_strerror( if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end()) { - symbolt new_symbol_size; - new_symbol_size.base_name="__strerror_buffer_size"; + symbolt new_symbol_size{identifier_size, size_type(), ID_C}; + new_symbol_size.base_name = identifier_size; new_symbol_size.pretty_name=new_symbol_size.base_name; - new_symbol_size.name=identifier_size; - new_symbol_size.mode=ID_C; - new_symbol_size.type=size_type(); new_symbol_size.is_state_var=true; new_symbol_size.is_lvalue=true; new_symbol_size.is_static_lifetime=true; array_typet type(char_type(), new_symbol_size.symbol_expr()); - symbolt new_symbol_buf; - new_symbol_buf.mode=ID_C; - new_symbol_buf.type=type; + symbolt new_symbol_buf{identifier_buf, type, ID_C}; new_symbol_buf.is_state_var=true; new_symbol_buf.is_lvalue=true; new_symbol_buf.is_static_lifetime=true; - new_symbol_buf.base_name="__strerror_buffer"; + new_symbol_buf.base_name = identifier_buf; new_symbol_buf.pretty_name=new_symbol_buf.base_name; - new_symbol_buf.name=new_symbol_buf.base_name; symbol_table.insert(std::move(new_symbol_buf)); symbol_table.insert(std::move(new_symbol_size)); @@ -812,12 +806,9 @@ void string_instrumentationt::invalidate_buffer( if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end()) { - symbolt new_symbol; + symbolt new_symbol{cntr_id, size_type(), ID_C}; new_symbol.base_name="$counter"; new_symbol.pretty_name=new_symbol.base_name; - new_symbol.name=cntr_id; - new_symbol.mode=ID_C; - new_symbol.type=size_type(); new_symbol.is_state_var=true; new_symbol.is_lvalue=true; new_symbol.is_static_lifetime=true; diff --git a/src/pointer-analysis/add_failed_symbols.cpp b/src/pointer-analysis/add_failed_symbols.cpp index 659cd611e34..66f0739b902 100644 --- a/src/pointer-analysis/add_failed_symbols.cpp +++ b/src/pointer-analysis/add_failed_symbols.cpp @@ -36,14 +36,13 @@ void add_failed_symbol(symbolt &symbol, symbol_table_baset &symbol_table) { if(symbol.type.id()==ID_pointer) { - symbolt new_symbol; + symbolt new_symbol{ + failed_symbol_id(symbol.name), + to_pointer_type(symbol.type).base_type(), + symbol.mode}; new_symbol.is_lvalue=true; new_symbol.module=symbol.module; - new_symbol.mode=symbol.mode; new_symbol.base_name=failed_symbol_id(symbol.base_name); - new_symbol.name=failed_symbol_id(symbol.name); - new_symbol.type = to_pointer_type(symbol.type).base_type(); - new_symbol.value.make_nil(); new_symbol.type.set(ID_C_is_failed_symbol, true); symbol.type.set(ID_C_failed_symbol, new_symbol.name); diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 8b8990e6e0f..7bb7b1b1cef 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -103,13 +103,11 @@ static void add_main_function_block_call( PRECONDITION(1u == function_type.parameters().size()); const code_typet::parametert &data_block_interface = function_type.parameters().front(); - symbolt instance_data_block; - instance_data_block.name = - id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX; - instance_data_block.type = - to_type_with_subtype(data_block_interface.type()).subtype(); + symbolt instance_data_block{ + id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX, + to_type_with_subtype(data_block_interface.type()).subtype(), + ID_statement_list}; instance_data_block.is_static_lifetime = true; - instance_data_block.mode = ID_statement_list; symbol_table.add(instance_data_block); const address_of_exprt data_block_ref{instance_data_block.symbol_expr()}; @@ -124,10 +122,8 @@ static void add_main_function_block_call( static void generate_statement_list_init_function(symbol_table_baset &symbol_table) { - symbolt init; - init.name = INITIALIZE_FUNCTION; - init.mode = ID_statement_list; - init.type = code_typet({}, empty_typet{}); + symbolt init{ + INITIALIZE_FUNCTION, code_typet({}, empty_typet{}), ID_statement_list}; code_blockt dest; dest.add(code_labelt(CPROVER_HIDE, code_skipt())); @@ -146,9 +142,7 @@ generate_statement_list_init_function(symbol_table_baset &symbol_table) /// \param [out] symbol_table: Symbol table that should contain the symbol. static void generate_rounding_mode(symbol_table_baset &symbol_table) { - symbolt rounding_mode; - rounding_mode.name = rounding_mode_identifier(); - rounding_mode.type = signed_int_type(); + symbolt rounding_mode{rounding_mode_identifier(), signed_int_type(), ID_C}; rounding_mode.is_thread_local = true; rounding_mode.is_static_lifetime = true; const constant_exprt rounding_val{ @@ -179,12 +173,10 @@ bool generate_statement_list_start_function( add_main_function_block_call(start_function_body, symbol_table, main); // Add the start symbol. - symbolt start_symbol; - start_symbol.name = goto_functionst::entry_point(); + symbolt start_symbol{ + goto_functionst::entry_point(), code_typet{{}, empty_typet{}}, main.mode}; start_symbol.base_name = goto_functionst::entry_point(); - start_symbol.type = code_typet({}, empty_typet{}); start_symbol.value.swap(start_function_body); - start_symbol.mode = main.mode; if(!symbol_table.insert(std::move(start_symbol)).second) { diff --git a/src/statement-list/statement_list_typecheck.cpp b/src/statement-list/statement_list_typecheck.cpp index 09604809f14..e91f45ba535 100644 --- a/src/statement-list/statement_list_typecheck.cpp +++ b/src/statement-list/statement_list_typecheck.cpp @@ -158,12 +158,10 @@ void statement_list_typecheckt::typecheck_function_block_declaration( const statement_list_parse_treet::function_blockt &function_block) { // Create FB symbol. - symbolt function_block_sym; + symbolt function_block_sym{function_block.name, typet{}, ID_statement_list}; function_block_sym.module = module; - function_block_sym.name = function_block.name; function_block_sym.base_name = function_block_sym.name; function_block_sym.pretty_name = function_block_sym.name; - function_block_sym.mode = ID_statement_list; // When calling function blocks, the passed parameters are value-copied to a // corresponding instance data block. This block contains all input, inout, @@ -175,11 +173,11 @@ void statement_list_typecheckt::typecheck_function_block_declaration( // Create and add DB type symbol. const struct_typet data_block_type{ create_instance_data_block_type(function_block)}; - type_symbolt data_block{data_block_type}; - data_block.name = - id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX; + type_symbolt data_block{ + id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX, + data_block_type, + ID_statement_list}; data_block.base_name = data_block.name; - data_block.mode = ID_statement_list; symbol_table.add(data_block); // Create and add parameter symbol. @@ -206,12 +204,10 @@ void statement_list_typecheckt::typecheck_function_block_declaration( void statement_list_typecheckt::typecheck_function_declaration( const statement_list_parse_treet::functiont &function) { - symbolt function_sym; + symbolt function_sym{function.name, typet{}, ID_statement_list}; function_sym.module = module; - function_sym.name = function.name; function_sym.base_name = function_sym.name; function_sym.pretty_name = function_sym.name; - function_sym.mode = ID_statement_list; code_typet::parameterst params; typecheck_function_var_decls( function.var_input, params, function.name, ID_statement_list_var_input); @@ -230,28 +226,22 @@ void statement_list_typecheckt::typecheck_tag_list() { for(const symbol_exprt &tag : parse_tree.tags) { - symbolt tag_sym; + symbolt tag_sym{tag.get_identifier(), tag.type(), ID_statement_list}; tag_sym.is_static_lifetime = true; tag_sym.module = module; - tag_sym.name = tag.get_identifier(); tag_sym.base_name = tag_sym.name; tag_sym.pretty_name = tag_sym.name; - tag_sym.type = tag.type(); - tag_sym.mode = ID_statement_list; symbol_table.add(tag_sym); } } void statement_list_typecheckt::add_temp_rlo() { - symbolt temp_rlo; + symbolt temp_rlo{CPROVER_TEMP_RLO, get_bool_type(), ID_statement_list}; temp_rlo.is_static_lifetime = true; temp_rlo.module = module; - temp_rlo.name = CPROVER_TEMP_RLO; temp_rlo.base_name = temp_rlo.name; temp_rlo.pretty_name = temp_rlo.name; - temp_rlo.type = get_bool_type(); - temp_rlo.mode = ID_statement_list; symbol_table.add(temp_rlo); } @@ -321,13 +311,13 @@ void statement_list_typecheckt::typecheck_temp_var_decls( for(const statement_list_parse_treet::var_declarationt &declaration : tia_module.var_temp) { - symbolt temp_sym; - temp_sym.name = id2string(tia_symbol.name) + - "::" + id2string(declaration.variable.get_identifier()); + symbolt temp_sym{ + id2string(tia_symbol.name) + + "::" + id2string(declaration.variable.get_identifier()), + declaration.variable.type(), + ID_statement_list}; temp_sym.base_name = declaration.variable.get_identifier(); temp_sym.pretty_name = temp_sym.base_name; - temp_sym.type = declaration.variable.type(); - temp_sym.mode = ID_statement_list; temp_sym.module = module; symbol_table.add(temp_sym); diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 4a1a2d390a0..8a3738b56c9 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -48,10 +48,9 @@ symbolt &get_fresh_aux_symbol( identifier = get_new_name(identifier, ns, '$'); std::string basename = id2string(identifier).substr(prefix_size); - auxiliary_symbolt new_symbol(basename, type); - new_symbol.name = identifier; + auxiliary_symbolt new_symbol(identifier, type, symbol_mode); + new_symbol.base_name = basename; new_symbol.location = source_location; - new_symbol.mode = symbol_mode; std::pair res = symbol_table.insert(std::move(new_symbol)); CHECK_RETURN(res.second); diff --git a/src/util/symbol.h b/src/util/symbol.h index d34c8351c43..09ae1a670dd 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -58,17 +58,39 @@ class symbolt } // global use - bool is_type, is_macro, is_exported, - is_input, is_output, is_state_var, is_property; + bool is_type = false; + bool is_macro = false; + bool is_exported = false; + bool is_input = false; + bool is_output = false; + bool is_state_var = false; + bool is_property = false; // ANSI-C - bool is_static_lifetime, is_thread_local; - bool is_lvalue, is_file_local, is_extern, is_volatile, - is_parameter, is_auxiliary, is_weak; + bool is_static_lifetime = false; + bool is_thread_local = false; + bool is_lvalue = false; + bool is_file_local = false; + bool is_extern = false; + bool is_volatile = false; + bool is_parameter = false; + bool is_auxiliary = false; + bool is_weak = false; symbolt() + : type(static_cast(get_nil_irep())), + value(static_cast(get_nil_irep())), + location(source_locationt::nil()) + { + } + + symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode) + : type(std::move(_type)), + value(static_cast(get_nil_irep())), + location(source_locationt::nil()), + name(_name), + mode(_mode) { - clear(); } /// Zero initialise a symbol object. @@ -132,10 +154,10 @@ std::ostream &operator<<(std::ostream &out, const symbolt &symbol); class type_symbolt:public symbolt { public: - explicit type_symbolt(const typet &_type) + type_symbolt(const irep_idt &_name, typet _type, const irep_idt &_mode) + : symbolt(_name, _type, _mode) { - type=_type; - is_type=true; + is_type = true; } }; @@ -155,12 +177,14 @@ class auxiliary_symbolt:public symbolt is_auxiliary=true; } - auxiliary_symbolt(const irep_idt &name, const typet &type): - auxiliary_symbolt() + auxiliary_symbolt(const irep_idt &name, typet type, const irep_idt &mode) + : symbolt(name, type, mode) { - this->name=name; - this->base_name=name; - this->type=type; + is_lvalue = true; + is_state_var = true; + is_thread_local = true; + is_file_local = true; + is_auxiliary = true; } }; diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp index bdec4ae5cfb..15d50d012e2 100644 --- a/unit/analyses/ai/ai.cpp +++ b/unit/analyses/ai/ai.cpp @@ -146,28 +146,16 @@ SCENARIO( // g: - symbolt gy; - gy.name = "gy"; - gy.mode = ID_C; - gy.type = signed_int_type(); - - symbolt g; - g.name = "g"; - g.mode = ID_C; - g.type = code_typet({}, empty_typet()); + symbolt gy{"gy", signed_int_type(), ID_C}; + + symbolt g{"g", code_typet({}, empty_typet()), ID_C}; g.value = code_assignt(gy.symbol_expr(), from_integer(0, signed_int_type())); // h: - symbolt hy; - hy.name = "hy"; - hy.mode = ID_C; - hy.type = signed_int_type(); + symbolt hy{"hy", signed_int_type(), ID_C}; - symbolt h; - h.name = "h"; - h.mode = ID_C; - h.type = code_typet({}, empty_typet()); + symbolt h{"h", code_typet({}, empty_typet()), ID_C}; h.value = code_assignt(hy.symbol_expr(), from_integer(0, signed_int_type())); goto_model.symbol_table.add(g); @@ -177,15 +165,9 @@ SCENARIO( // f: - symbolt x; - x.name = "x"; - x.mode = ID_C; - x.type = signed_int_type(); + symbolt x{"x", signed_int_type(), ID_C}; - symbolt y; - y.name = "y"; - y.mode = ID_C; - y.type = signed_int_type(); + symbolt y{"y", signed_int_type(), ID_C}; goto_model.symbol_table.add(x); goto_model.symbol_table.add(y); @@ -221,21 +203,16 @@ SCENARIO( f_body.copy_to_operands(make_void_call(g.symbol_expr())); - symbolt f; - f.name = "f"; - f.mode = ID_C; - f.type = code_typet({}, empty_typet()); + symbolt f{"f", code_typet({}, empty_typet()), ID_C}; f.value = f_body; goto_model.symbol_table.add(f); // __CPROVER_start: - symbolt start; - start.name = goto_functionst::entry_point(); + symbolt start{ + goto_functionst::entry_point(), code_typet{{}, empty_typet{}}, ID_C}; start.base_name = goto_functionst::entry_point(); - start.mode = ID_C; - start.type = code_typet({}, empty_typet()); start.value = make_void_call(f.symbol_expr()); goto_model.symbol_table.add(start); diff --git a/unit/analyses/constant_propagator.cpp b/unit/analyses/constant_propagator.cpp index 0b0ca0fec6b..36bd4ace8c0 100644 --- a/unit/analyses/constant_propagator.cpp +++ b/unit/analyses/constant_propagator.cpp @@ -36,14 +36,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") // int x = 1; // int y = 2; - symbolt local_x; - symbolt local_y; - local_x.name = "x"; - local_x.type = integer_typet(); - local_x.mode = ID_C; - local_y.name = "y"; - local_y.type = integer_typet(); - local_y.mode = ID_C; + symbolt local_x{"x", integer_typet(), ID_C}; + symbolt local_y{"y", integer_typet(), ID_C}; code_blockt code( {code_declt(local_x.symbol_expr()), @@ -53,11 +47,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") code_assignt( local_y.symbol_expr(), constant_exprt("2", integer_typet()))}); - symbolt main_function_symbol; - main_function_symbol.name = "main"; - main_function_symbol.type = code_typet({}, empty_typet()); + symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C}; main_function_symbol.value = code; - main_function_symbol.mode = ID_C; goto_model.symbol_table.add(local_x); goto_model.symbol_table.add(local_y); @@ -120,14 +111,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") goto_modelt goto_model; namespacet ns(goto_model.symbol_table); - symbolt bool_local; - symbolt c_bool_local; - bool_local.name = "bool_local"; - bool_local.type = bool_typet(); - bool_local.mode = ID_C; - c_bool_local.name = "c_bool_local"; - c_bool_local.type = c_bool_typet(8); - c_bool_local.mode = ID_C; + symbolt bool_local{"bool_local", bool_typet(), ID_C}; + symbolt c_bool_local{"c_bool_local", c_bool_typet(8), ID_C}; code_blockt code({code_declt(bool_local.symbol_expr()), code_declt(c_bool_local.symbol_expr())}); @@ -144,11 +129,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") code.add(std::move(bool_cond_block)); code.add(std::move(c_bool_cond_block)); - symbolt main_function_symbol; - main_function_symbol.name = "main"; - main_function_symbol.type = code_typet({}, empty_typet()); + symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C}; main_function_symbol.value = code; - main_function_symbol.mode = ID_C; goto_model.symbol_table.add(bool_local); goto_model.symbol_table.add(c_bool_local); @@ -216,19 +198,13 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") for(size_t i = 0; i < n_bool_locals; ++i) { - symbolt bool_local; - bool_local.name = "b" + std::to_string(i); - bool_local.type = bool_typet(); - bool_local.mode = ID_C; + symbolt bool_local{"b" + std::to_string(i), bool_typet(), ID_C}; bool_locals.push_back(bool_local); } for(size_t i = 0; i < n_c_bool_locals; ++i) { - symbolt c_bool_local; - c_bool_local.name = "cb" + std::to_string(i); - c_bool_local.type = c_bool_typet(8); - c_bool_local.mode = ID_C; + symbolt c_bool_local{"cb" + std::to_string(i), c_bool_typet(8), ID_C}; c_bool_locals.push_back(c_bool_local); } @@ -272,10 +248,7 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") const bool c_bool_expectations[n_c_bool_locals] = { true, true, true, false, false, true, false, true}; - symbolt marker_symbol; - marker_symbol.type = signedbv_typet(32); - marker_symbol.name = "marker"; - marker_symbol.mode = ID_C; + symbolt marker_symbol{"marker", signedbv_typet(32), ID_C}; codet program = code_assignt( marker_symbol.symbol_expr(), from_integer(1234, marker_symbol.type)); @@ -294,11 +267,8 @@ SCENARIO("constant_propagator", "[core][analyses][constant_propagator]") for(const symbolt &symbol : c_bool_locals) goto_model.symbol_table.add(symbol); - symbolt main_function_symbol; - main_function_symbol.name = "main"; - main_function_symbol.type = code_typet({}, empty_typet()); + symbolt main_function_symbol{"main", code_typet({}, empty_typet()), ID_C}; main_function_symbol.value = program; - main_function_symbol.mode = ID_C; goto_model.symbol_table.add(marker_symbol); goto_model.symbol_table.add(main_function_symbol); diff --git a/unit/analyses/dependence_graph.cpp b/unit/analyses/dependence_graph.cpp index d948598968d..19410bbb0bc 100644 --- a/unit/analyses/dependence_graph.cpp +++ b/unit/analyses/dependence_graph.cpp @@ -53,10 +53,9 @@ SCENARIO("dependence_graph", "[core][analyses][dependence_graph]") typet int_type = signed_int_type(); - symbolt x_symbol; - x_symbol.name = id2string(goto_functionst::entry_point()) + "::x"; + symbolt x_symbol{ + id2string(goto_functionst::entry_point()) + "::x", int_type, ID_C}; x_symbol.base_name = "x"; - x_symbol.type = int_type; x_symbol.is_lvalue = true; x_symbol.is_state_var = true; x_symbol.is_thread_local = true; diff --git a/unit/analyses/variable-sensitivity/eval.cpp b/unit/analyses/variable-sensitivity/eval.cpp index c6a99d6326f..15f50e48a36 100644 --- a/unit/analyses/variable-sensitivity/eval.cpp +++ b/unit/analyses/variable-sensitivity/eval.cpp @@ -14,9 +14,8 @@ static symbolt simple_symbol(const irep_idt &identifier, const typet &type) { - symbolt b1; - b1.name = b1.base_name = b1.pretty_name = identifier; - b1.type = type; + symbolt b1{identifier, type, irep_idt{}}; + b1.base_name = b1.pretty_name = identifier; return b1; } diff --git a/unit/goto-programs/goto_program_assume.cpp b/unit/goto-programs/goto_program_assume.cpp index dcdb959d321..2998f0a4103 100644 --- a/unit/goto-programs/goto_program_assume.cpp +++ b/unit/goto-programs/goto_program_assume.cpp @@ -23,13 +23,11 @@ SCENARIO( { symbol_tablet symbol_table; const typet type1 = signedbv_typet(32); - symbolt symbol; - symbolt fun_symbol; + symbolt symbol{"a", type1, ID_C}; irep_idt fun_name = "foo"; + symbolt fun_symbol; fun_symbol.name = fun_name; - irep_idt symbol_name = "a"; - symbol.name = symbol_name; - symbol_exprt varx(symbol_name, type1); + symbol_exprt varx = symbol.symbol_expr(); exprt val10 = from_integer(10, type1); binary_relation_exprt x_le_10(varx, ID_le, val10); @@ -37,7 +35,6 @@ SCENARIO( auto assertion = goto_function.body.add(goto_programt::make_assertion(x_le_10)); - symbol.type = type1; symbol_table.insert(symbol); symbol_table.insert(fun_symbol); namespacet ns(symbol_table); diff --git a/unit/goto-programs/goto_program_dead.cpp b/unit/goto-programs/goto_program_dead.cpp index 7abba241eea..9383dabbbb0 100644 --- a/unit/goto-programs/goto_program_dead.cpp +++ b/unit/goto-programs/goto_program_dead.cpp @@ -27,11 +27,8 @@ SCENARIO( irep_idt fun_name = "foo"; fun_symbol.name = fun_name; - symbolt var_symbol; - irep_idt var_symbol_name = "a"; - var_symbol.type = type1; - var_symbol.name = var_symbol_name; - symbol_exprt var_a(var_symbol_name, type1); + symbolt var_symbol{"a", type1, irep_idt{}}; + symbol_exprt var_a = var_symbol.symbol_expr(); goto_functiont goto_function; auto &instructions = goto_function.body.instructions; diff --git a/unit/goto-programs/goto_program_declaration.cpp b/unit/goto-programs/goto_program_declaration.cpp index 7a16550a5cc..38ae8e93183 100644 --- a/unit/goto-programs/goto_program_declaration.cpp +++ b/unit/goto-programs/goto_program_declaration.cpp @@ -27,11 +27,8 @@ SCENARIO( irep_idt fun_name = "foo"; fun_symbol.name = fun_name; - symbolt var_symbol; - irep_idt var_symbol_name = "a"; - var_symbol.type = type1; - var_symbol.name = var_symbol_name; - symbol_exprt var_a(var_symbol_name, type1); + symbolt var_symbol{"a", type1, irep_idt{}}; + symbol_exprt var_a = var_symbol.symbol_expr(); goto_functiont goto_function; goto_function.body.add(goto_programt::make_decl(var_a)); diff --git a/unit/goto-programs/goto_program_function_call.cpp b/unit/goto-programs/goto_program_function_call.cpp index 14256a01ddd..0d1d898bd39 100644 --- a/unit/goto-programs/goto_program_function_call.cpp +++ b/unit/goto-programs/goto_program_function_call.cpp @@ -25,28 +25,19 @@ SCENARIO( const signedbv_typet type2(64); const code_typet code_type({}, type1); - symbolt var_symbol; - irep_idt var_symbol_name = "a"; - var_symbol.name = var_symbol_name; - symbol_exprt var_a(var_symbol_name, type1); - - symbolt var_symbol2; - irep_idt var_symbol_name2 = "b"; - var_symbol2.name = var_symbol_name2; - symbol_exprt var_b(var_symbol_name2, type2); - - symbolt fun_symbol; - irep_idt fun_symbol_name = "foo"; - fun_symbol.name = fun_symbol_name; - fun_symbol.type = code_type; - symbol_exprt fun_foo(fun_symbol_name, code_type); + symbolt var_symbol{"a", type1, irep_idt{}}; + symbol_exprt var_a = var_symbol.symbol_expr(); + + symbolt var_symbol2{"b", type2, irep_idt{}}; + symbol_exprt var_b = var_symbol2.symbol_expr(); + + symbolt fun_symbol{"foo", code_type, irep_idt{}}; + symbol_exprt fun_foo = fun_symbol.symbol_expr(); goto_functiont goto_function; auto &instructions = goto_function.body.instructions; instructions.emplace_back(goto_program_instruction_typet::FUNCTION_CALL); - var_symbol.type = type1; - var_symbol2.type = type2; symbol_table.insert(var_symbol); symbol_table.insert(var_symbol2); symbol_table.insert(fun_symbol); diff --git a/unit/goto-programs/goto_program_goto_target.cpp b/unit/goto-programs/goto_program_goto_target.cpp index d46a66b42c2..dce68a4c5a6 100644 --- a/unit/goto-programs/goto_program_goto_target.cpp +++ b/unit/goto-programs/goto_program_goto_target.cpp @@ -27,10 +27,8 @@ SCENARIO( irep_idt fun_name = "foo"; fun_symbol.name = fun_name; - symbolt symbol; - irep_idt symbol_name = "a"; - symbol.name = symbol_name; - symbol_exprt varx(symbol_name, type1); + symbolt symbol{"a", type1, irep_idt{}}; + symbol_exprt varx = symbol.symbol_expr(); exprt val10 = from_integer(10, type1); binary_relation_exprt x_le_10(varx, ID_le, val10); @@ -41,7 +39,6 @@ SCENARIO( instructions.emplace_back( goto_programt::make_goto(instructions.begin(), true_exprt())); - symbol.type = type1; symbol_table.insert(symbol); symbol_table.insert(fun_symbol); namespacet ns(symbol_table); diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index 7c1b4f88eec..cba68ed1d56 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -28,60 +28,38 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") goto_modelt goto_model; // void f(){int x = 1;} - symbolt x; - x.name = "x"; - x.mode = ID_C; - x.type = signed_int_type(); + symbolt x{"x", signed_int_type(), ID_C}; goto_model.symbol_table.add(x); - symbolt f; - f.name = "f"; - f.mode = ID_C; - f.type = code_typet({}, empty_typet()); // void rtn, take no params + // void rtn, take no params + symbolt f{"f", code_typet({}, empty_typet()), ID_C}; code_blockt f_body{ {code_declt(x.symbol_expr()), code_assignt(x.symbol_expr(), from_integer(1, signed_int_type()))}}; - f.value = f_body; goto_model.symbol_table.add(f); // void g(){int y = 2;} - symbolt y; - y.name = "y"; - y.mode = ID_C; - y.type = signed_int_type(); + symbolt y{"y", signed_int_type(), ID_C}; goto_model.symbol_table.add(y); - symbolt g; - g.name = "g"; - g.mode = ID_C; - g.type = code_typet({}, empty_typet()); - + symbolt g{"g", code_typet({}, empty_typet()), ID_C}; code_blockt g_body{ {code_declt{y.symbol_expr()}, code_assignt{y.symbol_expr(), from_integer(2, signed_int_type())}}}; - g.value = g_body; goto_model.symbol_table.add(g); - symbolt z; - z.name = "z"; - z.mode = ID_C; - z.type = signed_int_type(); + symbolt z{"z", signed_int_type(), ID_C}; goto_model.symbol_table.add(z); - symbolt fn_ptr; - fn_ptr.name = "fn_ptr"; - fn_ptr.mode = ID_C; - // pointer to fn call - fn_ptr.type = pointer_typet(code_typet{{}, empty_typet()}, 64); + symbolt fn_ptr{ + "fn_ptr", pointer_typet(code_typet{{}, empty_typet()}, 64), ID_C}; goto_model.symbol_table.add(fn_ptr); - symbolt entry_point; - entry_point.name = goto_functionst::entry_point(); - entry_point.mode = ID_C; - entry_point.type = code_typet({}, empty_typet{}); + symbolt entry_point{ + goto_functionst::entry_point(), code_typet({}, empty_typet{}), ID_C}; code_blockt entry_point_body{ {code_declt{z.symbol_expr()}, code_assignt{z.symbol_expr(), from_integer(3, signed_int_type())}, diff --git a/unit/goto-programs/remove_returns.cpp b/unit/goto-programs/remove_returns.cpp index bc9d37b24c3..a56b5a4d701 100644 --- a/unit/goto-programs/remove_returns.cpp +++ b/unit/goto-programs/remove_returns.cpp @@ -20,11 +20,9 @@ Author: Diffblue Ltd. TEST_CASE("Return-value removal", "[core][goto-programs][remove_returns]") { symbol_tablet symbol_table; - symbolt function_symbol; - function_symbol.name = "a"; + symbolt function_symbol{"a", code_typet({}, signedbv_typet(32)), irep_idt{}}; function_symbol.pretty_name = "a"; function_symbol.base_name = "a"; - function_symbol.type = code_typet({}, signedbv_typet(32)); symbol_table.add(function_symbol); @@ -50,14 +48,12 @@ TEST_CASE( symbol_tablet symbol_table; goto_functionst goto_functions; - symbolt foo_function_symbol; - foo_function_symbol.name = "foo_function"; - foo_function_symbol.type = code_typet{{}, empty_typet{}}; + symbolt foo_function_symbol{ + "foo_function", code_typet{{}, empty_typet{}}, irep_idt{}}; symbol_table.insert(foo_function_symbol); - symbolt bar_function_symbol; - bar_function_symbol.name = "bar_function"; - bar_function_symbol.type = code_typet{{}, signedbv_typet{32}}; + symbolt bar_function_symbol{ + "bar_function", code_typet{{}, signedbv_typet{32}}, irep_idt{}}; symbol_table.insert(bar_function_symbol); *goto_functions.function_map["foo_function"].body.add_instruction() = diff --git a/unit/goto-symex/apply_condition.cpp b/unit/goto-symex/apply_condition.cpp index ff843e99a34..e666c4ff2c9 100644 --- a/unit/goto-symex/apply_condition.cpp +++ b/unit/goto-symex/apply_condition.cpp @@ -17,9 +17,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol; - symbol.name = symbol_expr.get_identifier(); - symbol.type = symbol_expr.type(); + symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 1935d184cfb..438e13c0eb2 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -19,9 +19,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol; - symbol.name = symbol_expr.get_identifier(); - symbol.type = symbol_expr.type(); + symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index aa2395be29b..e5c69966cf0 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -26,9 +26,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol; - symbol.name = symbol_expr.get_identifier(); - symbol.type = symbol_expr.type(); + symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/goto-symex/symex_level0.cpp b/unit/goto-symex/symex_level0.cpp index 901f523f161..b60e50eaad5 100644 --- a/unit/goto-symex/symex_level0.cpp +++ b/unit/goto-symex/symex_level0.cpp @@ -28,9 +28,8 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") const symbol_exprt symbol_nonshared{"nonShared", int_type}; const ssa_exprt ssa_nonshared{symbol_nonshared}; symbol_table.insert([&] { - symbolt symbol; - symbol.name = symbol_nonshared.get_identifier(); - symbol.type = symbol_nonshared.type(); + symbolt symbol{ + symbol_nonshared.get_identifier(), symbol_nonshared.type(), irep_idt{}}; symbol.value = symbol_nonshared; symbol.is_thread_local = true; return symbol; @@ -39,9 +38,8 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") const symbol_exprt symbol_shared{"shared", int_type}; const ssa_exprt ssa_shared{symbol_shared}; symbol_table.insert([&] { - symbolt symbol; - symbol.name = symbol_shared.get_identifier(); - symbol.type = symbol_shared.type(); + symbolt symbol{ + symbol_shared.get_identifier(), symbol_shared.type(), irep_idt{}}; symbol.value = symbol_shared; symbol.is_thread_local = false; return symbol; @@ -51,9 +49,8 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") bool_typet{}}; const ssa_exprt ssa_guard{symbol_guard}; symbol_table.insert([&] { - symbolt symbol; - symbol.name = symbol_guard.get_identifier(); - symbol.type = symbol_guard.type(); + symbolt symbol{ + symbol_guard.get_identifier(), symbol_guard.type(), irep_idt{}}; symbol.value = symbol_guard; symbol.is_thread_local = false; return symbol; @@ -63,9 +60,8 @@ SCENARIO("Level 0 renaming", "[core][goto-symex][symex-level0]") const symbol_exprt symbol_fun{"fun", code_type}; const ssa_exprt ssa_fun{symbol_fun}; symbol_table.insert([&] { - symbolt fun_symbol; - fun_symbol.name = symbol_fun.get_identifier(); - fun_symbol.type = symbol_fun.type(); + symbolt fun_symbol{ + symbol_fun.get_identifier(), symbol_fun.type(), irep_idt{}}; fun_symbol.value = symbol_fun; fun_symbol.is_thread_local = true; return fun_symbol; diff --git a/unit/goto-symex/symex_level1.cpp b/unit/goto-symex/symex_level1.cpp index f298f3408a1..27a783ba537 100644 --- a/unit/goto-symex/symex_level1.cpp +++ b/unit/goto-symex/symex_level1.cpp @@ -25,9 +25,8 @@ SCENARIO("Level 1 renaming", "[core][goto-symex][symex-level1]") const symbol_exprt symbol_nonshared{"foo", int_type}; ssa_exprt ssa{symbol_nonshared}; symbol_table.insert([&] { - symbolt symbol; - symbol.name = symbol_nonshared.get_identifier(); - symbol.type = symbol_nonshared.type(); + symbolt symbol{ + symbol_nonshared.get_identifier(), symbol_nonshared.type(), irep_idt{}}; symbol.value = symbol_nonshared; symbol.is_thread_local = true; return symbol; diff --git a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp index 3b3f5d28509..4ca9cb1a572 100644 --- a/unit/goto-symex/try_evaluate_pointer_comparisons.cpp +++ b/unit/goto-symex/try_evaluate_pointer_comparisons.cpp @@ -16,9 +16,7 @@ static void add_to_symbol_table( symbol_tablet &symbol_table, const symbol_exprt &symbol_expr) { - symbolt symbol; - symbol.name = symbol_expr.get_identifier(); - symbol.type = symbol_expr.type(); + symbolt symbol{symbol_expr.get_identifier(), symbol_expr.type(), irep_idt{}}; symbol.value = symbol_expr; symbol.is_thread_local = true; symbol_table.insert(symbol); diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index d946d6c8701..81dafd11518 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -62,8 +62,7 @@ SCENARIO( A_y.set_base_name("y"); A_y.set_pretty_name("y"); - type_symbolt A_symbol(struct_A); - A_symbol.name = "A"; + type_symbolt A_symbol{"A", struct_A, irep_idt{}}; A_symbol.base_name = "A"; A_symbol.pretty_name = "A"; @@ -71,27 +70,21 @@ SCENARIO( // Create global symbols struct A a1, a2, a3; - symbolt a1_symbol; - a1_symbol.name = "a1"; + symbolt a1_symbol{"a1", struct_tag_typet(A_symbol.name), irep_idt{}}; a1_symbol.base_name = "a1"; a1_symbol.pretty_name = "a1"; - a1_symbol.type = struct_tag_typet(A_symbol.name); a1_symbol.is_static_lifetime = true; symbol_table.add(a1_symbol); - symbolt a2_symbol; - a2_symbol.name = "a2"; + symbolt a2_symbol{"a2", struct_tag_typet(A_symbol.name), irep_idt{}}; a2_symbol.base_name = "a2"; a2_symbol.pretty_name = "a2"; - a2_symbol.type = struct_tag_typet(A_symbol.name); a2_symbol.is_static_lifetime = true; symbol_table.add(a2_symbol); - symbolt a3_symbol; - a3_symbol.name = "a3"; + symbolt a3_symbol{"a3", struct_tag_typet(A_symbol.name), irep_idt{}}; a3_symbol.base_name = "a3"; a3_symbol.pretty_name = "a3"; - a3_symbol.type = struct_tag_typet(A_symbol.name); a3_symbol.is_static_lifetime = true; symbol_table.add(a3_symbol); @@ -234,27 +227,21 @@ SCENARIO( signedbv_typet int32_type(32); pointer_typet int32_ptr(int32_type, 64); - symbolt i1; - i1.name = "i1"; + symbolt i1{"i1", int32_type, irep_idt{}}; i1.base_name = "i1"; i1.pretty_name = "i1"; - i1.type = int32_type; i1.is_static_lifetime = true; symbol_table.add(i1); - symbolt i2; - i2.name = "i2"; + symbolt i2{"i2", int32_type, irep_idt{}}; i2.base_name = "i2"; i2.pretty_name = "i2"; - i2.type = int32_type; i2.is_static_lifetime = true; symbol_table.add(i2); - symbolt i3; - i3.name = "i3"; + symbolt i3{"i3", int32_type, irep_idt{}}; i3.base_name = "i3"; i3.pretty_name = "i3"; - i3.type = int32_type; i3.is_static_lifetime = true; symbol_table.add(i3); diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 5f4a35f6fa2..1564f2a6973 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -151,17 +151,12 @@ smt_responset decision_procedure_test_environmentt::receive_response() static symbolt make_test_symbol(irep_idt id, typet type) { - symbolt new_symbol; - new_symbol.name = std::move(id); - new_symbol.type = std::move(type); - return new_symbol; + return symbolt{std::move(id), std::move(type), irep_idt{}}; } static symbolt make_test_symbol(irep_idt id, exprt value) { - symbolt new_symbol; - new_symbol.name = std::move(id); - new_symbol.type = value.type(); + symbolt new_symbol{std::move(id), value.type(), irep_idt{}}; new_symbol.value = std::move(value); return new_symbol; } diff --git a/unit/testing-utils/call_graph_test_utils.cpp b/unit/testing-utils/call_graph_test_utils.cpp index bca85d6da1e..167deaecfc7 100644 --- a/unit/testing-utils/call_graph_test_utils.cpp +++ b/unit/testing-utils/call_graph_test_utils.cpp @@ -14,10 +14,7 @@ symbolt create_void_function_symbol(const irep_idt &name, const codet &code) { const code_typet void_function_type({}, empty_typet()); - symbolt function; - function.name = name; - function.type = void_function_type; - function.mode = ID_java; + symbolt function{name, void_function_type, ID_java}; function.value = code; return function; } diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 0cb55f766e9..c47c3318df0 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -455,17 +455,13 @@ TEST_CASE("Simplifying cast expressions", "[core][util]") const auto long_type = signedbv_typet(64); array_typet array_type(int_type, from_integer(5, int_type)); - symbolt a_symbol; + symbolt a_symbol{"a", array_type, irep_idt{}}; a_symbol.base_name = "a"; - a_symbol.name = "a"; - a_symbol.type = array_type; a_symbol.is_lvalue = true; symbol_table.add(a_symbol); - symbolt i_symbol; + symbolt i_symbol{"i", int_type, irep_idt{}}; i_symbol.base_name = "i"; - i_symbol.name = "i"; - i_symbol.type = int_type; i_symbol.is_lvalue = true; symbol_table.add(i_symbol); diff --git a/unit/util/symbol.cpp b/unit/util/symbol.cpp index cf4c420384e..1ef7c7befe0 100644 --- a/unit/util/symbol.cpp +++ b/unit/util/symbol.cpp @@ -18,12 +18,10 @@ SCENARIO( { GIVEN("A valid symbol") { - symbolt symbol; irep_idt symbol_name = "Test_TestBase"; - symbol.name = symbol_name; + symbolt symbol{symbol_name, typet{}, ID_C}; symbol.base_name = "TestBase"; symbol.module = "TestModule"; - symbol.mode = "C"; THEN("Symbol should be well formed") { diff --git a/unit/util/symbol_table.cpp b/unit/util/symbol_table.cpp index 6b189a78df7..88371873147 100644 --- a/unit/util/symbol_table.cpp +++ b/unit/util/symbol_table.cpp @@ -76,12 +76,10 @@ SCENARIO( { symbol_tablet symbol_table; - symbolt symbol; irep_idt symbol_name = "Test_TestBase"; - symbol.name = symbol_name; + symbolt symbol{symbol_name, typet{}, ID_C}; symbol.base_name = "TestBase"; symbol.module = "TestModule"; - symbol.mode = "C"; symbol_table.insert(symbol);