CBMC
pattern.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Pattern matching for bytecode instructions
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_JAVA_BYTECODE_PATTERN_H
13
#define CPROVER_JAVA_BYTECODE_PATTERN_H
14
15
#include "
bytecode_info.h
"
16
20
class
patternt
21
{
22
public
:
23
explicit
patternt
(
const
char
*_p) :
p
(_p)
24
{
25
}
26
27
// match with '?'
28
bool
operator==
(
const
u1
bytecode)
const
29
{
30
const
char
*what =
bytecode_info
[bytecode].
mnemonic
;
31
32
std::size_t i;
33
34
for
(i = 0; what[i] != 0; i++)
35
if
(
p
[i] == 0)
36
return
false
;
37
else
if
(
p
[i] !=
'?'
&&
p
[i] != what[i])
38
return
false
;
39
40
return
p
[i] == 0;
41
}
42
43
friend
bool
operator==
(
const
u1
bytecode,
const
patternt
&
p
)
44
{
45
return
p
== bytecode;
46
}
47
48
friend
bool
operator!=
(
const
u1
bytecode,
const
patternt
&
p
)
49
{
50
return
!(
p
== bytecode);
51
}
52
53
protected
:
54
const
char
*
p
;
55
};
56
57
#endif // CPROVER_JAVA_BYTECODE_PATTERN_H
bytecode_infot::mnemonic
const char * mnemonic
Definition:
bytecode_info.h:46
patternt::operator!=
friend bool operator!=(const u1 bytecode, const patternt &p)
Definition:
pattern.h:48
patternt::operator==
friend bool operator==(const u1 bytecode, const patternt &p)
Definition:
pattern.h:43
bytecode_info.h
patternt::patternt
patternt(const char *_p)
Definition:
pattern.h:23
patternt::p
const char * p
Definition:
pattern.h:54
u1
uint8_t u1
Definition:
bytecode_info.h:55
patternt::operator==
bool operator==(const u1 bytecode) const
Definition:
pattern.h:28
patternt
Given a string of the format '?blah?', will return true when compared against a string that matches a...
Definition:
pattern.h:20
bytecode_info
struct bytecode_infot const bytecode_info[]
Definition:
bytecode_info.cpp:16
jbmc
src
java_bytecode
pattern.h
Generated by
1.8.17