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
struct bytecode_infot const bytecode_info[]
uint8_t u1
Definition: bytecode_info.h:55
Given a string of the format '?blah?', will return true when compared against a string that matches a...
Definition: pattern.h:21
bool operator==(const u1 bytecode) const
Definition: pattern.h:28
const char * p
Definition: pattern.h:54
patternt(const char *_p)
Definition: pattern.h:23
friend bool operator==(const u1 bytecode, const patternt &p)
Definition: pattern.h:43
friend bool operator!=(const u1 bytecode, const patternt &p)
Definition: pattern.h:48
const char * mnemonic
Definition: bytecode_info.h:46