Skip to content

Commit 9ed4722

Browse files
Matthias Güdemannsmowton
Matthias Güdemann
authored andcommitted
Change source location of jump target in {table|lookup}switch
Before we considered the `code_switch_caset` to belong to the target instruction which lead to uncoverable goals of the form: IF condition 1 then GOTO 1 ... 1: GOTO 2 ASSERT false // uncoverable block ... 2:
1 parent 882e202 commit 9ed4722

File tree

1 file changed

+5
-2
lines changed

1 file changed

+5
-2
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1959,9 +1959,12 @@ codet java_bytecode_convert_methodt::convert_switch(
19591959
mp_integer number;
19601960
bool ret = to_integer(to_constant_expr(*a_it), number);
19611961
DATA_INVARIANT(!ret, "case label expected to be integer");
1962+
// The switch case does not contain any code, it just branches via a GOTO
1963+
// to the jump target of the tableswitch/lookupswitch case at
1964+
// hand. Therefore we consider this code to belong to the source bytecode
1965+
// instruction and not the target instruction.
19621966
code_case.code() = code_gotot(label(integer2string(number)));
1963-
code_case.code().add_source_location() =
1964-
address_map.at(integer2unsigned(number)).source->source_location;
1967+
code_case.code().add_source_location() = location;
19651968

19661969
if(a_it == args.begin())
19671970
code_case.set_default();

0 commit comments

Comments
 (0)