From 1d5c4b120f67662a3b47088fa6d8f09e05780b30 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Feb 2022 14:25:59 +0000 Subject: [PATCH] Java front-end: fix vector index type in populate_live_range_holes CodeQL rightly complained that there is comparison using a more narrow type on the left-hand side of a less-than in a loop condition, which may give rise to a non-terminating loop in case of integer overflow. While at it, also add checks before unconditionally accessing the first element. --- jbmc/src/java_bytecode/java_local_variable_table.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index e40fa80b410..2a2f3d5d128 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -513,18 +513,18 @@ static void populate_live_range_holes( merge_vars.begin(), merge_vars.end()); std::sort(sorted_by_startpc.begin(), sorted_by_startpc.end(), lt_startpc); + PRECONDITION(!sorted_by_startpc.empty()); maybe_add_hole( merge_into, expanded_live_range_start, sorted_by_startpc[0]->var.start_pc); - for(java_bytecode_convert_methodt::method_offsett idx = 0; - idx < sorted_by_startpc.size() - 1; - ++idx) + for(auto it = std::next(sorted_by_startpc.begin()); + it != sorted_by_startpc.end(); + ++it) { + auto &local_var = (*std::prev(it))->var; maybe_add_hole( - merge_into, - sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->var.length, - sorted_by_startpc[idx+1]->var.start_pc); + merge_into, local_var.start_pc + local_var.length, (*it)->var.start_pc); } }