cprover
java_bytecode_typecheck.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: JAVA Bytecode Conversion / Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/std_types.h>
15 #include <util/prefix.h>
16 #include <util/config.h>
17 
18 #include "expr2java.h"
19 
21 {
22  return expr2java(expr, ns);
23 }
24 
26 {
27  return type2java(type, ns);
28 }
29 
31 {
32  assert(!symbol.is_type);
33  typecheck_type(symbol.type);
34  typecheck_expr(symbol.value);
35 }
36 
38 {
39  // The hash table iterators are not stable,
40  // and we might add new symbols.
41 
42  std::vector<irep_idt> identifiers;
43  identifiers.reserve(symbol_table.symbols.size());
45  identifiers.push_back(s_it->first);
46 
47  // We first check all type symbols,
48  // recursively doing base classes first.
49  for(const irep_idt &id : identifiers)
50  {
51  symbolt &symbol=symbol_table.symbols[id];
52 
53  if(!symbol.is_type)
54  continue;
55 
56  typecheck_type_symbol(symbol);
57  }
58 
59  // We now check all non-type symbols
60  for(const irep_idt &id : identifiers)
61  {
62  symbolt &symbol=symbol_table.symbols[id];
63 
64  if(symbol.is_type)
65  continue;
66 
68  }
69 }
70 
75 {
77  symbol_table, message_handler, string_refinement_enabled);
78  return java_bytecode_typecheck.typecheck_main();
79 }
80 
82  exprt &expr,
84  const namespacet &ns)
85 {
86  #if 0
88  java_bytecode_parse_treet java_bytecode_parse_tree;
89 
91  java_bytecode_parse_tree, symbol_table,
92  "", message_handler);
93 
94  try
95  {
96  java_bytecode_typecheck.typecheck_expr(expr);
97  }
98 
99  catch(int e)
100  {
101  java_bytecode_typecheck.error();
102  }
103 
104  catch(const char *e)
105  {
106  java_bytecode_typecheck.error(e);
107  }
108 
109  catch(const std::string &e)
110  {
111  java_bytecode_typecheck.error(e);
112  }
113 
114  return java_bytecode_typecheck.get_error_found();
115  #endif
116 
117  // fail for now
118  return true;
119 }
The type of an expression.
Definition: type.h:20
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:438
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
exprt value
Initial value of symbol.
Definition: symbol.h:40
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual std::string to_string(const exprt &expr)
JAVA Bytecode Language Type Checking.
symbolst symbols
Definition: symbol_table.h:57
bool java_bytecode_typecheck(symbol_tablet &symbol_table, message_handlert &message_handler, bool string_refinement_enabled)
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void typecheck_expr(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:37
API to type classes.
Base class for all expressions.
Definition: expr.h:46
mstreamt & error()
Definition: message.h:223
bool is_type
Definition: symbol.h:66
message_handlert * message_handler
Definition: message.h:259
virtual bool typecheck_main()
Definition: typecheck.cpp:12
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:431