Skip to content

Commit 081f743

Browse files
author
Daniel Kroening
committed
use proper constructor for code_assertt
1 parent 8e44191 commit 081f743

File tree

1 file changed

+4
-3
lines changed

1 file changed

+4
-3
lines changed

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -604,13 +604,14 @@ void java_bytecode_instrument_uncaught_exceptions(
604604
const source_locationt &source_location)
605605
{
606606
// check that there is no uncaught exception
607-
code_assertt assert_no_exception;
608-
assert_no_exception.assertion() = equal_exprt(
607+
code_assertt assert_no_exception(equal_exprt(
609608
exc_symbol.symbol_expr(),
610-
null_pointer_exprt(to_pointer_type(exc_symbol.type)));
609+
null_pointer_exprt(to_pointer_type(exc_symbol.type))));
610+
611611
source_locationt assert_location = source_location;
612612
assert_location.set_comment("no uncaught exception");
613613
assert_no_exception.add_source_location() = assert_location;
614+
614615
init_code.move_to_operands(assert_no_exception);
615616
}
616617

0 commit comments

Comments
 (0)