Skip to content

Commit 19ebb15

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 5eea667 commit 19ebb15

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

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

0 commit comments

Comments
 (0)