CBMC
Loading...
Searching...
No Matches
java_bytecode_typecheck.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: JAVA Bytecode Conversion / Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include "expr2java.h"
15
17{
18 return expr2java(expr, ns);
19}
20
22{
23 return type2java(type, ns);
24}
25
32
34{
35 // The hash table iterators are not stable,
36 // and we might add new symbols.
38 identifiers.reserve(symbol_table.symbols.size());
39 for(const auto &symbol_pair : symbol_table.symbols)
40 identifiers.insert(symbol_pair.first);
41 typecheck(identifiers);
42}
43
46{
47 // We first check all type symbols,
48 // recursively doing base classes first.
49 for(const irep_idt &id : identifiers)
50 {
52 if(symbol.is_type)
54 }
55 // We now check all non-type symbols
56 for(const irep_idt &id : identifiers)
57 {
59 if(!symbol.is_type)
61 }
62}
63
65 symbol_table_baset &symbol_table,
66 message_handlert &message_handler,
67 bool string_refinement_enabled)
68{
70 symbol_table, message_handler, string_refinement_enabled);
71 return java_bytecode_typecheck.typecheck_main();
72}
73
75 journalling_symbol_tablet &symbol_table,
76 message_handlert &message_handler,
77 bool string_refinement_enabled)
78{
80 symbol_table, message_handler, string_refinement_enabled);
81 return java_bytecode_typecheck.typecheck(symbol_table.get_updated());
82}
83
85 exprt &expr,
86 message_handlert &message_handler,
87 const namespacet &ns)
88{
89#if 0
90 symbol_tablet symbol_table;
92
94 java_bytecode_parse_tree, symbol_table,
95 "", message_handler);
96
97 try
98 {
99 java_bytecode_typecheck.typecheck_expr(expr);
100 }
101
102 catch(int e)
103 {
105 }
106
107 catch(const char *e)
108 {
110 }
111
112 catch(const std::string &e)
113 {
115 }
116
117 return java_bytecode_typecheck.get_error_found();
118#else
119 // unused parameters
120 (void)expr;
121 (void)message_handler;
122 (void)ns;
123#endif
124
125 // fail for now
126 return true;
127}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr(exprt &expr)
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
const changesett & get_updated() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table base class interface.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
exprt value
Initial value of symbol.
Definition symbol.h:34
The type of an expression, extends irept.
Definition type.h:29
std::string type2java(const typet &type, const namespacet &ns)
std::string expr2java(const exprt &expr, const namespacet &ns)
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)
JAVA Bytecode Language Type Checking.
#define PRECONDITION(CONDITION)
Definition invariant.h:463