CBMC
|
#include <bytecode_info.h>
Public Attributes | |
const char * | mnemonic |
unsigned char | opcode |
char | format |
unsigned | pop |
unsigned | push |
char | result_type |
Definition at line 44 of file bytecode_info.h.
char bytecode_infot::format |
Definition at line 48 of file bytecode_info.h.
const char* bytecode_infot::mnemonic |
Definition at line 46 of file bytecode_info.h.
unsigned char bytecode_infot::opcode |
Definition at line 47 of file bytecode_info.h.
unsigned bytecode_infot::pop |
Definition at line 49 of file bytecode_info.h.
unsigned bytecode_infot::push |
Definition at line 49 of file bytecode_info.h.
char bytecode_infot::result_type |
Definition at line 50 of file bytecode_info.h.