CBMC
java_bytecode_convert_methodt::variablet Class Reference

#include <java_bytecode_convert_method_class.h>

+ Collaboration diagram for java_bytecode_convert_methodt::variablet:

Public Member Functions

 variablet (const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length)
 
 variablet (const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter)
 
 variablet (const symbol_exprt &_symbol_expr, std::size_t _start_pc, std::size_t _length, bool _is_parameter, std::vector< holet > &&_holes)
 

Public Attributes

symbol_exprt symbol_expr
 
size_t start_pc
 
size_t length
 
bool is_parameter = false
 
std::vector< holetholes
 

Detailed Description

Definition at line 125 of file java_bytecode_convert_method_class.h.

Constructor & Destructor Documentation

◆ variablet() [1/3]

java_bytecode_convert_methodt::variablet::variablet ( const symbol_exprt _symbol_expr,
std::size_t  _start_pc,
std::size_t  _length 
)
inline

Definition at line 134 of file java_bytecode_convert_method_class.h.

◆ variablet() [2/3]

java_bytecode_convert_methodt::variablet::variablet ( const symbol_exprt _symbol_expr,
std::size_t  _start_pc,
std::size_t  _length,
bool  _is_parameter 
)
inline

Definition at line 142 of file java_bytecode_convert_method_class.h.

◆ variablet() [3/3]

java_bytecode_convert_methodt::variablet::variablet ( const symbol_exprt _symbol_expr,
std::size_t  _start_pc,
std::size_t  _length,
bool  _is_parameter,
std::vector< holet > &&  _holes 
)
inline

Definition at line 154 of file java_bytecode_convert_method_class.h.

Member Data Documentation

◆ holes

std::vector<holet> java_bytecode_convert_methodt::variablet::holes

Definition at line 132 of file java_bytecode_convert_method_class.h.

◆ is_parameter

bool java_bytecode_convert_methodt::variablet::is_parameter = false

Definition at line 131 of file java_bytecode_convert_method_class.h.

◆ length

size_t java_bytecode_convert_methodt::variablet::length

Definition at line 130 of file java_bytecode_convert_method_class.h.

◆ start_pc

size_t java_bytecode_convert_methodt::variablet::start_pc

Definition at line 129 of file java_bytecode_convert_method_class.h.

◆ symbol_expr

symbol_exprt java_bytecode_convert_methodt::variablet::symbol_expr

Definition at line 128 of file java_bytecode_convert_method_class.h.


The documentation for this class was generated from the following file: