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 #include <map>
15 
16 #include <util/optional.h>
17 #include <util/std_code.h>
18 #include <util/std_types.h>
19 
20 #include "bytecode_info.h"
21 
23 {
24  // Disallow copy construction and copy assignment, but allow move construction
25  // and move assignment.
31 
32  struct annotationt
33  {
35 
37  {
40  void output(std::ostream &) const;
41  };
42 
43  typedef std::vector<element_value_pairt> element_value_pairst;
45 
46  void output(std::ostream &) const;
47  };
48 
49  typedef std::vector<annotationt> annotationst;
50 
52  const annotationst &annotations,
53  const irep_idt &annotation_type_name);
54 
55  struct instructiont
56  {
58  unsigned address;
60  typedef std::vector<exprt> argst;
62  };
63 
64  struct membert
65  {
66  std::string descriptor;
71 
73  is_public(false), is_protected(false),
74  is_private(false), is_static(false), is_final(false)
75  {
76  }
77 
78  bool has_annotation(const irep_idt &annotation_id) const
79  {
80  return find_annotation(annotations, annotation_id).has_value();
81  }
82  };
83 
84  struct methodt : public membert
85  {
87  bool is_native = false, is_abstract = false, is_synchronized = false,
88  is_bridge = false, is_varargs = false, is_synthetic = false;
90 
91  typedef std::vector<instructiont> instructionst;
93 
95  {
96  instructions.push_back(instructiont());
97  return instructions.back();
98  }
99 
106  std::vector<annotationst> parameter_annotations;
107 
108  struct exceptiont
109  {
111  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
112  {
113  }
114 
115  std::size_t start_pc;
116  std::size_t end_pc;
117  std::size_t handler_pc;
119  };
120 
121  typedef std::vector<exceptiont> exception_tablet;
123 
124  std::vector<irep_idt> throws_exception_table;
125 
127  {
129  std::string descriptor;
131  std::size_t index;
132  std::size_t start_pc;
133  std::size_t length;
134  };
135 
136  typedef std::vector<local_variablet> local_variable_tablet;
138 
140  {
148  };
149 
151  {
153  {
156  };
158  size_t offset_delta;
159  size_t chops;
160  size_t appends;
161 
162  typedef std::vector<verification_type_infot>
164  typedef std::vector<verification_type_infot>
166 
169  };
170 
171  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
173 
174  void output(std::ostream &out) const;
175 
177  : is_native(false),
178  is_abstract(false),
179  is_synchronized(false),
180  is_bridge(false)
181  {
182  }
183  };
184 
185  struct fieldt : public membert
186  {
187  bool is_enum;
188 
189  void output(std::ostream &out) const;
190 
191  fieldt() : is_enum(false)
192  {
193  }
194  };
195 
196  struct classt
197  {
198  classt() = default;
199 
201  explicit classt(const irep_idt &name) : name(name)
202  {
203  }
204 
205  // Disallow copy construction and copy assignment, but allow move
206  // construction and move assignment.
207  classt(const classt &) = delete;
208  classt &operator=(const classt &) = delete;
209  classt(classt &&) = default;
210  classt &operator=(classt &&) = default;
211 
213  bool is_abstract=false;
214  bool is_enum=false;
215  bool is_public=false, is_protected=false, is_private=false;
216  bool is_final = false;
217  bool is_interface = false;
218  bool is_synthetic = false;
219  bool is_annotation = false;
220  bool is_inner_class = false;
221  bool is_static_class = false;
222  bool is_anonymous_class = false;
224  irep_idt outer_class; // when no outer class is set, there is no outer class
225  size_t enum_elements=0;
226 
228  {
231  };
232 
233  typedef std::vector<u2> u2_valuest;
235  {
243 
245  explicit lambda_method_handlet(const u2_valuest &params)
246  : u2_values(params)
247  {
248  }
249 
252  : u2_values(std::move(params))
253  {
254  }
255 
256  bool is_unknown_handle() const
257  {
259  }
260  };
261 
262  // TODO(tkiley): This map shouldn't be interacted with directly (instead
263  // TODO(tkiley): using add_method_handle and get_method_handle and instead
264  // TODO(tkiley): should be made private. TG-2785
265  typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
268 
269  typedef std::list<irep_idt> implementst;
272  typedef std::list<fieldt> fieldst;
273  typedef std::list<methodt> methodst;
277 
279  {
280  fields.push_back(fieldt());
281  return fields.back();
282  }
283 
285  {
286  methods.push_back(methodt());
287  return methods.back();
288  }
289 
291  size_t bootstrap_index,
292  const lambda_method_handlet &handle)
293  {
294  lambda_method_handle_map[{name, bootstrap_index}] = handle;
295  }
296 
297  const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
298  {
299  return lambda_method_handle_map.at({name, bootstrap_index});
300  }
301 
302  void output(std::ostream &out) const;
303  };
304 
306 
307 
308  void output(std::ostream &out) const;
309 
310  typedef std::set<irep_idt> class_refst;
312 
313  bool loading_successful = false;
314 
317 
319  explicit java_bytecode_parse_treet(const irep_idt &class_name)
320  : parsed_class(class_name)
321  {
322  }
323 };
324 
328 class fieldref_exprt : public exprt
329 {
330 public:
332  const typet &type,
333  const irep_idt &component_name,
334  const irep_idt &class_name)
335  : exprt(ID_empty_string, type)
336  {
337  set(ID_class, class_name);
338  set(ID_component_name, component_name);
339  }
340 
342  {
343  return get(ID_class);
344  }
345 
347  {
348  return get(ID_component_name);
349  }
350 };
351 
352 template <>
353 inline bool can_cast_expr<fieldref_exprt>(const exprt &base)
354 {
355  return !base.get(ID_class).empty() && !base.get(ID_component_name).empty();
356 }
357 
358 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
java_bytecode_parse_treet::classt::implements
implementst implements
Definition: java_bytecode_parse_tree.h:270
java_bytecode_parse_treet::loading_successful
bool loading_successful
Definition: java_bytecode_parse_tree.h:313
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:61
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
java_bytecode_parse_treet::methodt::throws_exception_table
std::vector< irep_idt > throws_exception_table
Definition: java_bytecode_parse_tree.h:124
java_bytecode_parse_treet::membert::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:67
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_handlet
lambda_method_handlet(u2_valuest &&params)
Construct a lambda method handle with parameters params.
Definition: java_bytecode_parse_tree.h:251
java_bytecode_parse_treet::membert
Definition: java_bytecode_parse_tree.h:65
java_bytecode_parse_treet::classt::lambda_method_handle_map
lambda_method_handle_mapt lambda_method_handle_map
Definition: java_bytecode_parse_tree.h:267
java_bytecode_parse_treet::classt::add_method_handle
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
Definition: java_bytecode_parse_tree.h:290
java_bytecode_parse_treet::methodt::local_variablet::name
irep_idt name
Definition: java_bytecode_parse_tree.h:128
java_bytecode_parse_treet::methodt::verification_type_infot::ITEM_NULL
@ ITEM_NULL
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::methodt::exceptiont::catch_type
struct_tag_typet catch_type
Definition: java_bytecode_parse_tree.h:118
java_bytecode_parse_treet::fieldt::fieldt
fieldt()
Definition: java_bytecode_parse_tree.h:191
java_bytecode_parse_treet::membert::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:69
java_bytecode_parse_treet::annotationt::element_value_pairs
element_value_pairst element_value_pairs
Definition: java_bytecode_parse_tree.h:44
java_bytecode_parse_treet::classt::is_annotation
bool is_annotation
Definition: java_bytecode_parse_tree.h:219
java_bytecode_parse_treet::methodt::local_variablet
Definition: java_bytecode_parse_tree.h:127
java_bytecode_parse_treet::methodt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:87
java_bytecode_parse_treet::membert::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:70
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:23
java_bytecode_parse_treet::methodt::methodt
methodt()
Definition: java_bytecode_parse_tree.h:176
java_bytecode_parse_treet::methodt::verification_type_infot::TOP
@ TOP
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::methodt::verification_type_infot::OBJECT
@ OBJECT
Definition: java_bytecode_parse_tree.h:143
typet
The type of an expression, extends irept.
Definition: type.h:29
u2
uint16_t u2
Definition: bytecode_info.h:56
java_bytecode_parse_treet::methodt
Definition: java_bytecode_parse_tree.h:85
java_bytecode_parse_treet::methodt::add_instruction
instructiont & add_instruction()
Definition: java_bytecode_parse_tree.h:94
u8
uint64_t u8
Definition: bytecode_info.h:58
can_cast_expr< fieldref_exprt >
bool can_cast_expr< fieldref_exprt >(const exprt &base)
Definition: java_bytecode_parse_tree.h:353
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:91
optional.h
java_bytecode_parse_treet::annotationt::output
void output(std::ostream &) const
Definition: java_bytecode_parse_tree.cpp:55
java_bytecode_parse_treet::methodt::stack_map_table_entryt::CHOP
@ CHOP
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parse_treet::methodt::local_variable_table
local_variable_tablet local_variable_table
Definition: java_bytecode_parse_tree.h:137
fieldref_exprt
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
Definition: java_bytecode_parse_tree.h:329
java_bytecode_parse_treet::annotationt::element_value_pairt::output
void output(std::ostream &) const
Definition: java_bytecode_parse_tree.cpp:80
java_bytecode_parse_treet::methodt::stack_map_table_entryt::stack_verification_type_infot
std::vector< verification_type_infot > stack_verification_type_infot
Definition: java_bytecode_parse_tree.h:165
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition: java_bytecode_parse_tree.h:59
java_bytecode_parse_treet::annotationst
std::vector< annotationt > annotationst
Definition: java_bytecode_parse_tree.h:49
java_bytecode_parse_treet::java_bytecode_parse_treet
java_bytecode_parse_treet()=default
An empty bytecode parse tree, no class name set.
java_bytecode_parse_treet::classt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:218
java_bytecode_parse_treet::classt::classt
classt(const classt &)=delete
java_bytecode_parse_treet::annotationt::element_value_pairt::value
exprt value
Definition: java_bytecode_parse_tree.h:39
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_name
irep_idt lambda_method_name
Definition: java_bytecode_parse_tree.h:237
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED
@ UNINITIALIZED
Definition: java_bytecode_parse_tree.h:143
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:56
java_bytecode_parse_treet::instructiont::address
unsigned address
Definition: java_bytecode_parse_tree.h:58
java_bytecode_parse_treet::classt::attribute_bootstrapmethods_read
bool attribute_bootstrapmethods_read
Definition: java_bytecode_parse_tree.h:223
java_bytecode_parse_treet::classt::implementst
std::list< irep_idt > implementst
Definition: java_bytecode_parse_tree.h:269
java_bytecode_parse_treet::methodt::verification_type_infot::verification_type_info_type
verification_type_info_type
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::methodt::verification_type_infot::tag
u1 tag
Definition: java_bytecode_parse_tree.h:145
exprt
Base class for all expressions.
Definition: expr.h:53
java_bytecode_parse_treet::methodt::verification_type_infot::INTEGER
@ INTEGER
Definition: java_bytecode_parse_tree.h:141
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
java_bytecode_parse_treet::classt::classt
classt()=default
java_bytecode_parse_treet::classt::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:216
java_bytecode_parse_treet::classt::is_inner_class
bool is_inner_class
Definition: java_bytecode_parse_tree.h:220
java_bytecode_parse_treet::annotationt::element_value_pairt
Definition: java_bytecode_parse_tree.h:37
java_bytecode_parse_treet::find_annotation
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
Definition: java_bytecode_parse_tree.cpp:97
java_bytecode_parse_treet::fieldt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:197
fieldref_exprt::component_name
irep_idt component_name() const
Definition: java_bytecode_parse_tree.h:346
java_bytecode_parse_treet::classt::lambda_method_handlet::is_unknown_handle
bool is_unknown_handle() const
Definition: java_bytecode_parse_tree.h:256
java_bytecode_parse_treet::classt::lambda_method_handlet::interface_type
irep_idt interface_type
Definition: java_bytecode_parse_tree.h:239
java_bytecode_parse_treet::methodt::parameter_annotations
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
Definition: java_bytecode_parse_tree.h:106
java_bytecode_parse_treet::membert::has_annotation
bool has_annotation(const irep_idt &annotation_id) const
Definition: java_bytecode_parse_tree.h:78
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME
@ SAME
Definition: java_bytecode_parse_tree.h:154
java_bytecode_parse_treet::classt::lambda_method_handlet
Definition: java_bytecode_parse_tree.h:235
java_bytecode_parse_treet::classt::lambda_method_handle_mapt
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt
Definition: java_bytecode_parse_tree.h:266
java_bytecode_parse_treet::annotationt::element_value_pairst
std::vector< element_value_pairt > element_value_pairst
Definition: java_bytecode_parse_tree.h:43
java_bytecode_parse_treet::methodt::verification_type_infot::FLOAT
@ FLOAT
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::classt::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:276
java_bytecode_parse_treet::membert::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:66
java_bytecode_parse_treet::instructiont::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:57
java_bytecode_parse_treet::methodt::verification_type_infot::DOUBLE
@ DOUBLE
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::classt::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:215
java_bytecode_parse_treet::classt::lambda_method_handlet::u2_values
u2_valuest u2_values
Definition: java_bytecode_parse_tree.h:241
java_bytecode_parse_treet::methodt::verification_type_infot::type
verification_type_info_type type
Definition: java_bytecode_parse_tree.h:144
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
java_bytecode_parse_treet::methodt::verification_type_infot
Definition: java_bytecode_parse_tree.h:140
java_bytecode_parse_treet::membert::membert
membert()
Definition: java_bytecode_parse_tree.h:72
java_bytecode_parse_treet::classt::enum_elements
size_t enum_elements
Definition: java_bytecode_parse_tree.h:225
java_bytecode_parse_treet::membert::is_static
bool is_static
Definition: java_bytecode_parse_tree.h:69
require_parse_tree::methodt
java_bytecode_parse_treet::methodt methodt
Definition: require_parse_tree.h:30
java_bytecode_parse_treet::classt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:214
java_bytecode_parse_treet::annotationt
Definition: java_bytecode_parse_tree.h:33
java_bytecode_parse_treet::classt::operator=
classt & operator=(classt &&)=default
java_bytecode_parse_treet::methodt::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:89
java_bytecode_parse_treet::methodt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:116
java_bytecode_parse_treet::operator=
java_bytecode_parse_treet & operator=(const java_bytecode_parse_treet &)=delete
java_bytecode_parse_treet::classt::name
irep_idt name
Definition: java_bytecode_parse_tree.h:212
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK
@ SAME_LOCALS_ONE_STACK
Definition: java_bytecode_parse_tree.h:154
java_bytecode_parse_treet::methodt::instructions
instructionst instructions
Definition: java_bytecode_parse_tree.h:92
java_bytecode_parse_treet::classt::lambda_method_handlet::handle_type
method_handle_typet handle_type
Definition: java_bytecode_parse_tree.h:236
java_bytecode_parse_treet::classt::operator=
classt & operator=(const classt &)=delete
std_types.h
java_bytecode_parse_treet::classt::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:30
java_bytecode_parse_treet::methodt::verification_type_infot::LONG
@ LONG
Definition: java_bytecode_parse_tree.h:141
java_bytecode_parse_treet::class_refs
class_refst class_refs
Definition: java_bytecode_parse_tree.h:311
bytecode_info.h
java_bytecode_parse_treet::methodt::exceptiont
Definition: java_bytecode_parse_tree.h:109
java_bytecode_parse_treet::methodt::local_variablet::length
std::size_t length
Definition: java_bytecode_parse_tree.h:133
java_bytecode_parse_treet::methodt::stack_map_table_entryt::offset_delta
size_t offset_delta
Definition: java_bytecode_parse_tree.h:158
java_bytecode_parse_treet::methodt::base_name
irep_idt base_name
Definition: java_bytecode_parse_tree.h:86
java_bytecode_parse_treet::methodt::stack_map_table_entryt::stack_frame_type
stack_frame_type
Definition: java_bytecode_parse_tree.h:153
java_bytecode_parse_treet::methodt::local_variablet::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:132
java_bytecode_parse_treet::classt::add_method
methodt & add_method()
Definition: java_bytecode_parse_tree.h:284
java_bytecode_parse_treet::methodt::exceptiont::handler_pc
std::size_t handler_pc
Definition: java_bytecode_parse_tree.h:117
java_bytecode_parse_treet::classt::get_method_handle
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
Definition: java_bytecode_parse_tree.h:297
java_bytecode_parse_treet::methodt::stack_map_table_entryt::FULL
@ FULL
Definition: java_bytecode_parse_tree.h:155
dstringt::empty
bool empty() const
Definition: dstring.h:88
java_bytecode_parse_treet::classt::is_private
bool is_private
Definition: java_bytecode_parse_tree.h:215
java_bytecode_parse_treet::membert::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:69
java_bytecode_parse_treet::output
void output(std::ostream &out) const
Definition: java_bytecode_parse_tree.cpp:21
java_bytecode_parse_treet::classt::methods
methodst methods
Definition: java_bytecode_parse_tree.h:275
java_bytecode_parse_treet::classt::classt
classt(classt &&)=default
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_bytecode_parse_treet::classt::fields
fieldst fields
Definition: java_bytecode_parse_tree.h:274
java_bytecode_parse_treet::methodt::stack_map_table_entryt::APPEND
@ APPEND
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parse_treet::classt::u2_valuest
std::vector< u2 > u2_valuest
Definition: java_bytecode_parse_tree.h:233
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_handlet
lambda_method_handlet()=default
java_bytecode_parse_treet::methodt::exceptiont::end_pc
std::size_t end_pc
Definition: java_bytecode_parse_tree.h:116
java_bytecode_parse_treet::classt::method_handle_typet::LAMBDA_METHOD_HANDLE
@ LAMBDA_METHOD_HANDLE
java_bytecode_parse_treet::methodt::exception_tablet
std::vector< exceptiont > exception_tablet
Definition: java_bytecode_parse_tree.h:121
java_bytecode_parse_treet::methodt::stack_map_table_entryt::stack
stack_verification_type_infot stack
Definition: java_bytecode_parse_tree.h:168
source_locationt
Definition: source_location.h:20
java_bytecode_parse_treet::methodt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::classt::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:215
java_bytecode_parse_treet::classt::method_handle_typet
method_handle_typet
Definition: java_bytecode_parse_tree.h:228
java_bytecode_parse_treet::methodt::stack_map_table
stack_map_tablet stack_map_table
Definition: java_bytecode_parse_tree.h:172
java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index
u2 cpool_index
Definition: java_bytecode_parse_tree.h:146
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:305
java_bytecode_parse_treet::membert::name
irep_idt name
Definition: java_bytecode_parse_tree.h:68
require_parse_tree::lambda_method_handlet
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
Definition: require_parse_tree.h:23
fieldref_exprt::class_name
irep_idt class_name() const
Definition: java_bytecode_parse_tree.h:341
java_bytecode_parse_treet::methodt::local_variablet::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:130
java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:136
java_bytecode_parse_treet::instructiont::argst
std::vector< exprt > argst
Definition: java_bytecode_parse_tree.h:60
java_bytecode_parse_treet::membert::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:69
u1
uint8_t u1
Definition: bytecode_info.h:55
java_bytecode_parse_treet::membert::is_private
bool is_private
Definition: java_bytecode_parse_tree.h:69
java_bytecode_parse_treet::classt::method_handle_typet::UNKNOWN_HANDLE
@ UNKNOWN_HANDLE
java_bytecode_parse_treet::methodt::is_native
bool is_native
Definition: java_bytecode_parse_tree.h:87
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
java_bytecode_parse_treet::methodt::stack_map_tablet
std::vector< stack_map_table_entryt > stack_map_tablet
Definition: java_bytecode_parse_tree.h:171
java_bytecode_parse_treet::methodt::is_bridge
bool is_bridge
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::classt::classt
classt(const irep_idt &name)
Create a class name.
Definition: java_bytecode_parse_tree.h:201
java_bytecode_parse_treet::methodt::exception_table
exception_tablet exception_table
Definition: java_bytecode_parse_tree.h:122
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
java_bytecode_parse_treet::classt::fieldst
std::list< fieldt > fieldst
Definition: java_bytecode_parse_tree.h:272
java_bytecode_parse_treet::annotationt::element_value_pairt::element_name
irep_idt element_name
Definition: java_bytecode_parse_tree.h:38
java_bytecode_parse_treet::classt::is_static_class
bool is_static_class
Definition: java_bytecode_parse_tree.h:221
java_bytecode_parse_treet::methodt::is_varargs
bool is_varargs
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::methodt::stack_map_table_entryt::chops
size_t chops
Definition: java_bytecode_parse_tree.h:159
java_bytecode_parse_treet::methodt::is_synchronized
bool is_synchronized
Definition: java_bytecode_parse_tree.h:87
java_bytecode_parse_treet::classt::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:271
java_bytecode_parse_treet::methodt::exceptiont::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:115
java_bytecode_parse_treet::fieldt
Definition: java_bytecode_parse_tree.h:186
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED_THIS
@ UNINITIALIZED_THIS
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::classt
Definition: java_bytecode_parse_tree.h:197
java_bytecode_parse_treet::class_refst
std::set< irep_idt > class_refst
Definition: java_bytecode_parse_tree.h:310
java_bytecode_parse_treet::methodt::stack_map_table_entryt::appends
size_t appends
Definition: java_bytecode_parse_tree.h:160
java_bytecode_parse_treet::classt::methodst
std::list< methodt > methodst
Definition: java_bytecode_parse_tree.h:273
java_bytecode_parse_treet::classt::lambda_method_handlet::method_type
irep_idt method_type
Definition: java_bytecode_parse_tree.h:240
java_bytecode_parse_treet::methodt::stack_map_table_entryt::type
stack_frame_type type
Definition: java_bytecode_parse_tree.h:157
java_bytecode_parse_treet::java_bytecode_parse_treet
java_bytecode_parse_treet(const irep_idt &class_name)
Create a blank parse tree for class class_name.
Definition: java_bytecode_parse_tree.h:319
java_bytecode_parse_treet::methodt::stack_map_table_entryt
Definition: java_bytecode_parse_tree.h:151
java_bytecode_parse_treet::methodt::exceptiont::exceptiont
exceptiont()
Definition: java_bytecode_parse_tree.h:110
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_ref
irep_idt lambda_method_ref
Definition: java_bytecode_parse_tree.h:238
java_bytecode_parse_treet::fieldt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:187
java_bytecode_parse_treet::classt::add_field
fieldt & add_field()
Definition: java_bytecode_parse_tree.h:278
java_bytecode_parse_treet::methodt::verification_type_infot::offset
u2 offset
Definition: java_bytecode_parse_tree.h:147
java_bytecode_parse_treet::methodt::stack_map_table_entryt::locals
local_verification_type_infot locals
Definition: java_bytecode_parse_tree.h:167
java_bytecode_parse_treet::classt::is_interface
bool is_interface
Definition: java_bytecode_parse_tree.h:217
java_bytecode_parse_treet::classt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:213
java_bytecode_parse_treet::methodt::local_variablet::index
std::size_t index
Definition: java_bytecode_parse_tree.h:131
java_bytecode_parse_treet::methodt::stack_map_table_entryt::local_verification_type_infot
std::vector< verification_type_infot > local_verification_type_infot
Definition: java_bytecode_parse_tree.h:163
java_bytecode_parse_treet::classt::inner_name
irep_idt inner_name
Definition: java_bytecode_parse_tree.h:212
java_bytecode_parse_treet::classt::outer_class
irep_idt outer_class
Definition: java_bytecode_parse_tree.h:224
java_bytecode_parse_treet::operator=
java_bytecode_parse_treet & operator=(java_bytecode_parse_treet &&)=default
java_bytecode_parse_treet::classt::is_anonymous_class
bool is_anonymous_class
Definition: java_bytecode_parse_tree.h:222
fieldref_exprt::fieldref_exprt
fieldref_exprt(const typet &type, const irep_idt &component_name, const irep_idt &class_name)
Definition: java_bytecode_parse_tree.h:331
java_bytecode_parse_treet::classt::super_class
irep_idt super_class
Definition: java_bytecode_parse_tree.h:212
java_bytecode_parse_treet::java_bytecode_parse_treet
java_bytecode_parse_treet(java_bytecode_parse_treet &&)=default
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_handlet
lambda_method_handlet(const u2_valuest &params)
Construct a lambda method handle with parameters params.
Definition: java_bytecode_parse_tree.h:245
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK_EXTENDED
@ SAME_LOCALS_ONE_STACK_EXTENDED
Definition: java_bytecode_parse_tree.h:154
java_bytecode_parse_treet::methodt::local_variablet::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:129
java_bytecode_parse_treet::annotationt::type
typet type
Definition: java_bytecode_parse_tree.h:34
java_bytecode_parse_treet::java_bytecode_parse_treet
java_bytecode_parse_treet(const java_bytecode_parse_treet &)=delete
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_EXTENDED
@ SAME_EXTENDED
Definition: java_bytecode_parse_tree.h:155