cprover
Loading...
Searching...
No Matches
jsil_typecheck.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Jsil Language
4
5Author: Michael Tautschnig, tautschn@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_JSIL_JSIL_TYPECHECK_H
13#define CPROVER_JSIL_JSIL_TYPECHECK_H
14
15#include <unordered_set>
16
17#include <util/namespace.h>
18#include <util/typecheck.h>
19
20class code_assignt;
24class code_try_catcht;
25class codet;
28class symbol_exprt;
29class symbol_tablet;
30
32 symbol_tablet &symbol_table,
33 message_handlert &message_handler);
34
36 exprt &expr,
37 message_handlert &message_handler,
38 const namespacet &ns);
39
41{
42public:
44 symbol_table_baset &_symbol_table,
45 message_handlert &_message_handler)
46 : typecheckt(_message_handler),
47 symbol_table(_symbol_table),
49 proc_name()
50 {
51 }
52
53 virtual ~jsil_typecheckt() { }
54
55 virtual void typecheck();
56 virtual void typecheck_expr(exprt &expr);
57
58protected:
61 // prefix to variables which is set in typecheck_declaration
63
64 void update_expr_type(exprt &expr, const typet &type);
65 void make_type_compatible(exprt &expr, const typet &type, bool must);
68 void typecheck_symbol_expr(symbol_exprt &symbol_expr);
70 void typecheck_expr_delete(exprt &expr);
71 void typecheck_expr_index(exprt &expr);
75 void typecheck_expr_ref(exprt &expr);
76 void typecheck_expr_field(exprt &expr);
77 void typecheck_expr_base(exprt &expr);
80 void typecheck_expr_subtype(exprt &expr);
89 void typecheck_expr_main(exprt &expr);
90 void typecheck_code(codet &code);
93 void typecheck_block(codet &code);
97 void typecheck_type(typet &type);
98 irep_idt add_prefix(const irep_idt &ds);
99
100 // overload to use language-specific syntax
101 virtual std::string to_string(const exprt &expr);
102 virtual std::string to_string(const typet &type);
103
104 std::unordered_set<irep_idt> already_typechecked;
105};
106
107#endif // CPROVER_JSIL_JSIL_TYPECHECK_H
A codet representing an assignment in the program.
codet representation of a "return from a function" statement.
Definition std_code.h:893
codet representation of a function call statement.
codet representation of an if-then-else statement.
Definition std_code.h:460
codet representation of a try/catch block.
Definition std_code.h:1986
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.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
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)
const namespacet ns
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)
virtual void typecheck()
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...
Definition namespace.h:91
A side_effect_exprt representation of a side effect that throws an exception.
Definition std_code.h:1757
Expression to hold a symbol (variable)
Definition std_expr.h:80
The symbol table base class interface.
The symbol table.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)