Skip to content

Commit 5e2dd60

Browse files
author
Matthias Güdemann
committed
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 a3f20f2 commit 5e2dd60

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
@@ -1957,9 +1957,12 @@ codet java_bytecode_convert_methodt::convert_switch(
19571957
mp_integer number;
19581958
bool ret = to_integer(to_constant_expr(*a_it), number);
19591959
DATA_INVARIANT(!ret, "case label expected to be integer");
1960+
// The switch case does not contain any code, it just branches via a GOTO
1961+
// to the jump target of the tableswitch/lookupswitch case at
1962+
// hand. Therefore we consider this code to belong to the source bytecode
1963+
// instruction and not the target instruction.
19601964
code_case.code() = code_gotot(label(integer2string(number)));
1961-
code_case.code().add_source_location() =
1962-
address_map.at(integer2unsigned(number)).source->source_location;
1965+
code_case.code().add_source_location() = location;
19631966

19641967
if(a_it == args.begin())
19651968
code_case.set_default();

0 commit comments

Comments
 (0)