44 identifiers.insert(symbol_pair.first);
53 for(
const irep_idt &
id : identifiers)
60 for(
const irep_idt &
id : identifiers)
71 bool string_refinement_enabled)
74 symbol_table, message_handler, string_refinement_enabled);
81 bool string_refinement_enabled)
84 symbol_table, message_handler, string_refinement_enabled);
98 java_bytecode_parse_tree, symbol_table,
116 catch(
const std::string &e)
125 (void)message_handler;
void typecheck_non_type_symbol(symbolt &)
The type of an expression, extends irept.
std::string type2java(const typet &type, const namespacet &ns)
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void typecheck_type(typet &)
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
exprt value
Initial value of symbol.
void typecheck_type_symbol(symbolt &)
virtual std::string to_string(const exprt &expr)
JAVA Bytecode Language Type Checking.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
symbol_table_baset & symbol_table
const changesett & get_updated() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void typecheck_expr(exprt &expr)
typet type
Type of symbol.
Base class for all expressions.
The symbol table base class interface.
std::unordered_set< irep_idt > changesett
std::string expr2java(const exprt &expr, const namespacet &ns)