12#ifndef CPROVER_JSIL_JSIL_TYPECHECK_H
13#define CPROVER_JSIL_JSIL_TYPECHECK_H
15#include <unordered_set>
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A goto_instruction_codet representing an assignment in the program.
codet representation of a "return from a function" statement.
goto_instruction_codet representation of a function call statement.
codet representation of an if-then-else statement.
codet representation of a try/catch block.
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
void typecheck_expr_binary_arith(exprt &expr)
void typecheck_expr_constant(exprt &expr)
void typecheck_expr_has_field(exprt &expr)
void typecheck_expr_main(exprt &expr)
void typecheck_type_symbol(symbolt &)
void typecheck_function_call(code_function_callt &function_call)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_try_catch(code_try_catcht &code)
void typecheck_assign(code_assignt &code)
symbol_table_baset & symbol_table
void typecheck_expr_index(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_subtype(exprt &expr)
void typecheck_expr_ref(exprt &expr)
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_concatenation(exprt &expr)
jsil_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler)
void typecheck_expr_field(exprt &expr)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_code(codet &code)
virtual std::string to_string(const exprt &expr)
std::unordered_set< irep_idt > already_typechecked
void make_type_compatible(exprt &expr, const typet &type, bool must)
void typecheck_exp_binary_equal(exprt &expr)
void typecheck_expr_operands(exprt &expr)
void typecheck_expr_base(exprt &expr)
void typecheck_expr_delete(exprt &expr)
void typecheck_expr_proto_obj(exprt &expr)
virtual ~jsil_typecheckt()
void typecheck_block(codet &code)
void typecheck_expr_unary_num(exprt &expr)
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
void typecheck_type(typet &type)
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void update_expr_type(exprt &expr, const typet &type)
void typecheck_return(code_frontend_returnt &)
void typecheck_expr_binary_compare(exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
A side_effect_exprt representation of a side effect that throws an exception.
Expression to hold a symbol (variable)
The symbol table base class interface.
The type of an expression, extends irept.
bool jsil_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler)