Skip to content

Commit 0c74e6d

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 70887e2 commit 0c74e6d

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

19601963
if(a_it == args.begin())
19611964
code_case.set_default();

0 commit comments

Comments
 (0)