cprover
bytecode_info.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_BYTECODE_INFO_H
11
#define CPROVER_JAVA_BYTECODE_BYTECODE_INFO_H
12
13
#include <cstdint>
14
15
// http://en.wikipedia.org/wiki/Java_bytecode_instruction_listings
16
17
// The 'result_type' is one of the following:
18
// i integer
19
// l long
20
// s short
21
// b byte
22
// c character
23
// f float
24
// d double
25
// z boolean
26
// a reference
27
28
// The 'format' is:
29
// ' ' - just one byte
30
// 'c' - a constant_pool index, one byte
31
// 'C' - a constant_pool index, two bytes
32
// 'b' - a byte, signed
33
// 'o' - two byte branch offset
34
// 'O' - four byte branch offset
35
// 'v' - local variable index, one byte
36
// 'V' - local variable index, one byte, plus one byte, signed
37
// 'I' - two byte constant_pool index, plus two bytes
38
// 'L' - lookupswitch
39
// 'T' - tableswitch
40
// 'm' - multianewarray
41
// 't' - array subtype, one byte
42
// 's' - a short, signed
43
44
struct
bytecode_infot
45
{
46
const
char
*
mnemonic
;
47
unsigned
char
opcode
;
48
char
format
;
49
unsigned
pop
,
push
;
50
char
result_type
;
51
};
52
53
extern
struct
bytecode_infot
const
bytecode_info
[];
54
55
typedef
uint8_t
u1
;
// NOLINT(readability/identifiers)
56
typedef
uint16_t
u2
;
// NOLINT(readability/identifiers)
57
typedef
uint32_t
u4
;
// NOLINT(readability/identifiers)
58
typedef
uint64_t
u8
;
// NOLINT(readability/identifiers)
59
typedef
int8_t
s1
;
// NOLINT(readability/identifiers)
60
typedef
int16_t
s2
;
// NOLINT(readability/identifiers)
61
typedef
int32_t
s4
;
// NOLINT(readability/identifiers)
62
typedef
int64_t
s8
;
// NOLINT(readability/identifiers)
63
64
#endif // CPROVER_JAVA_BYTECODE_BYTECODE_INFO_H
u8
uint64_t u8
Definition:
bytecode_info.h:58
bytecode_infot
Definition:
bytecode_info.h:44
bytecode_infot::format
char format
Definition:
bytecode_info.h:48
u4
uint32_t u4
Definition:
bytecode_info.h:57
bytecode_infot::result_type
char result_type
Definition:
bytecode_info.h:50
bytecode_infot::push
unsigned push
Definition:
bytecode_info.h:49
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition:
bytecode_info.cpp:16
u2
uint16_t u2
Definition:
bytecode_info.h:56
s4
int32_t s4
Definition:
bytecode_info.h:61
bytecode_infot::pop
unsigned pop
Definition:
bytecode_info.h:49
s8
int64_t s8
Definition:
bytecode_info.h:62
bytecode_infot::mnemonic
const char * mnemonic
Definition:
bytecode_info.h:46
u1
uint8_t u1
Definition:
bytecode_info.h:55
bytecode_infot::opcode
unsigned char opcode
Definition:
bytecode_info.h:47
s1
int8_t s1
Definition:
bytecode_info.h:59
s2
int16_t s2
Definition:
bytecode_info.h:60
jbmc
src
java_bytecode
bytecode_info.h
Generated by
1.8.14