CBMC
java_bytecode_parse_treet::methodt Struct Reference

#include <java_bytecode_parse_tree.h>

+ Inheritance diagram for java_bytecode_parse_treet::methodt:
+ Collaboration diagram for java_bytecode_parse_treet::methodt:

Classes

struct  exceptiont
 
struct  local_variablet
 
struct  stack_map_table_entryt
 
struct  verification_type_infot
 

Public Types

typedef std::vector< instructiontinstructionst
 
typedef std::vector< exceptiontexception_tablet
 
typedef std::vector< local_variabletlocal_variable_tablet
 
typedef std::vector< stack_map_table_entrytstack_map_tablet
 

Public Member Functions

instructiontadd_instruction ()
 
void output (std::ostream &out) const
 
 methodt ()
 
- Public Member Functions inherited from java_bytecode_parse_treet::membert
 membert ()
 
bool has_annotation (const irep_idt &annotation_id) const
 

Public Attributes

irep_idt base_name
 
bool is_native = false
 
bool is_abstract = false
 
bool is_synchronized = false
 
bool is_bridge = false
 
bool is_varargs = false
 
bool is_synthetic = false
 
source_locationt source_location
 
instructionst instructions
 
std::vector< annotationstparameter_annotations
 Java annotations that were applied to parameters of this method. More...
 
exception_tablet exception_table
 
std::vector< irep_idtthrows_exception_table
 
local_variable_tablet local_variable_table
 
stack_map_tablet stack_map_table
 
- Public Attributes inherited from java_bytecode_parse_treet::membert
std::string descriptor
 
std::optional< std::string > signature
 
irep_idt name
 
bool is_public
 
bool is_protected
 
bool is_private
 
bool is_static
 
bool is_final
 
annotationst annotations
 

Detailed Description

Definition at line 84 of file java_bytecode_parse_tree.h.

Member Typedef Documentation

◆ exception_tablet

◆ instructionst

◆ local_variable_tablet

◆ stack_map_tablet

Constructor & Destructor Documentation

◆ methodt()

java_bytecode_parse_treet::methodt::methodt ( )
inline

Definition at line 176 of file java_bytecode_parse_tree.h.

Member Function Documentation

◆ add_instruction()

instructiont& java_bytecode_parse_treet::methodt::add_instruction ( )
inline

Definition at line 94 of file java_bytecode_parse_tree.h.

◆ output()

void java_bytecode_parse_treet::methodt::output ( std::ostream &  out) const

Definition at line 114 of file java_bytecode_parse_tree.cpp.

Member Data Documentation

◆ base_name

irep_idt java_bytecode_parse_treet::methodt::base_name

Definition at line 86 of file java_bytecode_parse_tree.h.

◆ exception_table

exception_tablet java_bytecode_parse_treet::methodt::exception_table

Definition at line 122 of file java_bytecode_parse_tree.h.

◆ instructions

instructionst java_bytecode_parse_treet::methodt::instructions

Definition at line 92 of file java_bytecode_parse_tree.h.

◆ is_abstract

bool java_bytecode_parse_treet::methodt::is_abstract = false

Definition at line 87 of file java_bytecode_parse_tree.h.

◆ is_bridge

bool java_bytecode_parse_treet::methodt::is_bridge = false

Definition at line 88 of file java_bytecode_parse_tree.h.

◆ is_native

bool java_bytecode_parse_treet::methodt::is_native = false

Definition at line 87 of file java_bytecode_parse_tree.h.

◆ is_synchronized

bool java_bytecode_parse_treet::methodt::is_synchronized = false

Definition at line 87 of file java_bytecode_parse_tree.h.

◆ is_synthetic

bool java_bytecode_parse_treet::methodt::is_synthetic = false

Definition at line 88 of file java_bytecode_parse_tree.h.

◆ is_varargs

bool java_bytecode_parse_treet::methodt::is_varargs = false

Definition at line 88 of file java_bytecode_parse_tree.h.

◆ local_variable_table

local_variable_tablet java_bytecode_parse_treet::methodt::local_variable_table

Definition at line 137 of file java_bytecode_parse_tree.h.

◆ parameter_annotations

std::vector<annotationst> java_bytecode_parse_treet::methodt::parameter_annotations

Java annotations that were applied to parameters of this method.

Remarks
Each element in the vector corresponds to the annotations on the parameter of this method with the matching index. A parameter that does not have annotations can have an entry in this vector that is an empty annotationst. Trailing parameters that have no annotations may be entirely omitted from this vector.

Definition at line 106 of file java_bytecode_parse_tree.h.

◆ source_location

source_locationt java_bytecode_parse_treet::methodt::source_location

Definition at line 89 of file java_bytecode_parse_tree.h.

◆ stack_map_table

stack_map_tablet java_bytecode_parse_treet::methodt::stack_map_table

Definition at line 172 of file java_bytecode_parse_tree.h.

◆ throws_exception_table

std::vector<irep_idt> java_bytecode_parse_treet::methodt::throws_exception_table

Definition at line 124 of file java_bytecode_parse_tree.h.


The documentation for this struct was generated from the following files: