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 #include "java_types.h"
22 
24 {
25  // Disallow copy construction and copy assignment, but allow move construction
26  // and move assignment.
32 
33  struct annotationt
34  {
36 
38  {
41  void output(std::ostream &) const;
42  };
43 
44  typedef std::vector<element_value_pairt> element_value_pairst;
46 
47  void output(std::ostream &) const;
48  };
49 
50  typedef std::vector<annotationt> annotationst;
51 
53  const annotationst &annotations,
54  const irep_idt &annotation_type_name);
55 
56  struct instructiont
57  {
59  unsigned address;
61  typedef std::vector<exprt> argst;
63  };
64 
65  struct membert
66  {
67  std::string descriptor;
72 
74  is_public(false), is_protected(false),
75  is_private(false), is_static(false), is_final(false)
76  {
77  }
78 
79  bool has_annotation(const irep_idt &annotation_id) const
80  {
81  return find_annotation(annotations, annotation_id).has_value();
82  }
83  };
84 
85  struct methodt : public membert
86  {
88  bool is_native = false, is_abstract = false, is_synchronized = false,
89  is_bridge = false, is_varargs = false, is_synthetic = false;
91 
92  typedef std::vector<instructiont> instructionst;
94 
96  {
97  instructions.push_back(instructiont());
98  return instructions.back();
99  }
100 
107  std::vector<annotationst> parameter_annotations;
108 
109  struct exceptiont
110  {
112  : start_pc(0), end_pc(0), handler_pc(0), catch_type(irep_idt())
113  {
114  }
115 
116  std::size_t start_pc;
117  std::size_t end_pc;
118  std::size_t handler_pc;
120  };
121 
122  typedef std::vector<exceptiont> exception_tablet;
124 
125  std::vector<irep_idt> throws_exception_table;
126 
128  {
130  std::string descriptor;
132  std::size_t index;
133  std::size_t start_pc;
134  std::size_t length;
135  };
136 
137  typedef std::vector<local_variablet> local_variable_tablet;
139 
141  {
149  };
150 
152  {
154  {
157  };
159  size_t offset_delta;
160  size_t chops;
161  size_t appends;
162 
163  typedef std::vector<verification_type_infot>
165  typedef std::vector<verification_type_infot>
167 
170  };
171 
172  typedef std::vector<stack_map_table_entryt> stack_map_tablet;
174 
175  void output(std::ostream &out) const;
176 
178  : is_native(false),
179  is_abstract(false),
180  is_synchronized(false),
181  is_bridge(false)
182  {
183  }
184  };
185 
186  struct fieldt : public membert
187  {
188  bool is_enum;
189 
190  void output(std::ostream &out) const;
191 
192  fieldt() : is_enum(false)
193  {
194  }
195  };
196 
197  struct classt
198  {
199  classt() = default;
200 
202  explicit classt(const irep_idt &name) : name(name)
203  {
204  }
205 
206  // Disallow copy construction and copy assignment, but allow move
207  // construction and move assignment.
208  classt(const classt &) = delete;
209  classt &operator=(const classt &) = delete;
210  classt(classt &&) = default;
211  classt &operator=(classt &&) = default;
212 
214  bool is_abstract=false;
215  bool is_enum=false;
216  bool is_public=false, is_protected=false, is_private=false;
217  bool is_final = false;
218  bool is_interface = false;
219  bool is_synthetic = false;
220  bool is_annotation = false;
221  bool is_inner_class = false;
222  bool is_static_class = false;
223  bool is_anonymous_class = false;
225  irep_idt outer_class; // when no outer class is set, there is no outer class
226  size_t enum_elements=0;
227 
228  typedef std::vector<u2> u2_valuest;
230  {
233 
239  {
240  PRECONDITION(
242  }
243 
245  : handle_type(java_class_typet::method_handle_kindt::UNKNOWN_HANDLE),
247  {
248  }
249 
251  {
252  return lambda_method_handlet{};
253  }
254 
255  bool is_unknown_handle() const
256  {
257  return handle_type ==
259  }
260 
262  {
264  return *method_descriptor;
265  }
266  };
267 
268  // TODO(tkiley): This map shouldn't be interacted with directly (instead
269  // TODO(tkiley): using add_method_handle and get_method_handle and instead
270  // TODO(tkiley): should be made private. TG-2785
271  typedef std::map<std::pair<irep_idt, size_t>, lambda_method_handlet>
274 
275  typedef std::list<irep_idt> implementst;
278  typedef std::list<fieldt> fieldst;
279  typedef std::list<methodt> methodst;
283 
285  {
286  fields.push_back(fieldt());
287  return fields.back();
288  }
289 
291  {
292  methods.push_back(methodt());
293  return methods.back();
294  }
295 
297  size_t bootstrap_index,
298  const lambda_method_handlet &handle)
299  {
300  lambda_method_handle_map[{name, bootstrap_index}] = handle;
301  }
302 
303  const lambda_method_handlet &get_method_handle(size_t bootstrap_index) const
304  {
305  return lambda_method_handle_map.at({name, bootstrap_index});
306  }
307 
308  void output(std::ostream &out) const;
309  };
310 
312 
313 
314  void output(std::ostream &out) const;
315 
316  typedef std::set<irep_idt> class_refst;
318 
319  bool loading_successful = false;
320 
323 
325  explicit java_bytecode_parse_treet(const irep_idt &class_name)
326  : parsed_class(class_name)
327  {
328  }
329 };
330 
334 class fieldref_exprt : public exprt
335 {
336 public:
338  const typet &type,
339  const irep_idt &component_name,
340  const irep_idt &class_name)
341  : exprt(ID_empty_string, type)
342  {
343  set(ID_class, class_name);
344  set(ID_component_name, component_name);
345  }
346 
348  {
349  return get(ID_class);
350  }
351 
353  {
354  return get(ID_component_name);
355  }
356 };
357 
358 template <>
359 inline bool can_cast_expr<fieldref_exprt>(const exprt &base)
360 {
361  return !base.get(ID_class).empty() && !base.get(ID_component_name).empty();
362 }
363 
364 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
java_bytecode_parse_treet::classt::implements
implementst implements
Definition: java_bytecode_parse_tree.h:276
java_bytecode_parse_treet::loading_successful
bool loading_successful
Definition: java_bytecode_parse_tree.h:319
java_bytecode_parse_treet::instructiont::args
argst args
Definition: java_bytecode_parse_tree.h:62
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:125
java_bytecode_parse_treet::membert::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:68
java_bytecode_parse_treet::membert
Definition: java_bytecode_parse_tree.h:66
java_bytecode_parse_treet::classt::lambda_method_handle_map
lambda_method_handle_mapt lambda_method_handle_map
Definition: java_bytecode_parse_tree.h:273
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:296
java_bytecode_parse_treet::methodt::local_variablet::name
irep_idt name
Definition: java_bytecode_parse_tree.h:129
java_bytecode_parse_treet::methodt::verification_type_infot::ITEM_NULL
@ ITEM_NULL
Definition: java_bytecode_parse_tree.h:143
java_bytecode_parse_treet::methodt::exceptiont::catch_type
struct_tag_typet catch_type
Definition: java_bytecode_parse_tree.h:119
java_bytecode_parse_treet::fieldt::fieldt
fieldt()
Definition: java_bytecode_parse_tree.h:192
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_handlet
lambda_method_handlet()
Definition: java_bytecode_parse_tree.h:244
java_bytecode_parse_treet::membert::is_final
bool is_final
Definition: java_bytecode_parse_tree.h:70
java_bytecode_parse_treet::annotationt::element_value_pairs
element_value_pairst element_value_pairs
Definition: java_bytecode_parse_tree.h:45
java_bytecode_parse_treet::classt::is_annotation
bool is_annotation
Definition: java_bytecode_parse_tree.h:220
java_bytecode_parse_treet::classt::lambda_method_handlet::handle_type
java_class_typet::method_handle_kindt handle_type
Definition: java_bytecode_parse_tree.h:231
java_bytecode_parse_treet::methodt::local_variablet
Definition: java_bytecode_parse_tree.h:128
java_bytecode_parse_treet::methodt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::membert::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:71
java_bytecode_parse_treet
Definition: java_bytecode_parse_tree.h:24
java_bytecode_parse_treet::methodt::methodt
methodt()
Definition: java_bytecode_parse_tree.h:177
java_bytecode_parse_treet::methodt::verification_type_infot::TOP
@ TOP
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::methodt::verification_type_infot::OBJECT
@ OBJECT
Definition: java_bytecode_parse_tree.h:144
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:86
java_bytecode_parse_treet::methodt::add_instruction
instructiont & add_instruction()
Definition: java_bytecode_parse_tree.h:95
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:359
java_bytecode_parse_treet::methodt::instructionst
std::vector< instructiont > instructionst
Definition: java_bytecode_parse_tree.h:92
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:156
java_bytecode_parse_treet::methodt::local_variable_table
local_variable_tablet local_variable_table
Definition: java_bytecode_parse_tree.h:138
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:335
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:166
java_bytecode_parse_treet::instructiont::bytecode
u8 bytecode
Definition: java_bytecode_parse_tree.h:60
java_bytecode_parse_treet::annotationst
std::vector< annotationt > annotationst
Definition: java_bytecode_parse_tree.h:50
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:219
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:40
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED
@ UNINITIALIZED
Definition: java_bytecode_parse_tree.h:144
java_bytecode_parse_treet::instructiont
Definition: java_bytecode_parse_tree.h:57
java_bytecode_parse_treet::instructiont::address
unsigned address
Definition: java_bytecode_parse_tree.h:59
java_bytecode_parse_treet::classt::attribute_bootstrapmethods_read
bool attribute_bootstrapmethods_read
Definition: java_bytecode_parse_tree.h:224
java_bytecode_parse_treet::classt::implementst
std::list< irep_idt > implementst
Definition: java_bytecode_parse_tree.h:275
java_bytecode_parse_treet::methodt::verification_type_infot::verification_type_info_type
verification_type_info_type
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::methodt::verification_type_infot::tag
u1 tag
Definition: java_bytecode_parse_tree.h:146
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:142
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:217
java_bytecode_parse_treet::classt::is_inner_class
bool is_inner_class
Definition: java_bytecode_parse_tree.h:221
java_bytecode_parse_treet::annotationt::element_value_pairt
Definition: java_bytecode_parse_tree.h:38
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:352
java_bytecode_parse_treet::classt::lambda_method_handlet::is_unknown_handle
bool is_unknown_handle() const
Definition: java_bytecode_parse_tree.h:255
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:107
java_bytecode_parse_treet::membert::has_annotation
bool has_annotation(const irep_idt &annotation_id) const
Definition: java_bytecode_parse_tree.h:79
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME
@ SAME
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parse_treet::classt::lambda_method_handlet
Definition: java_bytecode_parse_tree.h:230
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:272
java_bytecode_parse_treet::annotationt::element_value_pairst
std::vector< element_value_pairt > element_value_pairst
Definition: java_bytecode_parse_tree.h:44
java_class_typet
Definition: java_types.h:199
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
java_bytecode_parse_treet::methodt::verification_type_infot::FLOAT
@ FLOAT
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::classt::annotations
annotationst annotations
Definition: java_bytecode_parse_tree.h:282
java_bytecode_parse_treet::membert::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:67
java_bytecode_parse_treet::instructiont::source_location
source_locationt source_location
Definition: java_bytecode_parse_tree.h:58
java_bytecode_parse_treet::methodt::verification_type_infot::DOUBLE
@ DOUBLE
Definition: java_bytecode_parse_tree.h:142
java_bytecode_parse_treet::classt::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:216
java_bytecode_parse_treet::methodt::verification_type_infot::type
verification_type_info_type type
Definition: java_bytecode_parse_tree.h:145
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:141
java_bytecode_parse_treet::classt::lambda_method_handlet::lambda_method_handlet
lambda_method_handlet(const class_method_descriptor_exprt &method_descriptor, java_class_typet::method_handle_kindt handle_type)
Construct a lambda method handle with parameters params.
Definition: java_bytecode_parse_tree.h:235
java_bytecode_parse_treet::membert::membert
membert()
Definition: java_bytecode_parse_tree.h:73
java_bytecode_parse_treet::classt::enum_elements
size_t enum_elements
Definition: java_bytecode_parse_tree.h:226
java_bytecode_parse_treet::membert::is_static
bool is_static
Definition: java_bytecode_parse_tree.h:70
require_parse_tree::methodt
java_bytecode_parse_treet::methodt methodt
Definition: require_parse_tree.h:29
java_bytecode_parse_treet::classt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:215
java_bytecode_parse_treet::annotationt
Definition: java_bytecode_parse_tree.h:34
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:90
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:213
java_bytecode_parse_treet::methodt::stack_map_table_entryt::SAME_LOCALS_ONE_STACK
@ SAME_LOCALS_ONE_STACK
Definition: java_bytecode_parse_tree.h:155
java_bytecode_parse_treet::methodt::instructions
instructionst instructions
Definition: java_bytecode_parse_tree.h:93
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
java_bytecode_parse_treet::classt::operator=
classt & operator=(const classt &)=delete
std_types.h
Pre-defined types.
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:142
java_bytecode_parse_treet::class_refs
class_refst class_refs
Definition: java_bytecode_parse_tree.h:317
bytecode_info.h
java_bytecode_parse_treet::classt::lambda_method_handlet::get_method_descriptor
const class_method_descriptor_exprt & get_method_descriptor() const
Definition: java_bytecode_parse_tree.h:261
java_bytecode_parse_treet::methodt::exceptiont
Definition: java_bytecode_parse_tree.h:110
java_bytecode_parse_treet::methodt::local_variablet::length
std::size_t length
Definition: java_bytecode_parse_tree.h:134
java_bytecode_parse_treet::methodt::stack_map_table_entryt::offset_delta
size_t offset_delta
Definition: java_bytecode_parse_tree.h:159
java_bytecode_parse_treet::methodt::base_name
irep_idt base_name
Definition: java_bytecode_parse_tree.h:87
java_bytecode_parse_treet::methodt::stack_map_table_entryt::stack_frame_type
stack_frame_type
Definition: java_bytecode_parse_tree.h:154
java_bytecode_parse_treet::methodt::local_variablet::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:133
java_bytecode_parse_treet::classt::add_method
methodt & add_method()
Definition: java_bytecode_parse_tree.h:290
java_bytecode_parse_treet::methodt::exceptiont::handler_pc
std::size_t handler_pc
Definition: java_bytecode_parse_tree.h:118
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:303
java_bytecode_parse_treet::methodt::stack_map_table_entryt::FULL
@ FULL
Definition: java_bytecode_parse_tree.h:156
java_class_typet::method_handle_kindt::UNKNOWN_HANDLE
@ UNKNOWN_HANDLE
Can't be called.
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:216
java_bytecode_parse_treet::membert::is_public
bool is_public
Definition: java_bytecode_parse_tree.h:70
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:281
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:280
java_bytecode_parse_treet::methodt::stack_map_table_entryt::APPEND
@ APPEND
Definition: java_bytecode_parse_tree.h:156
java_bytecode_parse_treet::classt::u2_valuest
std::vector< u2 > u2_valuest
Definition: java_bytecode_parse_tree.h:228
java_bytecode_parse_treet::methodt::exceptiont::end_pc
std::size_t end_pc
Definition: java_bytecode_parse_tree.h:117
java_bytecode_parse_treet::methodt::exception_tablet
std::vector< exceptiont > exception_tablet
Definition: java_bytecode_parse_tree.h:122
java_bytecode_parse_treet::methodt::stack_map_table_entryt::stack
stack_verification_type_infot stack
Definition: java_bytecode_parse_tree.h:169
source_locationt
Definition: source_location.h:20
java_bytecode_parse_treet::methodt::is_synthetic
bool is_synthetic
Definition: java_bytecode_parse_tree.h:89
java_bytecode_parse_treet::classt::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:216
java_bytecode_parse_treet::methodt::stack_map_table
stack_map_tablet stack_map_table
Definition: java_bytecode_parse_tree.h:173
java_bytecode_parse_treet::methodt::verification_type_infot::cpool_index
u2 cpool_index
Definition: java_bytecode_parse_tree.h:147
java_bytecode_parse_treet::parsed_class
classt parsed_class
Definition: java_bytecode_parse_tree.h:311
java_bytecode_parse_treet::membert::name
irep_idt name
Definition: java_bytecode_parse_tree.h:69
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:347
java_bytecode_parse_treet::methodt::local_variablet::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:131
java_bytecode_parse_treet::methodt::local_variable_tablet
std::vector< local_variablet > local_variable_tablet
Definition: java_bytecode_parse_tree.h:137
java_bytecode_parse_treet::instructiont::argst
std::vector< exprt > argst
Definition: java_bytecode_parse_tree.h:61
java_bytecode_parse_treet::membert::is_protected
bool is_protected
Definition: java_bytecode_parse_tree.h:70
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:70
java_bytecode_parse_treet::methodt::is_native
bool is_native
Definition: java_bytecode_parse_tree.h:88
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:172
java_bytecode_parse_treet::methodt::is_bridge
bool is_bridge
Definition: java_bytecode_parse_tree.h:89
java_bytecode_parse_treet::classt::classt
classt(const irep_idt &name)
Create a class name.
Definition: java_bytecode_parse_tree.h:202
java_bytecode_parse_treet::methodt::exception_table
exception_tablet exception_table
Definition: java_bytecode_parse_tree.h:123
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:278
java_bytecode_parse_treet::annotationt::element_value_pairt::element_name
irep_idt element_name
Definition: java_bytecode_parse_tree.h:39
java_bytecode_parse_treet::classt::is_static_class
bool is_static_class
Definition: java_bytecode_parse_tree.h:222
java_bytecode_parse_treet::methodt::is_varargs
bool is_varargs
Definition: java_bytecode_parse_tree.h:89
java_bytecode_parse_treet::methodt::stack_map_table_entryt::chops
size_t chops
Definition: java_bytecode_parse_tree.h:160
java_bytecode_parse_treet::methodt::is_synchronized
bool is_synchronized
Definition: java_bytecode_parse_tree.h:88
java_bytecode_parse_treet::classt::signature
optionalt< std::string > signature
Definition: java_bytecode_parse_tree.h:277
java_bytecode_parse_treet::methodt::exceptiont::start_pc
std::size_t start_pc
Definition: java_bytecode_parse_tree.h:116
java_bytecode_parse_treet::fieldt
Definition: java_bytecode_parse_tree.h:187
java_bytecode_parse_treet::methodt::verification_type_infot::UNINITIALIZED_THIS
@ UNINITIALIZED_THIS
Definition: java_bytecode_parse_tree.h:143
java_bytecode_parse_treet::classt
Definition: java_bytecode_parse_tree.h:198
java_bytecode_parse_treet::class_refst
std::set< irep_idt > class_refst
Definition: java_bytecode_parse_tree.h:316
java_bytecode_parse_treet::methodt::stack_map_table_entryt::appends
size_t appends
Definition: java_bytecode_parse_tree.h:161
java_class_typet::method_handle_kindt
method_handle_kindt
Indicates what sort of code should be synthesised for a lambda call:
Definition: java_types.h:467
java_bytecode_parse_treet::classt::methodst
std::list< methodt > methodst
Definition: java_bytecode_parse_tree.h:279
java_bytecode_parse_treet::methodt::stack_map_table_entryt::type
stack_frame_type type
Definition: java_bytecode_parse_tree.h:158
java_types.h
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:325
java_bytecode_parse_treet::methodt::stack_map_table_entryt
Definition: java_bytecode_parse_tree.h:152
java_bytecode_parse_treet::methodt::exceptiont::exceptiont
exceptiont()
Definition: java_bytecode_parse_tree.h:111
java_bytecode_parse_treet::fieldt::is_enum
bool is_enum
Definition: java_bytecode_parse_tree.h:188
java_bytecode_parse_treet::classt::add_field
fieldt & add_field()
Definition: java_bytecode_parse_tree.h:284
java_bytecode_parse_treet::methodt::verification_type_infot::offset
u2 offset
Definition: java_bytecode_parse_tree.h:148
java_bytecode_parse_treet::methodt::stack_map_table_entryt::locals
local_verification_type_infot locals
Definition: java_bytecode_parse_tree.h:168
java_bytecode_parse_treet::classt::is_interface
bool is_interface
Definition: java_bytecode_parse_tree.h:218
java_bytecode_parse_treet::classt::is_abstract
bool is_abstract
Definition: java_bytecode_parse_tree.h:214
java_bytecode_parse_treet::methodt::local_variablet::index
std::size_t index
Definition: java_bytecode_parse_tree.h:132
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:164
java_bytecode_parse_treet::classt::lambda_method_handlet::method_descriptor
optionalt< class_method_descriptor_exprt > method_descriptor
Definition: java_bytecode_parse_tree.h:232
java_bytecode_parse_treet::classt::inner_name
irep_idt inner_name
Definition: java_bytecode_parse_tree.h:213
java_bytecode_parse_treet::classt::outer_class
irep_idt outer_class
Definition: java_bytecode_parse_tree.h:225
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:223
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:337
java_bytecode_parse_treet::classt::super_class
irep_idt super_class
Definition: java_bytecode_parse_tree.h:213
java_bytecode_parse_treet::java_bytecode_parse_treet
java_bytecode_parse_treet(java_bytecode_parse_treet &&)=default
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:155
java_bytecode_parse_treet::methodt::local_variablet::descriptor
std::string descriptor
Definition: java_bytecode_parse_tree.h:130
java_bytecode_parse_treet::classt::lambda_method_handlet::get_unknown_handle
static lambda_method_handlet get_unknown_handle()
Definition: java_bytecode_parse_tree.h:250
java_bytecode_parse_treet::annotationt::type
typet type
Definition: java_bytecode_parse_tree.h:35
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:156