cprover
jsil_typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Jsil Language
4 
5 Author: 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/typecheck.h>
18 #include <util/namespace.h>
19 #include <util/std_code.h>
20 
21 class symbol_exprt;
22 class codet;
23 
24 bool jsil_typecheck(
25  symbol_tablet &symbol_table,
27 
28 bool jsil_typecheck(
29  exprt &expr,
31  const namespacet &ns);
32 
34 {
35 public:
37  symbol_tablet &_symbol_table,
38  message_handlert &_message_handler):
39  typecheckt(_message_handler),
40  symbol_table(_symbol_table),
42  proc_name()
43  {
44  }
45 
46  virtual ~jsil_typecheckt() { }
47 
48  virtual void typecheck();
49  virtual void typecheck_expr(exprt &expr);
50 
51 protected:
53  const namespacet ns;
54  // prefix to variables which is set in typecheck_declaration
56 
57  void update_expr_type(exprt &expr, const typet &type);
58  void make_type_compatible(exprt &expr, const typet &type, bool must);
59  void typecheck_type_symbol(symbolt &symbol) {}
60  void typecheck_non_type_symbol(symbolt &symbol);
61  void typecheck_symbol_expr(symbol_exprt &symbol_expr);
63  void typecheck_expr_delete(exprt &expr);
64  void typecheck_expr_index(exprt &expr);
66  void typecheck_expr_proto_obj(exprt &expr);
67  void typecheck_expr_has_field(exprt &expr);
68  void typecheck_expr_ref(exprt &expr);
69  void typecheck_expr_field(exprt &expr);
70  void typecheck_expr_base(exprt &expr);
71  void typecheck_expr_constant(exprt &expr);
73  void typecheck_expr_subtype(exprt &expr);
80  void typecheck_expr_unary_num(exprt &expr);
81  void typecheck_expr_operands(exprt &expr);
82  void typecheck_expr_main(exprt &expr);
83  void typecheck_code(codet &code);
84  void typecheck_function_call(code_function_callt &function_call);
85  void typecheck_return(code_returnt &code);
86  void typecheck_block(codet &code);
88  void typecheck_assign(code_assignt &code);
90  void typecheck_type(typet &type);
91  irep_idt add_prefix(const irep_idt &ds);
92 
93  // overload to use language-specific syntax
94  virtual std::string to_string(const exprt &expr);
95  virtual std::string to_string(const typet &type);
96 
97  std::unordered_set<irep_idt> already_typechecked;
98 };
99 
100 #endif // CPROVER_JSIL_JSIL_TYPECHECK_H
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_constant(exprt &expr)
The type of an expression.
Definition: type.h:22
jsil_typecheckt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void typecheck_expr_proto_obj(exprt &expr)
A try/catch block.
Definition: std_code.h:1621
void typecheck_expr_unary_num(exprt &expr)
void typecheck_expr_base(exprt &expr)
void typecheck_expr_ref(exprt &expr)
void typecheck_expr_binary_arith(exprt &expr)
void typecheck_assign(code_assignt &code)
const namespacet ns
void typecheck_expr_main(exprt &expr)
void typecheck_function_call(code_function_callt &function_call)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void typecheck_expr_side_effect_throw(side_effect_expr_throwt &expr)
A side effect that throws an exception.
Definition: std_code.h:1409
void typecheck_symbol_expr(symbol_exprt &symbol_expr)
irep_idt proc_name
void typecheck_exp_binary_equal(exprt &expr)
virtual std::string to_string(const exprt &expr)
irep_idt add_prefix(const irep_idt &ds)
Prefix parameters and variables with a procedure name.
void typecheck_expr_concatenation(exprt &expr)
void typecheck_code(codet &code)
void typecheck_non_type_symbol(symbolt &symbol)
typechecking procedure declaration; any other symbols should have been typechecked during typecheckin...
void typecheck_expr_unary_boolean(exprt &expr)
void typecheck_return(code_returnt &code)
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void typecheck_type_symbol(symbolt &symbol)
A function call.
Definition: std_code.h:828
void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_expr_subtype(exprt &expr)
void typecheck_expr_proto_field(exprt &expr)
virtual ~jsil_typecheckt()
void typecheck_type(typet &type)
void make_type_compatible(exprt &expr, const typet &type, bool must)
void typecheck_expr_unary_string(exprt &expr)
void typecheck_block(codet &code)
Base class for all expressions.
Definition: expr.h:42
void typecheck_expr_operands(exprt &expr)
bool jsil_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler)
symbol_tablet & symbol_table
An if-then-else.
Definition: std_code.h:461
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void typecheck_expr_delete(exprt &expr)
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:893
void typecheck_expr_binary_compare(exprt &expr)
void typecheck_ifthenelse(code_ifthenelset &code)
void typecheck_expr_field(exprt &expr)
Assignment.
Definition: std_code.h:195
void typecheck_expr_has_field(exprt &expr)
std::unordered_set< irep_idt > already_typechecked
void typecheck_try_catch(code_try_catcht &code)
virtual void typecheck()
void update_expr_type(exprt &expr, const typet &type)
void typecheck_expr_index(exprt &expr)