12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H 13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H 28 bool string_refinement_enabled);
41 bool _string_refinement_enabled):
76 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H void typecheck_non_type_symbol(symbolt &)
The type of an expression.
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...
java_bytecode_typecheckt(symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
virtual std::string to_string(const exprt &expr)
std::set< irep_idt > already_typechecked
Extract member of struct or union.
void typecheck_code(codet &)
API to expression classes.
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
symbol_tablet & symbol_table
Base class for all expressions.
virtual ~java_bytecode_typecheckt()
Expression to hold a symbol (variable)
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 java_bytecode_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
bool string_refinement_enabled
void typecheck_expr_java_string_literal(exprt &)