CBMC
Loading...
Searching...
No Matches
java_bytecode_typecheck.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Language Type Checking
4
5Author: 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
18#include <util/typecheck.h>
19#include <util/namespace.h>
20
21class codet;
23
25 symbol_table_baset &symbol_table,
26 message_handlert &message_handler,
27 bool string_refinement_enabled);
28
30 journalling_symbol_tablet &symbol_table,
31 message_handlert &message_handler,
32 bool string_refinement_enabled);
33
35 exprt &expr,
36 message_handlert &message_handler,
37 const namespacet &ns);
38
40{
41public:
52
54
55 virtual void typecheck();
56 void typecheck(const journalling_symbol_tablet::changesett &identifiers);
57 virtual void typecheck_expr(exprt &expr);
58
59protected:
63
66 void typecheck_code(codet &);
67 void typecheck_type(typet &);
71
72 // overload to use language-specific syntax
73 virtual std::string to_string(const exprt &expr);
74 virtual std::string to_string(const typet &type);
75
76 std::set<irep_idt> already_typechecked;
77};
78
79#endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
Definition expr.h:56
std::set< irep_idt > already_typechecked
virtual std::string to_string(const exprt &expr)
java_bytecode_typecheckt(symbol_table_baset &_symbol_table, message_handlert &_message_handler, bool _string_refinement_enabled)
void typecheck_expr_java_new(side_effect_exprt &)
virtual void typecheck_expr(exprt &expr)
void typecheck_expr_java_new_array(side_effect_exprt &)
symbol_table_baset & symbol_table
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
std::unordered_set< irep_idt > changesett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
An expression containing a side effect.
Definition std_code.h:1450
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
bool java_bytecode_typecheck(symbol_table_baset &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
void java_bytecode_typecheck_updated_symbols(journalling_symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
Author: Diffblue Ltd.