diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index a1dc45880ed..1b7290597cf 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -468,8 +468,8 @@ void goto_convertt::do_cpp_new( assert(code_type.parameters().size()==1 || code_type.parameters().size()==2); - const symbolt &tmp_symbol= - new_tmp_symbol(return_type, "new", dest, rhs.source_location()); + const symbolt &tmp_symbol = + new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); tmp_symbol_expr=tmp_symbol.symbol_expr(); @@ -499,8 +499,8 @@ void goto_convertt::do_cpp_new( assert(code_type.parameters().size()==2 || code_type.parameters().size()==3); - const symbolt &tmp_symbol= - new_tmp_symbol(return_type, "new", dest, rhs.source_location()); + const symbolt &tmp_symbol = + new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp); tmp_symbol_expr=tmp_symbol.symbol_expr(); @@ -663,13 +663,10 @@ void goto_convertt::do_java_new_array( // Must directly assign the new array to a temporary // because goto-symex will notice `x=side_effect_exprt` but not // `x=typecast_exprt(side_effect_exprt(...))` - symbol_exprt new_array_data_symbol= + symbol_exprt new_array_data_symbol = new_tmp_symbol( - data_java_new_expr.type(), - "new_array_data", - dest, - location) - .symbol_expr(); + data_java_new_expr.type(), "new_array_data", dest, location, ID_java) + .symbol_expr(); goto_programt::targett t_p2=dest.add_instruction(ASSIGN); t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr); t_p2->source_location=location; @@ -707,8 +704,9 @@ void goto_convertt::do_java_new_array( goto_programt tmp; - symbol_exprt tmp_i= - new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr(); + symbol_exprt tmp_i = + new_tmp_symbol(length.type(), "index", tmp, location, ID_java) + .symbol_expr(); code_fort for_loop; @@ -730,8 +728,9 @@ void goto_convertt::do_java_new_array( plus_exprt(data, tmp_i), data.type().subtype()); code_blockt for_body; - symbol_exprt init_sym= - new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr(); + symbol_exprt init_sym = + new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java) + .symbol_expr(); code_assignt init_subarray(init_sym, sub_java_new); code_assignt assign_subarray( diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 8c82a34a582..0660f80335f 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -237,8 +237,8 @@ void goto_convertt::clean_expr( if(result_is_used) { - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "if_expr", dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), "if_expr", dest, source_location, expr.get(ID_mode)); code_assignt assignment_true; assignment_true.lhs()=new_symbol.symbol_expr(); diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 2bca47c7723..40d590c1b25 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -2055,16 +2055,16 @@ symbolt &goto_convertt::new_tmp_symbol( const typet &type, const std::string &suffix, goto_programt &dest, - const source_locationt &source_location) + const source_locationt &source_location, + const irep_idt &mode) { - symbolt &new_symbol= - get_fresh_aux_symbol( - type, - tmp_symbol_prefix, - "tmp_"+suffix, - source_location, - irep_idt(), - symbol_table); + symbolt &new_symbol = get_fresh_aux_symbol( + type, + tmp_symbol_prefix, + "tmp_" + suffix, + source_location, + mode, + symbol_table); code_declt decl; decl.symbol()=new_symbol.symbol_expr(); @@ -2081,8 +2081,8 @@ void goto_convertt::make_temp_symbol( { const source_locationt source_location=expr.find_source_location(); - symbolt &new_symbol= - new_tmp_symbol(expr.type(), suffix, dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), suffix, dest, source_location, expr.get(ID_mode)); code_assignt assignment; assignment.lhs()=new_symbol.symbol_expr(); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index e74833815c4..84a90cb59cf 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -59,7 +59,8 @@ class goto_convertt:public messaget const typet &type, const std::string &suffix, goto_programt &dest, - const source_locationt &); + const source_locationt &, + const irep_idt &mode); symbol_exprt make_compound_literal( const exprt &expr, diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index bec761420ca..def8d98b170 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -522,10 +522,8 @@ void goto_convertt::remove_temporary_object( throw 0; } - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location()); - - new_symbol.mode=expr.get(ID_mode); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode)); if(expr.operands().size()==1) { @@ -599,8 +597,12 @@ void goto_convertt::remove_statement_expression( source_locationt source_location=last.find_source_location(); - symbolt &new_symbol= - new_tmp_symbol(expr.type(), "statement_expression", dest, source_location); + symbolt &new_symbol = new_tmp_symbol( + expr.type(), + "statement_expression", + dest, + source_location, + expr.get(ID_mode)); symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type); tmp_symbol_expr.add_source_location()=source_location; diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index c000c3c5c0f..1a7ba984e82 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/src/goto-symex/symex_builtin_functions.cpp @@ -66,6 +66,9 @@ void goto_symext::symex_allocate( exprt size=code.op0(); typet object_type=nil_typet(); + auto function_symbol = outer_symbol_table.lookup(state.source.pc->function); + INVARIANT(function_symbol, "function associated with instruction not found"); + const irep_idt &mode = function_symbol->mode; // is the type given? if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty) @@ -142,7 +145,7 @@ void goto_symext::symex_allocate( size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name); size_symbol.is_lvalue=true; size_symbol.type=tmp_size.type(); - size_symbol.mode=ID_C; + size_symbol.mode = mode; state.symbol_table.add(size_symbol); @@ -161,7 +164,7 @@ void goto_symext::symex_allocate( value_symbol.is_lvalue=true; value_symbol.type=object_type; value_symbol.type.set("#dynamic", true); - value_symbol.mode=ID_C; + value_symbol.mode = mode; state.symbol_table.add(value_symbol); diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 877252f5e12..62e1fd51fdc 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -740,6 +740,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) symbol.base_name=symbol_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: diff --git a/src/java_bytecode/java_bytecode_typecheck_type.cpp b/src/java_bytecode/java_bytecode_typecheck_type.cpp index aa92d9333cf..2f26feb59bc 100644 --- a/src/java_bytecode/java_bytecode_typecheck_type.cpp +++ b/src/java_bytecode/java_bytecode_typecheck_type.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_bytecode_typecheck.h" +#include #include void java_bytecode_typecheckt::typecheck_type(typet &type) @@ -19,17 +20,12 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) { irep_idt identifier=to_symbol_type(type).get_identifier(); - symbol_tablet::symbolst::const_iterator s_it= - symbol_table.symbols.find(identifier); - - // must exist already in the symbol table - if(s_it==symbol_table.symbols.end()) - { - error() << "failed to find type symbol "<< identifier << eom; - throw 0; - } - - assert(s_it->second.is_type); + auto type_symbol = symbol_table.lookup(identifier); + DATA_INVARIANT( + type_symbol, "symbol " + id2string(identifier) + " must exist already"); + DATA_INVARIANT( + type_symbol->is_type, + "symbol " + id2string(identifier) + " must be a type"); } else if(type.id()==ID_pointer) { @@ -55,7 +51,9 @@ void java_bytecode_typecheckt::typecheck_type(typet &type) void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol) { - assert(symbol.is_type); + DATA_INVARIANT( + symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type"); + symbol.mode = ID_java; typecheck_type(symbol.type); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 009882d2dab..460398abbd9 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -247,6 +247,7 @@ void java_string_library_preprocesst::add_string_type( string_symbol->pretty_name=id2string(class_name); string_symbol->type=string_type; string_symbol->is_type=true; + string_symbol->mode = ID_java; } /// add a symbol in the table with static lifetime and name containing diff --git a/unit/testing-utils/load_java_class.cpp b/unit/testing-utils/load_java_class.cpp index f198008dff4..217a3bb25d7 100644 --- a/unit/testing-utils/load_java_class.cpp +++ b/unit/testing-utils/load_java_class.cpp @@ -16,6 +16,8 @@ #include +#include + #include #include @@ -37,11 +39,13 @@ symbol_tablet load_java_class_lazy( free_form_cmdlinet lazy_command_line; lazy_command_line.add_flag("lazy-methods"); + register_language(new_java_bytecode_language); + return load_java_class( java_class_name, class_path, main, - new_java_bytecode_language(), + get_language_from_mode(ID_java), lazy_command_line); } @@ -59,8 +63,10 @@ symbol_tablet load_java_class( const std::string &class_path, const std::string &main) { + register_language(new_java_bytecode_language); + return load_java_class( - java_class_name, class_path, main, new_java_bytecode_language()); + java_class_name, class_path, main, get_language_from_mode(ID_java)); } /// Go through the process of loading, type-checking and finalising loading a