Skip to content

Commit 838aa80

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 5e84ac2 commit 838aa80

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-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: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1830,8 +1830,9 @@ 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+
const auto i = numeric_cast<std::size_t>(*it);
1834+
if(!i.has_value())
1835+
return true;
18351836

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

0 commit comments

Comments
 (0)