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 "java_types.h"
16 
17 #include <set>
18 #include <map>
19 
21 #include <util/typecheck.h>
22 #include <util/namespace.h>
23 #include <util/std_code.h>
24 #include <util/std_expr.h>
25 #include <util/std_types.h>
26 
28  symbol_table_baset &symbol_table,
29  message_handlert &message_handler,
30  bool string_refinement_enabled);
31 
33  journalling_symbol_tablet &symbol_table,
34  message_handlert &message_handler,
35  bool string_refinement_enabled);
36 
38  exprt &expr,
39  message_handlert &message_handler,
40  const namespacet &ns);
41 
43 {
44 public:
46  symbol_table_baset &_symbol_table,
47  message_handlert &_message_handler,
48  bool _string_refinement_enabled):
49  typecheckt(_message_handler),
50  symbol_table(_symbol_table),
52  string_refinement_enabled(_string_refinement_enabled)
53  {
54  }
55 
57 
58  virtual void typecheck();
59  void typecheck(const journalling_symbol_tablet::changesett &identifiers);
60  virtual void typecheck_expr(exprt &expr);
61 
62 protected:
64  const namespacet ns;
66 
69  void typecheck_code(codet &);
70  void typecheck_type(typet &);
74 
75  // overload to use language-specific syntax
76  virtual std::string to_string(const exprt &expr);
77  virtual std::string to_string(const typet &type);
78 
79  std::set<irep_idt> already_typechecked;
80 };
81 
82 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
java_bytecode_typecheckt::~java_bytecode_typecheckt
virtual ~java_bytecode_typecheckt()
Definition: java_bytecode_typecheck.h:56
java_bytecode_typecheckt::typecheck_expr_java_new
void typecheck_expr_java_new(side_effect_exprt &)
Definition: java_bytecode_typecheck_expr.cpp:59
java_bytecode_typecheckt::java_bytecode_typecheckt
java_bytecode_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
Definition: java_bytecode_typecheck.h:45
java_bytecode_typecheckt::to_string
virtual std::string to_string(const exprt &expr)
Definition: java_bytecode_typecheck.cpp:20
typet
The type of an expression, extends irept.
Definition: type.h:29
java_bytecode_typecheckt::typecheck_code
void typecheck_code(codet &)
Definition: java_bytecode_typecheck_code.cpp:14
exprt
Base class for all expressions.
Definition: expr.h:53
journalling_symbol_table.h
Author: Diffblue Ltd.
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
java_bytecode_typecheckt::typecheck_type
void typecheck_type(typet &)
Definition: java_bytecode_typecheck_type.cpp:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_bytecode_typecheckt::typecheck_type_symbol
void typecheck_type_symbol(symbolt &)
Definition: java_bytecode_typecheck_type.cpp:53
java_bytecode_typecheckt::ns
const namespacet ns
Definition: java_bytecode_typecheck.h:64
typecheck.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_types.h
Pre-defined types.
journalling_symbol_tablet::changesett
std::unordered_set< irep_idt > changesett
Definition: journalling_symbol_table.h:38
java_bytecode_typecheckt::symbol_table
symbol_table_baset & symbol_table
Definition: java_bytecode_typecheck.h:63
message_handlert
Definition: message.h:28
java_bytecode_typecheckt::string_refinement_enabled
bool string_refinement_enabled
Definition: java_bytecode_typecheck.h:65
std_code.h
java_bytecode_typecheckt::typecheck_non_type_symbol
void typecheck_non_type_symbol(symbolt &)
Definition: java_bytecode_typecheck.cpp:30
java_bytecode_typecheckt::typecheck_expr_symbol
void typecheck_expr_symbol(symbol_exprt &)
Definition: java_bytecode_typecheck_expr.cpp:74
java_bytecode_typecheckt::typecheck
virtual void typecheck()
Definition: java_bytecode_typecheck.cpp:37
java_bytecode_typecheckt
Definition: java_bytecode_typecheck.h:43
java_bytecode_typecheck
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:68
java_bytecode_typecheckt::already_typechecked
std::set< irep_idt > already_typechecked
Definition: java_bytecode_typecheck.h:79
symbolt
Symbol table entry.
Definition: symbol.h:28
java_bytecode_typecheckt::typecheck_expr_java_new_array
void typecheck_expr_java_new_array(side_effect_exprt &)
Definition: java_bytecode_typecheck_expr.cpp:66
typecheckt
Definition: typecheck.h:17
java_types.h
std_expr.h
API to expression classes.
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
java_bytecode_typecheck_updated_symbols
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Definition: java_bytecode_typecheck.cpp:78
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
java_bytecode_typecheckt::typecheck_expr
virtual void typecheck_expr(exprt &expr)
Definition: java_bytecode_typecheck_expr.cpp:26
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35