Skip to content

Commit 64d2fc0

Browse files
author
Daniel Kroening
committed
use high-level numerical conversion
Direct access to the value of a constant_exprt is prone to error; the already existing functions should be used instead.
1 parent 35ee875 commit 64d2fc0

File tree

2 files changed

+8
-3
lines changed

2 files changed

+8
-3
lines changed

jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,9 @@ static const std::string get_thread_block_identifier(
8686
{
8787
PRECONDITION(f_code.arguments().size() == 1);
8888
const exprt &expr = f_code.arguments()[0];
89-
mp_integer lbl_id = bv2integer(expr.op0().get_string(ID_value), false);
89+
mp_integer lbl_id;
90+
if(to_integer(to_constant_expr(expr), lbl_id))
91+
CHECK_RETURN(false);
9092
return integer2string(lbl_id);
9193
}
9294

src/goto-programs/goto_convert.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1834,8 +1834,11 @@ bool goto_convertt::get_string_constant(
18341834
forall_operands(it, index_op)
18351835
if(it->is_constant())
18361836
{
1837-
unsigned long i = integer2ulong(
1838-
bv2integer(id2string(to_constant_expr(*it).get_value()), true));
1837+
mp_integer int_value;
1838+
if(to_integer(to_constant_expr(*it), int_value))
1839+
return true;
1840+
1841+
unsigned long i = integer2ulong(int_value);
18391842

18401843
if(i!=0) // to skip terminating 0
18411844
result+=static_cast<char>(i);

0 commit comments

Comments
 (0)