cprover
java_bytecode_typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
14 
15 #include <set>
16 #include <map>
17 
18 #include <util/symbol_table.h>
19 #include <util/typecheck.h>
20 #include <util/namespace.h>
21 #include <util/std_code.h>
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 
26  symbol_tablet &symbol_table,
27  message_handlert &message_handler,
28  bool string_refinement_enabled);
29 
31  exprt &expr,
32  message_handlert &message_handler,
33  const namespacet &ns);
34 
36 {
37 public:
39  symbol_tablet &_symbol_table,
40  message_handlert &_message_handler,
41  bool _string_refinement_enabled):
42  typecheckt(_message_handler),
43  symbol_table(_symbol_table),
45  string_refinement_enabled(_string_refinement_enabled)
46  {
47  }
48 
50 
51  virtual void typecheck();
52  virtual void typecheck_expr(exprt &expr);
53 
54 protected:
56  const namespacet ns;
58 
61  void typecheck_code(codet &);
62  void typecheck_type(typet &);
68 
69  // overload to use language-specific syntax
70  virtual std::string to_string(const exprt &expr);
71  virtual std::string to_string(const typet &type);
72 
73  std::set<irep_idt> already_typechecked;
74 };
75 
76 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
The type of an expression.
Definition: type.h:20
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
java_bytecode_typecheckt(symbol_tablet &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
virtual std::string to_string(const exprt &expr)
std::set< irep_idt > already_typechecked
Extract member of struct or union.
Definition: std_expr.h:3214
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Symbol table.
void typecheck_expr_java_new_array(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
API to type classes.
Base class for all expressions.
Definition: expr.h:46
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
An expression containing a side effect.
Definition: std_code.h:997
void typecheck_expr_java_new(side_effect_exprt &)
bool java_bytecode_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)