@@ -1558,6 +1558,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1558
1558
code_blockt block;
1559
1559
if (throw_runtime_exceptions)
1560
1560
{
1561
+ // throw NullPointerException if necessary
1561
1562
codet null_dereference_check=
1562
1563
throw_null_dereference_exception (
1563
1564
op[0 ],
@@ -1566,6 +1567,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
1566
1567
}
1567
1568
else
1568
1569
{
1570
+ // add assertion
1569
1571
const typecast_exprt lhs (op[0 ], pointer_typet (empty_typet ()));
1570
1572
const exprt rhs (null_pointer_exprt (to_pointer_type (lhs.type ())));
1571
1573
const exprt not_equal_null (
@@ -1596,12 +1598,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
1596
1598
1597
1599
if (throw_runtime_exceptions)
1598
1600
{
1601
+ // throw ClassCastException
1599
1602
codet conditional_check=
1600
1603
throw_class_cast_exception (op[0 ], arg0, i_it->source_location );
1601
1604
c=std::move (conditional_check);
1602
1605
}
1603
1606
else
1604
1607
{
1608
+ // add assertion
1605
1609
binary_predicate_exprt check (op[0 ], ID_java_instanceof, arg0);
1606
1610
code_assertt assert_class (check);
1607
1611
assert_class.add_source_location ().
@@ -2334,6 +2338,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
2334
2338
assert (op.size ()==1 && results.size ()==1 );
2335
2339
if (throw_runtime_exceptions)
2336
2340
{
2341
+ // throw NullPointerException if necessary
2337
2342
codet null_dereference_check=
2338
2343
throw_null_dereference_exception (
2339
2344
op[0 ],
@@ -2369,6 +2374,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
2369
2374
assert (op.size ()==2 && results.size ()==0 );
2370
2375
if (throw_runtime_exceptions)
2371
2376
{
2377
+ // throw NullPointerException if necessary
2372
2378
codet null_dereference_check=
2373
2379
throw_null_dereference_exception (
2374
2380
op[0 ],
0 commit comments