Skip to content

Commit 653d887

Browse files
Remove wrong assumption from goto check
The argument of throw might be null even if it is of type java.lang.AssertionError.
1 parent 07acde4 commit 653d887

File tree

1 file changed

+9
-14
lines changed

1 file changed

+9
-14
lines changed

src/analyses/goto_check.cpp

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1627,21 +1627,16 @@ void goto_checkt::goto_check(
16271627

16281628
exprt pointer=i.code.op0().op0();
16291629

1630-
if(pointer.type().subtype().get(ID_identifier)!=
1631-
"java::java.lang.AssertionError")
1632-
{
1633-
notequal_exprt not_eq_null(
1634-
pointer,
1635-
null_pointer_exprt(to_pointer_type(pointer.type())));
1630+
const notequal_exprt not_eq_null(
1631+
pointer, null_pointer_exprt(to_pointer_type(pointer.type())));
16361632

1637-
add_guarded_claim(
1638-
not_eq_null,
1639-
"throwing null",
1640-
"pointer dereference",
1641-
i.source_location,
1642-
pointer,
1643-
guardt());
1644-
}
1633+
add_guarded_claim(
1634+
not_eq_null,
1635+
"throwing null",
1636+
"pointer dereference",
1637+
i.source_location,
1638+
pointer,
1639+
guardt());
16451640
}
16461641

16471642
// this has no successor

0 commit comments

Comments
 (0)