12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H 13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H 30 bool string_refinement_enabled);
33 journalling_symbol_tablet &symbol_table,
35 bool string_refinement_enabled);
48 bool _string_refinement_enabled):
59 void typecheck(
const journalling_symbol_tablet::changesett &identifiers);
83 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H void typecheck_non_type_symbol(symbolt &)
The type of an expression.
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void typecheck_type(typet &)
void typecheck_type_symbol(symbolt &)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
virtual std::string to_string(const exprt &expr)
std::set< irep_idt > already_typechecked
Extract member of struct or union.
java_bytecode_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
symbol_table_baset & symbol_table
void typecheck_code(codet &)
API to expression classes.
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Base class for all expressions.
virtual ~java_bytecode_typecheckt()
The symbol table base class interface.
Expression to hold a symbol (variable)
goto_programt coverage_criteriont message_handlert & message_handler
void typecheck_expr_member(member_exprt &)
A statement in a programming language.
An expression containing a side effect.
void typecheck_expr_java_new(side_effect_exprt &)
void typecheck_expr_symbol(symbol_exprt &)
bool string_refinement_enabled