40 identifiers.insert(symbol_pair.first);
49 for(
const irep_idt &
id : identifiers)
56 for(
const irep_idt &
id : identifiers)
67 bool string_refinement_enabled)
70 symbol_table, message_handler, string_refinement_enabled);
77 bool string_refinement_enabled)
80 symbol_table, message_handler, string_refinement_enabled);
94 java_bytecode_parse_tree, symbol_table,
112 catch(
const std::string &e)
121 (void)message_handler;
Base class for all expressions.
void typecheck_type_symbol(symbolt &)
void typecheck_type(typet &)
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr(exprt &expr)
void typecheck_non_type_symbol(symbolt &)
symbol_table_baset & symbol_table
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
std::unordered_set< irep_idt > changesett
const changesett & get_updated() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The symbol table base class interface.
typet type
Type of symbol.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
JAVA Bytecode Language Type Checking.
#define PRECONDITION(CONDITION)