Skip to content

Commit 04c957d

Browse files
committed
Typecheck within assert and assume statements
For example, assert(some_string_literal!=null) would not work previously
1 parent 870e7ff commit 04c957d

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/java_bytecode/java_bytecode_typecheck_code.cpp

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,4 +67,8 @@ void java_bytecode_typecheckt::typecheck_code(codet &code)
6767
a_it++)
6868
typecheck_expr(*a_it);
6969
}
70+
else if(statement==ID_assert || statement==ID_assume)
71+
{
72+
typecheck_expr(code.op0());
73+
}
7074
}

0 commit comments

Comments
 (0)