cprover
java_bytecode_parse_tree.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
12 
13 #include <set>
14 
15 #include <util/std_code.h>
16 #include <util/std_types.h>
17 
18 #include "bytecode_info.h"
19 
21 {
22 public:
24  {
25  public:
27 
29  {
30  public:
33  void output(std::ostream &) const;
34  };
35 
36  typedef std::vector<element_value_pairt> element_value_pairst;
38 
39  void output(std::ostream &) const;
40  };
41 
42  typedef std::vector<annotationt> annotationst;
43 
45  {
46  public:
48  unsigned address;
50  typedef std::vector<exprt> argst;
52  };
53 
54  class membert
55  {
56  public:
57  std::string signature;
61 
62  virtual void output(std::ostream &out) const = 0;
63 
65  is_public(false), is_protected(false), is_private(false),
66  is_static(false), is_final(false)
67  {
68  }
69  };
70 
71  class methodt:public membert
72  {
73  public:
77 
78  typedef std::vector<instructiont> instructionst;
80 
82  {
83  instructions.push_back(instructiont());
84  return instructions.back();
85  }
86 
87  struct exceptiont
88  {
89  public:
90  std::size_t start_pc;
91  std::size_t end_pc;
92  std::size_t handler_pc;
94  };
95 
96  typedef std::vector<exceptiont> exception_tablet;
98 
100  {
101  public:
103  std::string signature;
104  std::size_t index;
105  std::size_t start_pc;
106  std::size_t length;
107  };
108 
109  typedef std::vector<local_variablet> local_variable_tablet;
111 
113  {
114  public:
122  };
123 
125  {
126  public:
128  {
131  };
133  size_t offset_delta;
134  size_t chops;
135  size_t appends;
136 
137  typedef std::vector<verification_type_infot>
139  typedef std::vector<verification_type_infot>
141 
144  };
145 
146  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
148 
149  virtual void output(std::ostream &out) const;
150 
152  is_native(false),
153  is_abstract(false),
154  is_synchronized(false)
155  {
156  }
157  };
158 
159  class fieldt:public membert
160  {
161  public:
162  virtual void output(std::ostream &out) const;
163  bool is_enum;
164  };
165 
166  class classt
167  {
168  public:
170  bool is_abstract=false;
171  bool is_enum=false;
172  size_t enum_elements=0;
173 
174  typedef std::list<irep_idt> implementst;
176 
177  typedef std::list<fieldt> fieldst;
178  typedef std::list<methodt> methodst;
182 
184  {
185  fields.push_back(fieldt());
186  return fields.back();
187  }
188 
190  {
191  methods.push_back(methodt());
192  return methods.back();
193  }
194 
195  void output(std::ostream &out) const;
196 
197  void swap(classt &other);
198  };
199 
201 
203  {
205  other.class_refs.swap(class_refs);
206  std::swap(loading_successful, other.loading_successful);
207  }
208 
209  void output(std::ostream &out) const;
210 
211  typedef std::set<irep_idt> class_refst;
213 
215 
217  {
218  }
219 };
220 
221 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
The type of an expression.
Definition: type.h:20
virtual void output(std::ostream &out) const =0
virtual void output(std::ostream &out) const
std::vector< annotationt > annotationst
A reference into the symbol table.
Definition: std_types.h:109
std::vector< verification_type_infot > stack_verification_type_infot
void output(std::ostream &out) const
std::vector< instructiont > instructionst
uint16_t u2
Definition: bytecode_info.h:56
std::vector< verification_type_infot > local_verification_type_infot
void output(std::ostream &out) const
std::vector< element_value_pairt > element_value_pairst
API to type classes.
std::vector< exceptiont > exception_tablet
std::vector< stack_map_table_entryt > stack_map_tablet
uint8_t u1
Definition: bytecode_info.h:55
Base class for all expressions.
Definition: expr.h:46
void swap(java_bytecode_parse_treet &other)
std::vector< local_variablet > local_variable_tablet
virtual void output(std::ostream &out) const