From ca678aa2d074925a2f886816d183b4c006817372 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 16 Apr 2018 19:29:48 +0100 Subject: [PATCH 1/4] More permissive regression tests regarding tmp var suffixes --- regression/cbmc/Quantifiers-not-exists/test.desc | 10 +++++----- .../cbmc/Quantifiers-two-dimension-array/test.desc | 2 +- regression/cbmc/Quantifiers-type/test.desc | 4 ++-- .../cbmc/pointer-function-parameters-2/test.desc | 8 ++++---- regression/cbmc/pointer-function-parameters/test.desc | 6 +++--- 5 files changed, 15 insertions(+), 15 deletions(-) diff --git a/regression/cbmc/Quantifiers-not-exists/test.desc b/regression/cbmc/Quantifiers-not-exists/test.desc index e4fd61a058f..b7181ece960 100644 --- a/regression/cbmc/Quantifiers-not-exists/test.desc +++ b/regression/cbmc/Quantifiers-not-exists/test.desc @@ -3,11 +3,11 @@ main.c ^\*\* Results:$ ^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$ -^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$ -^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$ -^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$ -^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$ -^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$ +^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$ +^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 0 of 6 failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-two-dimension-array/test.desc b/regression/cbmc/Quantifiers-two-dimension-array/test.desc index 2c1c7dab05f..b588f1621aa 100644 --- a/regression/cbmc/Quantifiers-two-dimension-array/test.desc +++ b/regression/cbmc/Quantifiers-two-dimension-array/test.desc @@ -6,7 +6,7 @@ main.c ^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$ ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$ -^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$ +^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 0 of 5 failed ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc index 1451871c4ec..ba904aec101 100644 --- a/regression/cbmc/Quantifiers-type/test.desc +++ b/regression/cbmc/Quantifiers-type/test.desc @@ -2,8 +2,8 @@ CORE main.c ^\*\* Results:$ -^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$ -^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$ +^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$ +^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$ ^\*\* 1 of 2 failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/pointer-function-parameters-2/test.desc b/regression/cbmc/pointer-function-parameters-2/test.desc index 9b90858ce5a..5ffe7f3fa78 100644 --- a/regression/cbmc/pointer-function-parameters-2/test.desc +++ b/regression/cbmc/pointer-function-parameters-2/test.desc @@ -3,10 +3,10 @@ main.c --function fun --cover branch ^\*\* 7 of 7 covered \(100.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$ -^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$ +^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc/pointer-function-parameters/test.desc b/regression/cbmc/pointer-function-parameters/test.desc index 2ea09c85011..a816cc3039a 100644 --- a/regression/cbmc/pointer-function-parameters/test.desc +++ b/regression/cbmc/pointer-function-parameters/test.desc @@ -3,9 +3,9 @@ main.c --function fun --cover branch ^\*\* 5 of 5 covered \(100\.0%\)$ ^Test suite:$ -^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$ -^a=&tmp\$\d+!0, tmp\$\d+=4$ -^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$ +^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$ +^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$ ^EXIT=0$ ^SIGNAL=0$ -- From 9f0626ccb54140924dc37d96497cf1e9d90504e3 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 17 Apr 2018 20:18:19 +0100 Subject: [PATCH 2/4] Prefix temporary var names with function id Temporary variable names must be globally unique and changing the number of temporaries in one function must not change a variable name in another function. Otherwise, this has adverse effects on goto-diff. This commit gets rid of various global temporary variables counters that do not meet above criteria. Instead, we now always use the function id to prefix temporaries to eliminate cross-function effects and increment the numeric suffix only when the entire variable name already exists, using the rename facility. --- src/ansi-c/c_nondet_symbol_factory.cpp | 4 +- src/goto-instrument/code_contracts.cpp | 2 +- src/goto-programs/convert_nondet.cpp | 7 +- src/goto-programs/goto_convert_class.h | 2 - src/goto-programs/goto_convert_functions.cpp | 2 - .../goto_convert_side_effect.cpp | 9 +- .../remove_function_pointers.cpp | 15 +- src/goto-programs/remove_instanceof.cpp | 15 +- src/java_bytecode/java_entry_point.cpp | 24 +- src/java_bytecode/java_object_factory.cpp | 94 +++--- src/java_bytecode/java_object_factory.h | 3 + .../java_static_initializers.cpp | 5 +- .../java_string_library_preprocess.cpp | 287 ++++++++++-------- .../java_string_library_preprocess.h | 21 +- src/java_bytecode/object_factory_parameters.h | 3 + src/util/fresh_symbol.cpp | 42 ++- src/util/fresh_symbol.h | 2 - src/util/rename.cpp | 6 +- src/util/rename.h | 6 +- .../gen_nondet_string_init.cpp | 4 +- .../convert_exprt_to_string_exprt.cpp | 2 - 21 files changed, 312 insertions(+), 243 deletions(-) diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index f772a0ea9b7..9b7d88d2bfb 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -43,8 +43,8 @@ static const symbolt &c_new_tmp_symbol( const bool static_lifetime, const std::string &prefix="tmp") { - symbolt &tmp_symbol= - get_fresh_aux_symbol(type, "", prefix, loc, ID_C, symbol_table); + symbolt &tmp_symbol = get_fresh_aux_symbol( + type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table); tmp_symbol.is_static_lifetime=static_lifetime; return tmp_symbol; diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index a33b0934349..5f40b8e35c5 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -250,7 +250,7 @@ const symbolt &code_contractst::new_tmp_symbol( { return get_fresh_aux_symbol( type, - "", + id2string(source_location.get_function()), "tmp_cc", source_location, irep_idt(), diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp index 56215c07cd1..30fdca79ddf 100644 --- a/src/goto-programs/convert_nondet.cpp +++ b/src/goto-programs/convert_nondet.cpp @@ -17,6 +17,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com #include // gen_nondet_init #include +#include #include @@ -135,11 +136,13 @@ void convert_nondet( message_handlert &message_handler, const object_factory_parameterst &object_factory_parameters) { + object_factory_parameterst parameters = object_factory_parameters; + parameters.function_id = function.get_function_id(); convert_nondet( function.get_goto_function().body, function.get_symbol_table(), message_handler, - object_factory_parameters); + parameters); function.compute_location_numbers(); } @@ -158,6 +161,8 @@ void convert_nondet( if(symbol.mode==ID_java) { + object_factory_parameterst parameters = object_factory_parameters; + parameters.function_id = f_it.first; convert_nondet( f_it.second.body, symbol_table, diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 4c5541a0108..e74833815c4 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -34,7 +34,6 @@ class goto_convertt:public messaget messaget(_message_handler), symbol_table(_symbol_table), ns(_symbol_table), - temporary_counter(0), tmp_symbol_prefix("goto_convertt") { } @@ -46,7 +45,6 @@ class goto_convertt:public messaget protected: symbol_table_baset &symbol_table; namespacet ns; - unsigned temporary_counter; std::string tmp_symbol_prefix; void goto_convert_rec(const codet &code, goto_programt &dest); diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index f4edab30c47..6d6b2b7441e 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -147,8 +147,6 @@ void goto_convert_functionst::convert_function( // make tmp variables local to function tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::"; - temporary_counter=0; - reset_temporary_counter(); f.type=to_code_type(symbol.type); diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index d0cfa2c9b2f..bec761420ca 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -379,7 +379,7 @@ void goto_convertt::remove_function_call( new_base_name+='_'; new_base_name+=id2string(symbol.base_name); - new_base_name+="$"+std::to_string(++temporary_counter); + new_base_name += "$0"; new_symbol.base_name=new_base_name; new_symbol.mode=symbol.mode; @@ -387,6 +387,7 @@ void goto_convertt::remove_function_call( new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); + // ensure that the name is unique new_name(new_symbol); { @@ -429,10 +430,11 @@ void goto_convertt::remove_cpp_new( auxiliary_symbolt new_symbol; - new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter); + new_symbol.base_name = "new_ptr$0"; new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); + // ensure that the name is unique new_name(new_symbol); code_declt decl; @@ -480,11 +482,12 @@ void goto_convertt::remove_malloc( { auxiliary_symbolt new_symbol; - new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter); + new_symbol.base_name = "malloc_value$0"; new_symbol.type=expr.type(); new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name); new_symbol.location=expr.source_location(); + // ensure that the name is unique new_name(new_symbol); code_declt decl; diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 4c35d3b0667..854a706e5e7 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -233,14 +233,13 @@ void remove_function_pointerst::fix_return_type( code_type.return_type(), ns)) return; - symbolt &tmp_symbol= - get_fresh_aux_symbol( - code_type.return_type(), - "remove_function_pointers", - "tmp_return_val", - function_call.source_location(), - irep_idt(), - symbol_table); + symbolt &tmp_symbol = get_fresh_aux_symbol( + code_type.return_type(), + id2string(function_call.source_location().get_function()), + "tmp_return_val", + function_call.source_location(), + irep_idt(), + symbol_table); symbol_exprt tmp_symbol_expr; tmp_symbol_expr.type()=tmp_symbol.type; diff --git a/src/goto-programs/remove_instanceof.cpp b/src/goto-programs/remove_instanceof.cpp index e859c8d9384..ad62322e90a 100644 --- a/src/goto-programs/remove_instanceof.cpp +++ b/src/goto-programs/remove_instanceof.cpp @@ -106,14 +106,13 @@ std::size_t remove_instanceoft::lower_instanceof( symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype()); exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns); - symbolt &newsym= - get_fresh_aux_symbol( - object_clsid.type(), - "instanceof_tmp", - "instanceof_tmp", - source_locationt(), - ID_java, - symbol_table); + symbolt &newsym = get_fresh_aux_symbol( + object_clsid.type(), + id2string(this_inst->function), + "instanceof_tmp", + source_locationt(), + ID_java, + symbol_table); auto newinst=goto_program.insert_after(this_inst); newinst->make_assignment(); diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index fb5561ae1c9..53d81c5b78e 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -203,19 +203,21 @@ exprt::operandst java_build_arguments( bool allow_null= !assume_init_pointers_not_null && !is_main && !is_this; + object_factory_parameterst parameters = object_factory_parameters; + parameters.function_id = function.name; + // generate code to allocate and non-deterministicaly initialize the // argument - main_arguments[param_number]= - object_factory( - p.type(), - base_name, - init_code, - allow_null, - symbol_table, - object_factory_parameters, - allocation_typet::LOCAL, - function.location, - pointer_type_selector); + main_arguments[param_number] = object_factory( + p.type(), + base_name, + init_code, + allow_null, + symbol_table, + parameters, + allocation_typet::LOCAL, + function.location, + pointer_type_selector); // record as an input codet input(ID_input); diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 138033676b0..f05e6d13e90 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -35,21 +35,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_root_class.h" #include "generic_parameter_specialization_map_keys.h" -static symbolt &new_tmp_symbol( - symbol_table_baset &symbol_table, - const source_locationt &loc, - const typet &type, - const std::string &prefix = "tmp_object_factory") -{ - return get_fresh_aux_symbol( - type, - "", - prefix, - loc, - ID_java, - symbol_table); -} - class java_object_factoryt { /// Every new variable initialized by the code emitted by the methods of this @@ -195,6 +180,7 @@ exprt allocate_dynamic_object( const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &output_code, std::vector &symbols_created, bool cast_needed) @@ -212,11 +198,13 @@ exprt allocate_dynamic_object( // create a symbol for the malloc expression so we can initialize // without having to do it potentially through a double-deref, which // breaks the to-SSA phase. - symbolt &malloc_sym=new_tmp_symbol( - symbol_table, - loc, + symbolt &malloc_sym = get_fresh_aux_symbol( pointer_type(allocate_type), - "malloc_site"); + id2string(function_id), + "malloc_site", + loc, + ID_java, + symbol_table); symbols_created.push_back(&malloc_sym); code_assignt assign=code_assignt(malloc_sym.symbol_expr(), malloc_expr); assign.add_source_location()=loc; @@ -253,6 +241,7 @@ exprt allocate_dynamic_object_with_decl( const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &output_code) { std::vector symbols_created; @@ -263,6 +252,7 @@ exprt allocate_dynamic_object_with_decl( allocate_type, symbol_table, loc, + function_id, tmp_block, symbols_created, false); @@ -306,7 +296,13 @@ exprt java_object_factoryt::allocate_object( case allocation_typet::LOCAL: case allocation_typet::GLOBAL: { - symbolt &aux_symbol=new_tmp_symbol(symbol_table, loc, allocate_type); + symbolt &aux_symbol = get_fresh_aux_symbol( + allocate_type, + id2string(object_factory_parameters.function_id), + "tmp_object_factory", + loc, + ID_java, + symbol_table); if(alloc_type==allocation_typet::GLOBAL) aux_symbol.is_static_lifetime=true; symbols_created.push_back(&aux_symbol); @@ -327,6 +323,7 @@ exprt java_object_factoryt::allocate_object( allocate_type, symbol_table, loc, + object_factory_parameters.function_id, assignments, symbols_created, cast_needed); @@ -569,6 +566,7 @@ codet initialize_nondet_string_struct( const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable) { @@ -608,8 +606,13 @@ codet initialize_nondet_string_struct( { /// \todo Refactor with make_nondet_string_expr // length_expr = nondet(int); - const symbolt length_sym = - new_tmp_symbol(symbol_table, loc, java_int_type()); + const symbolt length_sym = get_fresh_aux_symbol( + java_int_type(), + id2string(function_id), + "tmp_object_factory", + loc, + ID_java, + symbol_table); const symbol_exprt length_expr = length_sym.symbol_expr(); const side_effect_expr_nondett nondet_length(length_expr.type()); code.add(code_declt(length_expr)); @@ -646,7 +649,7 @@ codet initialize_nondet_string_struct( // data_expr = nondet(char[INFINITY]) // we use infinity for variable size const dereference_exprt data_expr(data_pointer); const exprt nondet_array = - make_nondet_infinite_char_array(symbol_table, loc, code); + make_nondet_infinite_char_array(symbol_table, loc, function_id, code); code.add(code_assignt(data_expr, nondet_array)); struct_expr.copy_to_operands(length_expr); @@ -692,6 +695,7 @@ static bool add_nondet_string_pointer_initialization( bool printable, symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &code) { const namespacet ns(symbol_table); @@ -702,14 +706,15 @@ static bool add_nondet_string_pointer_initialization( if(!struct_type.has_component("data") || !struct_type.has_component("length")) return true; - const exprt malloc_site = - allocate_dynamic_object_with_decl(expr, symbol_table, loc, code); + const exprt malloc_site = allocate_dynamic_object_with_decl( + expr, symbol_table, loc, function_id, code); code.add( initialize_nondet_string_struct( dereference_exprt(malloc_site, struct_type), max_nondet_string_length, loc, + function_id, symbol_table, printable)); return false; @@ -862,6 +867,7 @@ void java_object_factoryt::gen_nondet_pointer_init( object_factory_parameters.string_printable, symbol_table, loc, + object_factory_parameters.function_id, assignments); } else @@ -967,7 +973,13 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init( const pointer_typet &replacement_pointer, size_t depth) { - symbolt new_symbol=new_tmp_symbol(symbol_table, loc, replacement_pointer); + symbolt new_symbol = get_fresh_aux_symbol( + replacement_pointer, + id2string(object_factory_parameters.function_id), + "tmp_object_factory", + loc, + ID_java, + symbol_table); // Generate a new object into this new symbol gen_nondet_init( @@ -1253,11 +1265,13 @@ void java_object_factoryt::allocate_nondet_length_array( const exprt &max_length_expr, const typet &element_type) { - symbolt &length_sym=new_tmp_symbol( - symbol_table, - loc, + symbolt &length_sym = get_fresh_aux_symbol( java_int_type(), - "nondet_array_length"); + id2string(object_factory_parameters.function_id), + "nondet_array_length", + loc, + ID_java, + symbol_table); symbols_created.push_back(&length_sym); const auto &length_sym_expr=length_sym.symbol_expr(); @@ -1347,11 +1361,13 @@ void java_object_factoryt::gen_nondet_array_init( // Interpose a new symbol, as the goto-symex stage can't handle array indexing // via a cast. - symbolt &array_init_symbol=new_tmp_symbol( - symbol_table, - loc, + symbolt &array_init_symbol = get_fresh_aux_symbol( init_array_expr.type(), - "array_data_init"); + id2string(object_factory_parameters.function_id), + "array_data_init", + loc, + ID_java, + symbol_table); symbols_created.push_back(&array_init_symbol); const auto &array_init_symexpr=array_init_symbol.symbol_expr(); codet data_assign=code_assignt(array_init_symexpr, init_array_expr); @@ -1360,11 +1376,13 @@ void java_object_factoryt::gen_nondet_array_init( // Emit init loop for(array_init_iter=0; array_init_iter!=array.length; // ++array_init_iter) init(array[array_init_iter]); - symbolt &counter=new_tmp_symbol( - symbol_table, - loc, + symbolt &counter = get_fresh_aux_symbol( length_expr.type(), - "array_init_iter"); + id2string(object_factory_parameters.function_id), + "array_init_iter", + loc, + ID_java, + symbol_table); symbols_created.push_back(&counter); exprt counter_expr=counter.symbol_expr(); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 9a5da141344..a5ba9ea5500 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -142,6 +142,7 @@ exprt allocate_dynamic_object( const typet &allocate_type, symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &output_code, std::vector &symbols_created, bool cast_needed = false); @@ -150,12 +151,14 @@ exprt allocate_dynamic_object_with_decl( const exprt &target_expr, symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &output_code); codet initialize_nondet_string_struct( const exprt &obj, const std::size_t &max_nondet_string_length, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable); diff --git a/src/java_bytecode/java_static_initializers.cpp b/src/java_bytecode/java_static_initializers.cpp index b95dedbfea2..9cb9b054fea 100644 --- a/src/java_bytecode/java_static_initializers.cpp +++ b/src/java_bytecode/java_static_initializers.cpp @@ -369,6 +369,9 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body( class_globals.first != class_globals.second, "class with synthetic clinit should have at least one global to init"); + object_factory_parameterst parameters = object_factory_parameters; + parameters.function_id = function_id; + for(auto it = class_globals.first; it != class_globals.second; ++it) { const symbol_exprt new_global_symbol = @@ -381,7 +384,7 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body( false, allocation_typet::DYNAMIC, !is_non_null_library_global(it->second), - object_factory_parameters, + parameters, pointer_type_selector, update_in_placet::NO_UPDATE_IN_PLACE); } diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 1f2ce3365d6..a05a285c18b 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -538,6 +538,7 @@ refined_string_exprt java_string_library_preprocesst::decl_string_expr( /// \return a new string_expr refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr( const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) { @@ -548,7 +549,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr( code.add(code_assignt(str.length(), nondet_length), loc); exprt nondet_array_expr = - make_nondet_infinite_char_array(symbol_table, loc, code); + make_nondet_infinite_char_array(symbol_table, loc, function_id, code); address_of_exprt array_pointer( index_exprt(nondet_array_expr, from_integer(0, java_int_type()))); @@ -573,11 +574,12 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr( exprt java_string_library_preprocesst::allocate_fresh_string( const typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) { exprt str=fresh_string(type, loc, symbol_table); - allocate_dynamic_object_with_decl(str, symbol_table, loc, code); + allocate_dynamic_object_with_decl(str, symbol_table, loc, function_id, code); return str; } @@ -590,12 +592,14 @@ exprt java_string_library_preprocesst::allocate_fresh_string( exprt java_string_library_preprocesst::allocate_fresh_array( const typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code) { exprt array=fresh_array(type, loc, symbol_table); code.add(code_declt(array), loc); - allocate_dynamic_object_with_decl(array, symbol_table, loc, code); + allocate_dynamic_object_with_decl( + array, symbol_table, loc, function_id, code); return array; } @@ -647,6 +651,7 @@ codet java_string_library_preprocesst::code_return_function_application( exprt make_nondet_infinite_char_array( symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &code) { const array_typet array_type( @@ -799,7 +804,7 @@ refined_string_exprt java_string_library_preprocesst::string_expr_of_function( code.add(code_declt(return_code), loc); const refined_string_exprt string_expr = - make_nondet_string_expr(loc, symbol_table, code); + make_nondet_string_expr(loc, function_name, symbol_table, code); // args is { str.length, str.content, arguments... } exprt::operandst args; @@ -942,6 +947,7 @@ java_string_library_preprocesst::string_literal_to_string_expr( codet java_string_library_preprocesst::make_equals_function_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table) { const typet &return_type = type.return_type(); @@ -991,6 +997,7 @@ codet java_string_library_preprocesst::make_equals_function_code( codet java_string_library_preprocesst::make_float_to_string_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table) { // Getting the argument @@ -1002,7 +1009,8 @@ codet java_string_library_preprocesst::make_float_to_string_code( code_blockt code; // Declaring and allocating String * str - exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); + exprt str = allocate_fresh_string( + type.return_type(), loc, function_id, symbol_table, code); // Expression representing 0.0 ieee_float_spect float_spec(to_floatbv_type(params[0].type())); @@ -1373,6 +1381,7 @@ exprt java_string_library_preprocesst::make_argument_for_format( int index, const struct_typet &structured_type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code) { @@ -1388,13 +1397,14 @@ exprt java_string_library_preprocesst::make_argument_for_format( if(name!="string_expr") { std::string tmp_name="tmp_"+id2string(name); - symbolt field_symbol=get_fresh_aux_symbol( - type, tmp_name, tmp_name, loc, ID_java, symbol_table); + symbolt field_symbol = get_fresh_aux_symbol( + type, id2string(function_id), tmp_name, loc, ID_java, symbol_table); field_expr=field_symbol.symbol_expr(); code.add(code_declt(field_expr), loc); } else - field_expr = make_nondet_string_expr(loc, symbol_table, code); + field_expr = + make_nondet_string_expr(loc, function_id, symbol_table, code); field_exprs.push_back(field_expr); arg_i_struct.copy_to_operands(field_expr); @@ -1402,10 +1412,16 @@ exprt java_string_library_preprocesst::make_argument_for_format( // arg_i = argv[index] exprt obj=get_object_at_index(argv, index); - symbolt object_symbol=get_fresh_aux_symbol( - obj.type(), "tmp_format_obj", "tmp_format_obj", loc, ID_java, symbol_table); + symbolt object_symbol = get_fresh_aux_symbol( + obj.type(), + id2string(function_id), + "tmp_format_obj", + loc, + ID_java, + symbol_table); symbol_exprt arg_i=object_symbol.symbol_expr(); - allocate_dynamic_object_with_decl(arg_i, symbol_table, loc, code); + allocate_dynamic_object_with_decl( + arg_i, symbol_table, loc, function_id, code); code.add(code_assignt(arg_i, obj), loc); code.add( code_assumet( @@ -1468,6 +1484,7 @@ exprt java_string_library_preprocesst::make_argument_for_format( codet java_string_library_preprocesst::make_string_format_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table) { PRECONDITION(type.parameters().size()==2); @@ -1495,13 +1512,14 @@ codet java_string_library_preprocesst::make_string_format_code( std::vector processed_args; processed_args.push_back(args[0]); for(std::size_t i=0; isecond(type, loc, symbol_table); + return it->second(type, loc, function_id, symbol_table); return nil_exprt(); } @@ -1911,28 +1937,29 @@ void java_string_library_preprocesst::initialize_conversion_table() // provided for them in the class-path. // String library + conversion_table["java::java.lang.String.:(Ljava/lang/String;)V"] = + std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); conversion_table - ["java::java.lang.String.:(Ljava/lang/String;)V"]= - std::bind( - &java_string_library_preprocesst::make_copy_constructor_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); - conversion_table - ["java::java.lang.String.:(Ljava/lang/StringBuilder;)V"]= - std::bind( - &java_string_library_preprocesst::make_copy_constructor_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.String.:(Ljava/lang/StringBuilder;)V"] = std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); conversion_table["java::java.lang.String.:([CII)V"] = std::bind( &java_string_library_preprocesst::make_init_from_array_code, this, std::placeholders::_1, std::placeholders::_2, - std::placeholders::_3); + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_constructor ["java::java.lang.String.:()V"]= ID_cprover_string_empty_string_func; @@ -1970,25 +1997,27 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]= ID_cprover_string_endswith_func; - conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"]= + conversion_table["java::java.lang.String.equals:(Ljava/lang/Object;)Z"] = std::bind( &java_string_library_preprocesst::make_equals_function_code, this, std::placeholders::_1, std::placeholders::_2, - std::placeholders::_3); + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_function ["java::java.lang.String.equalsIgnoreCase:(Ljava/lang/String;)Z"]= ID_cprover_string_equals_ignore_case_func; conversion_table ["java::java.lang.String.format:(Ljava/lang/String;[Ljava/lang/Object;)" - "Ljava/lang/String;"]= + "Ljava/lang/String;"] = std::bind( &java_string_library_preprocesst::make_string_format_code, this, std::placeholders::_1, std::placeholders::_2, - std::placeholders::_3); + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_function ["java::java.lang.String.hashCode:()I"]= ID_cprover_string_hash_code_func; @@ -2022,14 +2051,13 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_function ["java::java.lang.String.lastIndexOf:(Ljava/lang/String;I)I"]= ID_cprover_string_last_index_of_func; - conversion_table - ["java::java.lang.String.length:()I"]= - std::bind( - &java_string_library_preprocesst::make_string_length_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.String.length:()I"] = std::bind( + &java_string_library_preprocesst::make_string_length_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_function ["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/" "String;II)I"] = ID_cprover_string_offset_by_code_point_func; @@ -2061,14 +2089,14 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.toLowerCase:()Ljava/lang/String;"]= ID_cprover_string_to_lower_case_func; - conversion_table - ["java::java.lang.String.toString:()Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_copy_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.String.toString:()Ljava/lang/String;"] = + std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.toUpperCase:()Ljava/lang/String;"]= ID_cprover_string_to_upper_case_func; @@ -2081,22 +2109,22 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.valueOf:(C)Ljava/lang/String;"]= ID_cprover_string_of_char_func; - conversion_table - ["java::java.lang.String.valueOf:(D)Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_float_to_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); - conversion_table - ["java::java.lang.String.valueOf:(F)Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_float_to_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.String.valueOf:(D)Ljava/lang/String;"] = + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); + conversion_table["java::java.lang.String.valueOf:(F)Ljava/lang/String;"] = + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_string_returning_function ["java::java.lang.String.valueOf:(I)Ljava/lang/String;"]= ID_cprover_string_of_int_func; @@ -2106,13 +2134,13 @@ void java_string_library_preprocesst::initialize_conversion_table() // StringBuilder library conversion_table - ["java::java.lang.StringBuilder.:(Ljava/lang/String;)V"]= - std::bind( - &java_string_library_preprocesst::make_copy_constructor_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.StringBuilder.:(Ljava/lang/String;)V"] = std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_constructor ["java::java.lang.StringBuilder.:()V"]= ID_cprover_string_empty_string_func; @@ -2182,14 +2210,13 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_assign_and_return_function ["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/" "lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func; - conversion_table - ["java::java.lang.StringBuilder.length:()I"]= - std::bind( - &java_string_library_preprocesst::make_string_length_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.StringBuilder.length:()I"] = std::bind( + &java_string_library_preprocesst::make_string_length_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_assign_function ["java::java.lang.StringBuilder.setCharAt:(IC)V"]= ID_cprover_string_char_set_func; @@ -2203,23 +2230,23 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::java.lang.StringBuilder.substring:(I)Ljava/lang/String;"]= ID_cprover_string_substring_func; conversion_table - ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_copy_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.StringBuilder.toString:()Ljava/lang/String;"] = std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); // StringBuffer library conversion_table - ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"]= - std::bind( - &java_string_library_preprocesst::make_copy_constructor_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.StringBuffer.:(Ljava/lang/String;)V"] = std::bind( + &java_string_library_preprocesst::make_copy_constructor_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_constructor ["java::java.lang.StringBuffer.:()V"]= ID_cprover_string_empty_string_func; @@ -2303,39 +2330,39 @@ void java_string_library_preprocesst::initialize_conversion_table() ["java::org.cprover.CProverString.substring:(Ljava/Lang/" "StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func; conversion_table - ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_copy_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"] = std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); // CharSequence library cprover_equivalent_to_java_function ["java::java.lang.CharSequence.charAt:(I)C"]= ID_cprover_string_char_at_func; conversion_table - ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_copy_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + ["java::java.lang.CharSequence.toString:()Ljava/lang/String;"] = std::bind( + &java_string_library_preprocesst::make_copy_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); conversion_table ["java::java.lang.CharSequence.length:()I"]= conversion_table["java::java.lang.String.length:()I"]; // Other libraries - conversion_table - ["java::java.lang.Float.toString:(F)Ljava/lang/String;"]= - std::bind( - &java_string_library_preprocesst::make_float_to_string_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.Float.toString:(F)Ljava/lang/String;"] = + std::bind( + &java_string_library_preprocesst::make_float_to_string_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); cprover_equivalent_to_java_function ["java::java.lang.Integer.parseInt:(Ljava/lang/String;)I"]= ID_cprover_string_parse_int_func; @@ -2363,12 +2390,12 @@ void java_string_library_preprocesst::initialize_conversion_table() cprover_equivalent_to_java_string_returning_function ["java::java.lang.Long.toString:(JI)Ljava/lang/String;"]= ID_cprover_string_of_int_func; - conversion_table - ["java::java.lang.Object.getClass:()Ljava/lang/Class;"]= - std::bind( - &java_string_library_preprocesst::make_object_get_class_code, - this, - std::placeholders::_1, - std::placeholders::_2, - std::placeholders::_3); + conversion_table["java::java.lang.Object.getClass:()Ljava/lang/Class;"] = + std::bind( + &java_string_library_preprocesst::make_object_get_class_code, + this, + std::placeholders::_1, + std::placeholders::_2, + std::placeholders::_3, + std::placeholders::_4); } diff --git a/src/java_bytecode/java_string_library_preprocess.h b/src/java_bytecode/java_string_library_preprocess.h index c3bedd13734..d481047dc20 100644 --- a/src/java_bytecode/java_string_library_preprocess.h +++ b/src/java_bytecode/java_string_library_preprocess.h @@ -100,8 +100,11 @@ class java_string_library_preprocesst:public messaget const typet index_type; const refined_string_typet refined_string_type; - typedef std::function< - codet(const code_typet &, const source_locationt &, symbol_table_baset &)> + typedef std::function conversion_functiont; typedef std::unordered_map id_mapt; @@ -148,41 +151,49 @@ class java_string_library_preprocesst:public messaget codet make_equals_function_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_float_to_string_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_string_to_char_array_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_tablet &symbol_table); codet make_string_format_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_copy_string_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_copy_constructor_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_string_length_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); codet make_object_get_class_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); // Helper functions @@ -241,18 +252,21 @@ class java_string_library_preprocesst:public messaget refined_string_exprt make_nondet_string_expr( const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code); exprt allocate_fresh_string( const typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code); exprt allocate_fresh_array( const typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_tablet &symbol_table, code_blockt &code); @@ -329,6 +343,7 @@ class java_string_library_preprocesst:public messaget int index, const struct_typet &structured_type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code); @@ -344,12 +359,14 @@ class java_string_library_preprocesst:public messaget codet make_init_from_array_code( const code_typet &type, const source_locationt &loc, + const irep_idt &function_id, symbol_table_baset &symbol_table); }; exprt make_nondet_infinite_char_array( symbol_table_baset &symbol_table, const source_locationt &loc, + const irep_idt &function_id, code_blockt &code); void add_pointer_to_array_association( diff --git a/src/java_bytecode/object_factory_parameters.h b/src/java_bytecode/object_factory_parameters.h index dfc498c9661..5e0785bf7a7 100644 --- a/src/java_bytecode/object_factory_parameters.h +++ b/src/java_bytecode/object_factory_parameters.h @@ -34,6 +34,9 @@ struct object_factory_parameterst final /// Force string content to be ASCII printable characters when set to true. bool string_printable = false; + + /// Function id, used as a prefix for identifiers of temporaries + irep_idt function_id; }; #endif diff --git a/src/util/fresh_symbol.cpp b/src/util/fresh_symbol.cpp index 34cef89a30f..0f7c3a9daf2 100644 --- a/src/util/fresh_symbol.cpp +++ b/src/util/fresh_symbol.cpp @@ -11,16 +11,8 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "fresh_symbol.h" -// This needs to be outside get_fresh_aux_symbol -// to make it available for both reset_temporary_counter -// and get_fresh_aux_symbol -static size_t temporary_counter=0; - -// This is useful with loading multiple GOTO models -void reset_temporary_counter() -{ - temporary_counter=0; -} +#include "namespace.h" +#include "rename.h" /// Installs a fresh-named symbol with the requested name pattern /// \par parameters: `type`: type of new symbol @@ -38,19 +30,23 @@ symbolt &get_fresh_aux_symbol( const irep_idt &symbol_mode, symbol_table_baset &symbol_table) { - // Loop until find a name that doesn't clash with a non-auxilliary symbol - while(true) + namespacet ns(symbol_table); + irep_idt identifier = basename_prefix; + std::size_t prefix_size = 0; + if(!name_prefix.empty()) { - auxiliary_symbolt new_symbol( - // Distinguish local variables with the same name - basename_prefix + "$" + std::to_string(++temporary_counter), - type); - if(!name_prefix.empty()) - new_symbol.name=name_prefix+"::"+id2string(new_symbol.base_name); - new_symbol.location=source_location; - new_symbol.mode=symbol_mode; - std::pair res=symbol_table.insert(std::move(new_symbol)); - if(res.second) - return res.first; + identifier = name_prefix + "::" + basename_prefix; + prefix_size = name_prefix.size() + 2; } + get_new_name(identifier, ns, '$'); + std::string basename = id2string(identifier).substr(prefix_size); + + auxiliary_symbolt new_symbol(basename, type); + new_symbol.name = identifier; + new_symbol.location = source_location; + new_symbol.mode = symbol_mode; + std::pair res = symbol_table.insert(std::move(new_symbol)); + CHECK_RETURN(res.second); + + return res.first; } diff --git a/src/util/fresh_symbol.h b/src/util/fresh_symbol.h index 18d91164248..8cdedc56977 100644 --- a/src/util/fresh_symbol.h +++ b/src/util/fresh_symbol.h @@ -19,8 +19,6 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include #include -void reset_temporary_counter(); - symbolt &get_fresh_aux_symbol( const typet &type, const std::string &name_prefix, diff --git a/src/util/rename.cpp b/src/util/rename.cpp index b0fdf8d3219..17645508ebf 100644 --- a/src/util/rename.cpp +++ b/src/util/rename.cpp @@ -24,13 +24,13 @@ void get_new_name(symbolt &symbol, const namespacet &ns) /// automated variable renaming /// \par parameters: symbol to be renamed, namespace /// \return new symbol -void get_new_name(irep_idt &new_name, const namespacet &ns) +void get_new_name(irep_idt &new_name, const namespacet &ns, char delimiter) { const symbolt *symbol; if(ns.lookup(new_name, symbol)) - return; + return; // name not taken yet - std::string prefix=id2string(new_name)+"_"; + std::string prefix = id2string(new_name) + delimiter; new_name=prefix+std::to_string(ns.get_max(prefix)+1); } diff --git a/src/util/rename.h b/src/util/rename.h index 8e9269e02be..3456bfc3827 100644 --- a/src/util/rename.h +++ b/src/util/rename.h @@ -23,7 +23,9 @@ class symbolt; void get_new_name(symbolt &symbol, const namespacet &ns); -void get_new_name(irep_idt &new_name, - const namespacet &ns); +void get_new_name( + irep_idt &new_name, + const namespacet &ns, + char delimiter = '_'); #endif // CPROVER_UTIL_RENAME_H diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index f038a4e7642..efba76b4fe0 100644 --- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -48,8 +48,8 @@ SCENARIO( WHEN("Initialisation code for a string is generated") { - const codet code = - initialize_nondet_string_struct(expr, 20, loc, symbol_table, false); + const codet code = initialize_nondet_string_struct( + expr, 20, loc, "test", symbol_table, false); THEN("Code is produced") { diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp index c24a94b1f50..e9eca838d9c 100644 --- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp +++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp @@ -32,8 +32,6 @@ TEST_CASE("Convert exprt to string exprt") { GIVEN("A location, a string expression, and a symbol table") { - reset_temporary_counter(); - source_locationt loc; symbol_tablet symbol_table; namespacet ns(symbol_table); From 3cd8bf49b29b67d6c71cec2f6c10209c80eef4ea Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Mon, 16 Apr 2018 11:48:44 +0100 Subject: [PATCH 3/4] Temporary vars tests for goto-diff --- .../goto-diff/java-tmp-vars-array/new.jar | Bin 0 -> 662 bytes .../java-tmp-vars-array/new/Test.java | 11 +++++++++++ .../goto-diff/java-tmp-vars-array/old.jar | Bin 0 -> 668 bytes .../java-tmp-vars-array/old/Test.java | 11 +++++++++++ .../goto-diff/java-tmp-vars-array/test.desc | 10 ++++++++++ regression/goto-diff/java-tmp-vars-inc/new.jar | Bin 0 -> 657 bytes .../goto-diff/java-tmp-vars-inc/new/Test.java | 11 +++++++++++ regression/goto-diff/java-tmp-vars-inc/old.jar | Bin 0 -> 666 bytes .../goto-diff/java-tmp-vars-inc/old/Test.java | 11 +++++++++++ .../goto-diff/java-tmp-vars-inc/test.desc | 10 ++++++++++ regression/goto-diff/java-tmp-vars-new/new.jar | Bin 0 -> 1288 bytes .../goto-diff/java-tmp-vars-new/new/Test.java | 17 +++++++++++++++++ regression/goto-diff/java-tmp-vars-new/old.jar | Bin 0 -> 1294 bytes .../goto-diff/java-tmp-vars-new/old/Test.java | 17 +++++++++++++++++ .../goto-diff/java-tmp-vars-new/test.desc | 10 ++++++++++ .../goto-diff/java-tmp-vars-string/new.jar | Bin 0 -> 752 bytes .../java-tmp-vars-string/new/Test.java | 11 +++++++++++ .../goto-diff/java-tmp-vars-string/old.jar | Bin 0 -> 757 bytes .../java-tmp-vars-string/old/Test.java | 11 +++++++++++ .../goto-diff/java-tmp-vars-string/test.desc | 10 ++++++++++ 20 files changed, 140 insertions(+) create mode 100644 regression/goto-diff/java-tmp-vars-array/new.jar create mode 100644 regression/goto-diff/java-tmp-vars-array/new/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-array/old.jar create mode 100644 regression/goto-diff/java-tmp-vars-array/old/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-array/test.desc create mode 100644 regression/goto-diff/java-tmp-vars-inc/new.jar create mode 100644 regression/goto-diff/java-tmp-vars-inc/new/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-inc/old.jar create mode 100644 regression/goto-diff/java-tmp-vars-inc/old/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-inc/test.desc create mode 100644 regression/goto-diff/java-tmp-vars-new/new.jar create mode 100644 regression/goto-diff/java-tmp-vars-new/new/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-new/old.jar create mode 100644 regression/goto-diff/java-tmp-vars-new/old/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-new/test.desc create mode 100644 regression/goto-diff/java-tmp-vars-string/new.jar create mode 100644 regression/goto-diff/java-tmp-vars-string/new/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-string/old.jar create mode 100644 regression/goto-diff/java-tmp-vars-string/old/Test.java create mode 100644 regression/goto-diff/java-tmp-vars-string/test.desc diff --git a/regression/goto-diff/java-tmp-vars-array/new.jar b/regression/goto-diff/java-tmp-vars-array/new.jar new file mode 100644 index 0000000000000000000000000000000000000000..952a9a66e468cd6f39d0acb96d81bace3bc32eb4 GIT binary patch literal 662 zcmWIWW@Zs#;Nak3xRpG?hXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)Ca0?LM@ z7MJKH=Oh*v_x7FUJD4EQdVa;WsO|e2T5s$)s=84`y3^&+CIz$Dt$&s{sZM#Gq$>E4 zLC)(;N5pUO;1t%H6VI*(-so*Y2J4R^*$z`G|r=(pB@g z9jp5PZk^?RLiw2biOUX$icBj`Z4_D^x35X>j)2d)W5=hgXIY~kl`xfK^QRrR55M}! zetVAYPOImi8vpC5R5)Hx`EI!69w;_kEVq~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)Ca0?LM@ z7MJKH=Oh*vr}mxZJD4EQdVb5*pzGoj1f;j`P??sbJkg{uQb2n3wD}<`T0X_BQBjgR z;M^%GDE&X_+?k*IEoVM|{f*&*)3LU`C9P9hO%CS#Zj>+MsM=_vDslI&li;OV`+&ob zuLb|^e4Tsa;`Cm&%SUGh&$67q(R0J`-H+?mRqYel*lE?Wb!&Bzuz|os9YYSujjyE5 zBd)sNi#qH4WZ_57PbCvJ#Q4tJwC0GEX1t?#9*0=?=j2o2A{+H*B~Rs8Y_wut{gSf> zg;o`6#D8DR9e-<;&AV^^ou=pun4H_&c0?K!CoLOeeXarhs>KKj4Mrvr2Gl5p#TO__ zQ2{)TKoN|t6*-VW5sCn|Kqg!(QuLymfb1|(WFWv{AQKTa0p6@^AUS3r+zO;G0zJaO F002y%!ju32 literal 0 HcmV?d00001 diff --git a/regression/goto-diff/java-tmp-vars-array/old/Test.java b/regression/goto-diff/java-tmp-vars-array/old/Test.java new file mode 100644 index 00000000000..3ca17ac429d --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-array/old/Test.java @@ -0,0 +1,11 @@ +public class Test { + public int[] f00(int[] x) { + int[] y = x; + return y; + } + + public int[] f01(int[] z) { + int[] w = new int[z.length]; + return w; + } +} diff --git a/regression/goto-diff/java-tmp-vars-array/test.desc b/regression/goto-diff/java-tmp-vars-array/test.desc new file mode 100644 index 00000000000..9fb8793fd10 --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-array/test.desc @@ -0,0 +1,10 @@ +CORE +new.jar +old.jar +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(\[I\)\[I\ndeleted functions: +-- +^warning: ignoring diff --git a/regression/goto-diff/java-tmp-vars-inc/new.jar b/regression/goto-diff/java-tmp-vars-inc/new.jar new file mode 100644 index 0000000000000000000000000000000000000000..e814382258556d0db16267efe94abea3ab0659f3 GIT binary patch literal 657 zcmWIWW@Zs#;Nak3xSc$~hXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)Ca0?LM@ z7MJKH=Oh*v_xkPSV@wp7Q(8agzFccYfQ68%RHuuQh)aFBUD2V~Lmye>+!s&MuxV%) z+O3oo{pQWNGk)KG?y_en3D~euFTC$4nRA$+i z@6|QFwd!ipPP0}0cHXlS&M$g=FZ{5>mn$){kDeW~-6{FP;D#22SvngnGf$z13jqC2nqs5CJ_eIc!Wg~C>~J(JYqnximnwoWI?fr r0JcCTTq{zXqMLy1Fi;F2z+oU05g!5GtZX1TW+2=Oq>lkT!oUCkf}^*S literal 0 HcmV?d00001 diff --git a/regression/goto-diff/java-tmp-vars-inc/new/Test.java b/regression/goto-diff/java-tmp-vars-inc/new/Test.java new file mode 100644 index 00000000000..d0b696a8601 --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-inc/new/Test.java @@ -0,0 +1,11 @@ +public class Test { + public int f00(int x) { + int y = x++; + return y; + } + + public int f01(int z) { + int w = z++; + return w; + } +} diff --git a/regression/goto-diff/java-tmp-vars-inc/old.jar b/regression/goto-diff/java-tmp-vars-inc/old.jar new file mode 100644 index 0000000000000000000000000000000000000000..d2246a9163a321b88d4000fe3ab71bb9276f64b1 GIT binary patch literal 666 zcmWIWW@Zs#;Nak3xSc$~hXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)Ca0?LM@ z7MJKH=Oh*vr}mxZJD4EQdVb5*pwgSlie?czRHohVP!URWd=p(4v{2}jaD|Mtc4sU5 zhk&GIg3|w!^wRhJf3oLZzj}k&CbNU%aGrZ)-*wKkYWvz-T_!8hVW`EVs2!C2n(g(m zBez$$b_kj9DfqK)p{M{J zL!jtI*NPm(py)&ZTObpz6)AGjO+a=SC@K)(Fp!Cem;i59Hjo@M5N-w1=Ybw!U;qG@ CM8UcM literal 0 HcmV?d00001 diff --git a/regression/goto-diff/java-tmp-vars-inc/old/Test.java b/regression/goto-diff/java-tmp-vars-inc/old/Test.java new file mode 100644 index 00000000000..d70a47ebf75 --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-inc/old/Test.java @@ -0,0 +1,11 @@ +public class Test { + public int f00(int x) { + int y = x; + return y; + } + + public int f01(int z) { + int w = z++; + return w; + } +} diff --git a/regression/goto-diff/java-tmp-vars-inc/test.desc b/regression/goto-diff/java-tmp-vars-inc/test.desc new file mode 100644 index 00000000000..01f06839d18 --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-inc/test.desc @@ -0,0 +1,10 @@ +CORE +new.jar +old.jar +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(I\)I\ndeleted functions: +-- +^warning: ignoring diff --git a/regression/goto-diff/java-tmp-vars-new/new.jar b/regression/goto-diff/java-tmp-vars-new/new.jar new file mode 100644 index 0000000000000000000000000000000000000000..f52971d93f34a4a1ac30068b05fa8dd3878abac0 GIT binary patch literal 1288 zcmWIWW@Zs#;Nak3xRX4=hXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)A^2g*9? zCFdj-7wh`_b2k<6)CONR@&5gp(JIU(ZkMPd+uTKbt``E|x@#;=xb^*&fTN@Q0)El6 zFE+f*t**X(Z~k%a0|L6tS~|Sj7&)i)3B8h%lA6WxiSyGTS-~rX674rzF8h^x2c(^h z6IkOa(VbfN$#vJqKg!`frIVI7&S-aClz+rh+U4F+9D^tKbk+o`_RT!#V#=A6BL7PH}9Au{N-VWzrnPhjzU(i zEhf)?C38wiAn{aZ-I?O1-KSS8OZhRpR7EiS;lT#a1*{8K*V&8SJbAyZv&V~P z!N&zwy$4-CXzjMs-Z<;A^^0R|3C7W-D=z#9t-k+c{W3%At-ItwzB7+l8n_bZvj=#6 z#|4xPNi8mcc(AwM+xxJCNb7muTRzf@GjnTmT<)mq`LLFYE)u ze)>9{*pBS_DHZBFUY%;Rynklr^K*}Xr~l=Az|?Lwt01@Jg6Iv=7o1->ucgjf{#5kf zmp|1`$!pRkJ!s3+Q@>iQ)14`j{$@shGvmUit&10)-)we{^V{52T`qCUtuD_yb^TM0 zpsq5zSj&NV&9yQD8AsG#D=l1n+EMK3=Lc$WCtB9d(|YFkDQLw~ou-euzE0-hKYgb0 zXZ~EWswgN`a^d@*57Yh&sAqgQ|HZ)ZSJE}H_kA;t~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EVuUMhqj`ZH zDC?+~oRe5wtn2U3-BiF+8+_Ts`}b!?t1y?iU80U`a~JWsUI={auCX-X*7sKej*jvR z_(jjY*zh*Dy88CL`Nz2r2F{o2{sp` zkajXoV2!IpcWT`y*Igg~D2MlyPFmhLquq5;{t-)QmwQKz7amTqz24Gh)U0_>PwL#o zZvJzp`dub0Ji9w|U+0Y(-`s6ZZalPt|7ZBd>hgg1oSEhAHO)nT4Sl~I>CVo_a;l+fEQ~r}|oR9SRVbbN2d?ADOx=-dhcNmqutrbc(V4p8jJ> z%M1sfJ=3QqJY=+)vO~Y4m;3Y0#Duu_$Au4wyk%M7iz?ve-j&OBmi;7Xv+ z9^myI7f?1NwYUW0!Px$@UWXk-TF?95@{wMgnfupKpm4gz46b)tPMSNoLN~my@;p9k zlA6$DyXosh#2?*i7kc0FNQt@l+?k#C@67!9^Y0&~g2q~5-y3RHFSv5Jzp(sbd2HnO z_)*sa>vy&b4bP=bO88xnvV`g8HZ(@56mET8qXKYPR-@5=Ol z>Rq^vBdn2?*(u@pA-!)LCXddo@_4ag({z@XcXo4%8$DVv{b{j&)w#`6&+Pq}`?Mu* z)>7k0nVd2-Yq|N8oQyMU zbJkpBF6)i8u3cN$wc+2+#ir_Z3u>L$A2xfvEUS5~JtzQ|do1YVWMp6{2jT#4MkWyk z)T|B5x1g+z3gCGal+n?(B4;*G#zp{JAQP??DVrmk0Lqle=@yhJ5#TV83C*JDnvjzN qs-|5)|3MQtx+dfx0HqWJm;v-XBHaXdv$BEYSb~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EVuUO1pm~7{ zC>xSmT%wnplUQ6lH_+Grkb^+&WvBgXnzlB@%j}W(z-@BRM9$=6OI5>+ik#D4URmB* zuiszdR+;sK`A^`nNR?SD*dNP1JG*bL`RB6lU*EoDJ;0bH#$#b6rlV1iQoyU@wdTc& zR}o4X?ujyK$62=C+o2@lH+i1Ilv{~9dY_`>m&Bg$pAncJrF+P2ukD9-d()mA{hOxl zeRxOxjUS%Ar@nK9sh_;;FsF4>^G(t6o9otWO+2I&vj4T;Cxcg=SB@El?Pz_@ZWgxj z*t#WC0{#ib{9+a~SXy~_VMle#TzkveehJNP(`o`(w*NaVx`A)5yuY5P3UBe8hq1jA zCAw!PUr<(OnZ4Ld@##gKXUmrU{&PVq`KjcouM)4Waj-5wk;wA4=J&&3ZF`r#!oY-O zU;OtTteQO2=sDN3`;4G?_Br9ST8oi^ffX3p0p5&EA`Ga>1eOLs$pjU^;~kV}(6u5* v94L_>fGv;-*NT*6kWBzZFtWoy5sUzbflNen2Y9oxf#jHha4V2j1-lpk8`kPj literal 0 HcmV?d00001 diff --git a/regression/goto-diff/java-tmp-vars-string/new/Test.java b/regression/goto-diff/java-tmp-vars-string/new/Test.java new file mode 100644 index 00000000000..7313bba0d2c --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-string/new/Test.java @@ -0,0 +1,11 @@ +public class Test { + public String f00(String x) { + String y = x + "abc"; + return y; + } + + public String f01(String z) { + String w = z + "abc"; + return w; + } +} diff --git a/regression/goto-diff/java-tmp-vars-string/old.jar b/regression/goto-diff/java-tmp-vars-string/old.jar new file mode 100644 index 0000000000000000000000000000000000000000..bb988759ece858b6abc02758d01bd4625ef56213 GIT binary patch literal 757 zcmWIWW@Zs#;Nak3xRX4=hXDz2GO#fCx`sIFdiuHP|2xINz|0Wf&CUT*!30$nfK#&w zPz7AGucM!*n`>~0p0C?y-!rFuymj?1@_OrPojY@WbCAIm;|EWR^t^m^Jbf>gu43Vg zcp-U2dX|)C#t(5-wdYH;ES`&tJ`q=)#&9+JQ_;sFMzAaLcBwGA0PS!EV%)Ca0?LM@ z7MJKH=Oh*v_Xha-A94_xbA8&jD_UI~brWA4ZCJ73HQ zd^X`|e$ulbeARZA$4aj}oYqOUe6p(jka9;XZocH-eHRtpgv_%2sPd{-ul zJT&L)ZH)qrd7SS}b!r(wk-h2IiXeSP28Pc-9N^8!B*K82R$vJMlvYpyJn}&)2VE<2 t?154W0@wnXaIHw`2HgZ?hk;@l0S*J1h&T`MW@Q7(F$3XNAgu*}LP~ literal 0 HcmV?d00001 diff --git a/regression/goto-diff/java-tmp-vars-string/old/Test.java b/regression/goto-diff/java-tmp-vars-string/old/Test.java new file mode 100644 index 00000000000..685cf7f1544 --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-string/old/Test.java @@ -0,0 +1,11 @@ +public class Test { + public String f00(String x) { + String y = x; + return y; + } + + public String f01(String z) { + String w = z + "abc"; + return w; + } +} diff --git a/regression/goto-diff/java-tmp-vars-string/test.desc b/regression/goto-diff/java-tmp-vars-string/test.desc new file mode 100644 index 00000000000..f4cf78d370f --- /dev/null +++ b/regression/goto-diff/java-tmp-vars-string/test.desc @@ -0,0 +1,10 @@ +CORE +new.jar +old.jar +// Enable multi-line checking +activate-multi-line-match +EXIT=0 +SIGNAL=0 +new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(Ljava/lang/String;\)Ljava/lang/String;\ndeleted functions: +-- +^warning: ignoring From 0b3170d425ed5aa76e2c92c13cecae87098f271e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 17 Apr 2018 17:33:03 +0100 Subject: [PATCH 4/4] Stabilize clinit wrapper function type parameters Many accesses to the function type would add an ID_parameters if it is not there, which can cause inconsistencies in irep comparisons. --- src/java_bytecode/java_static_initializers.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/java_bytecode/java_static_initializers.cpp b/src/java_bytecode/java_static_initializers.cpp index 9cb9b054fea..aeac00275e6 100644 --- a/src/java_bytecode/java_static_initializers.cpp +++ b/src/java_bytecode/java_static_initializers.cpp @@ -114,6 +114,9 @@ static void create_clinit_wrapper_symbols( symbolt wrapper_method_symbol; code_typet wrapper_method_type; wrapper_method_type.return_type() = void_typet(); + // Ensure the parameters property is there + // to avoid trouble in irept comparisons + wrapper_method_type.parameters(); wrapper_method_symbol.name = clinit_wrapper_name(class_name); wrapper_method_symbol.pretty_name = wrapper_method_symbol.name; wrapper_method_symbol.base_name = "clinit_wrapper";