diff --git a/regression/cbmc-java/LocalVarTable2/LocalVarTable2.class b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.class new file mode 100644 index 00000000000..3191b63267e Binary files /dev/null and b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.class differ diff --git a/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java new file mode 100644 index 00000000000..9d32afe52a8 --- /dev/null +++ b/regression/cbmc-java/LocalVarTable2/LocalVarTable2.java @@ -0,0 +1,19 @@ +// Must compile this with -g (produces LocalVarTable) to exhibit bug. + +public class LocalVarTable2 { + + public static Object f() { + for(int i = 0; i < 10; ++i) { System.out.printf("Count %d\n", i); } + try { + return new Object(); + } + finally { + System.out.println("Finally executed\n"); + } + } + + public static void main(String[] args) { + f(); + } + +} diff --git a/regression/cbmc-java/LocalVarTable2/test.desc b/regression/cbmc-java/LocalVarTable2/test.desc new file mode 100644 index 00000000000..1e982eeac10 --- /dev/null +++ b/regression/cbmc-java/LocalVarTable2/test.desc @@ -0,0 +1,7 @@ +CORE +LocalVarTable2.class +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +-- +return_value.*(void \*)i diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 20a97d0f031..699c6556b80 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -99,35 +99,22 @@ class java_bytecode_convert_methodt:public messaget variablet &find_variable_for_slot(unsigned number_int, size_t address, variablest &var_list, instruction_sizet inst_size) { - size_t var_list_length = var_list.size(); - if(var_list_length > 1) - { - for(variablet &var : var_list) - { - size_t start_pc = var.start_pc; - size_t length = var.length; - if (address + (size_t) inst_size >= start_pc && address < start_pc + length) - return var; - } - // add unnamed local variable to end of list at this index - // with scope from 0 to INT_MAX - // as it is at the end of the vector, it will only be taken into account - // if no other variable is valid - size_t list_length = var_list.size(); - var_list.resize(list_length + 1); - var_list[list_length].start_pc = 0; - var_list[list_length].length = std::numeric_limits::max(); - return var_list[list_length]; - } - else if(var_list_length == 1) - return var_list[0]; - else - { - // return reference to unnamed local variable - // if no local variable is defined for this index - var_list.resize(1); - return var_list[0]; - } + for(variablet &var : var_list) + { + size_t start_pc = var.start_pc; + size_t length = var.length; + if (address + (size_t) inst_size >= start_pc && address < start_pc + length) + return var; + } + // add unnamed local variable to end of list at this index + // with scope from 0 to INT_MAX + // as it is at the end of the vector, it will only be taken into account + // if no other variable is valid + size_t list_length = var_list.size(); + var_list.resize(list_length + 1); + var_list[list_length].start_pc = 0; + var_list[list_length].length = std::numeric_limits::max(); + return var_list[list_length]; } // JVM local variables @@ -375,6 +362,8 @@ void java_bytecode_convert_methodt::convert( // add as a JVM variable std::size_t slots=get_variable_slots(parameters[i]); variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr(); + variables[param_index][0].start_pc=0; + variables[param_index][0].length = std::numeric_limits::max(); param_index+=slots; }