Go to the documentation of this file.
10 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
11 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
26 #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
42 void output(std::ostream &)
const;
48 void output(std::ostream &)
const;
55 const irep_idt &annotation_type_name);
62 typedef std::vector<exprt>
argst;
164 typedef std::vector<verification_type_infot>
166 typedef std::vector<verification_type_infot>
176 void output(std::ostream &out)
const;
191 void output(std::ostream &out)
const;
209 #ifndef _MSC_VER // Ommit this on MS VC2013 as move is not supported.
295 size_t bootstrap_index,
306 void output(std::ostream &out)
const;
312 void output(std::ostream &out)
const;
341 set(ID_class, class_name);
342 set(ID_component_name, component_name);
346 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_PARSE_TREE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::vector< irep_idt > throws_exception_table
optionalt< std::string > signature
lambda_method_handlet(u2_valuest &¶ms)
Construct a lambda method handle with parameters params.
lambda_method_handle_mapt lambda_method_handle_map
void add_method_handle(size_t bootstrap_index, const lambda_method_handlet &handle)
struct_tag_typet catch_type
element_value_pairst element_value_pairs
The type of an expression, extends irept.
instructiont & add_instruction()
std::vector< instructiont > instructionst
void output(std::ostream &) const
local_variable_tablet local_variable_table
Represents the argument of an instruction that uses a CONSTANT_Fieldref This is used for example as a...
void output(std::ostream &) const
std::vector< verification_type_infot > stack_verification_type_infot
std::vector< annotationt > annotationst
java_bytecode_parse_treet()=default
An empty bytecode parse tree, no class name set.
irep_idt lambda_method_name
bool attribute_bootstrapmethods_read
std::list< irep_idt > implementst
verification_type_info_type
Base class for all expressions.
A struct tag type, i.e., struct_typet with an identifier.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
void output(std::ostream &out) const
bool is_unknown_handle() const
std::vector< annotationst > parameter_annotations
Java annotations that were applied to parameters of this method.
bool has_annotation(const irep_idt &annotation_id) const
std::map< std::pair< irep_idt, size_t >, lambda_method_handlet > lambda_method_handle_mapt
std::vector< element_value_pairt > element_value_pairst
source_locationt source_location
verification_type_info_type type
typet & type()
Return the type of the expression.
java_bytecode_parse_treet::methodt methodt
source_locationt source_location
void output(std::ostream &out) const
java_bytecode_parse_treet & operator=(const java_bytecode_parse_treet &)=delete
instructionst instructions
method_handle_typet handle_type
classt & operator=(const classt &)=delete
void output(std::ostream &out) const
const lambda_method_handlet & get_method_handle(size_t bootstrap_index) const
void output(std::ostream &out) const
nonstd::optional< T > optionalt
std::vector< u2 > u2_valuest
lambda_method_handlet()=default
std::vector< exceptiont > exception_tablet
stack_verification_type_infot stack
stack_map_tablet stack_map_table
java_bytecode_parse_treet::classt::lambda_method_handlet lambda_method_handlet
optionalt< std::string > signature
std::vector< local_variablet > local_variable_tablet
std::vector< exprt > argst
std::vector< stack_map_table_entryt > stack_map_tablet
classt(const irep_idt &name)
Create a class name.
exception_tablet exception_table
void set(const irep_namet &name, const irep_idt &value)
std::list< fieldt > fieldst
optionalt< std::string > signature
std::set< irep_idt > class_refst
std::list< methodt > methodst
java_bytecode_parse_treet(const irep_idt &class_name)
Create a blank parse tree for class class_name.
irep_idt lambda_method_ref
local_verification_type_infot locals
std::vector< verification_type_infot > local_verification_type_infot
fieldref_exprt(const typet &type, const irep_idt &component_name, const irep_idt &class_name)
lambda_method_handlet(const u2_valuest ¶ms)
Construct a lambda method handle with parameters params.