Skip to content

Commit e4ac6e2

Browse files
author
thk123
committed
Modified definition of abstract to not fall over on void* types
Exception pointers are generated as a pointer_typet(empty_typet()) rather than a pointer to a struct. These shouldn't be considered abstract.
1 parent 2c79f51 commit e4ac6e2

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/java_bytecode/select_pointer_type.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,12 @@ bool select_pointer_typet::is_abstract_type(
5151
const pointer_typet &pointer_type) const
5252
{
5353
const typet &pointing_to_type=ns.follow(pointer_type.subtype());
54+
55+
// void* pointers should be not considered abstract
56+
// These happen in Java when initializing the exeception value.
57+
if(pointing_to_type.id()==ID_empty)
58+
return false;
59+
5460
INVARIANT(
5561
pointing_to_type.id()==ID_struct,
5662
"All pointers in Java should be to classes");

0 commit comments

Comments
 (0)