Skip to content

Commit 2cafd2a

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 163bc94 commit 2cafd2a

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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -86,7 +86,7 @@ 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+
const mp_integer lbl_id = numeric_cast_v<mp_integer>(expr.op0());
9090
return integer2string(lbl_id);
9191
}
9292

src/goto-programs/goto_convert.cpp

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1830,8 +1830,13 @@ bool goto_convertt::get_string_constant(
18301830
forall_operands(it, index_op)
18311831
if(it->is_constant())
18321832
{
1833-
unsigned long i = integer2ulong(
1834-
bv2integer(id2string(to_constant_expr(*it).get_value()), true));
1833+
mp_integer int_value;
1834+
if(to_integer(to_constant_expr(*it), int_value))
1835+
return true;
1836+
1837+
const auto i = numeric_cast<std::size_t>(*it);
1838+
if(!i.has_value())
1839+
return true;
18351840

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

0 commit comments

Comments
 (0)