Skip to content

Commit 54285dd

Browse files
author
Daniel Kroening
committed
use proper constructor for code_assertt
1 parent ff487f0 commit 54285dd

File tree

1 file changed

+6
-4
lines changed

1 file changed

+6
-4
lines changed

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -604,13 +604,15 @@ 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(
609-
exc_symbol.symbol_expr(),
610-
null_pointer_exprt(to_pointer_type(exc_symbol.type)));
607+
code_assertt assert_no_exception(
608+
equal_exprt(
609+
exc_symbol.symbol_expr(),
610+
null_pointer_exprt(to_pointer_type(exc_symbol.type))));
611+
611612
source_locationt assert_location = source_location;
612613
assert_location.set_comment("no uncaught exception");
613614
assert_no_exception.add_source_location() = assert_location;
615+
614616
init_code.move_to_operands(assert_no_exception);
615617
}
616618

0 commit comments

Comments
 (0)