Skip to content

Commit cb90b89

Browse files
author
Daniel Kroening
committed
use new messaging API in Java typechecker
1 parent b05f4c1 commit cb90b89

File tree

2 files changed

+2
-7
lines changed

2 files changed

+2
-7
lines changed

src/java_bytecode/java_bytecode_typecheck.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,13 +27,13 @@ bool java_bytecode_typecheck(
2727
message_handlert &message_handler,
2828
const namespacet &ns);
2929

30-
class java_bytecode_typecheckt:public legacy_typecheckt
30+
class java_bytecode_typecheckt:public typecheckt
3131
{
3232
public:
3333
java_bytecode_typecheckt(
3434
symbol_tablet &_symbol_table,
3535
message_handlert &_message_handler):
36-
legacy_typecheckt(_message_handler),
36+
typecheckt(_message_handler),
3737
symbol_table(_symbol_table),
3838
ns(symbol_table)
3939
{

src/java_bytecode/java_bytecode_typecheck_expr.cpp

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -191,14 +191,9 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
191191
expr.struct_op()=m;
192192
}
193193

194-
#if 0
195194
warning().source_location=expr.source_location();
196195
warning() << "failed to find field `"
197196
<< component_name << "` in class hierarchy" << eom;
198-
#else
199-
warning_msg("failed to find field `"+
200-
id2string(component_name)+"` in class hierarchy");
201-
#endif
202197

203198
// We replace by a non-det of same type
204199
side_effect_expr_nondett nondet(expr.type());

0 commit comments

Comments
 (0)