cprover
byte_operators.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_UTIL_BYTE_OPERATORS_H
11 #define CPROVER_UTIL_BYTE_OPERATORS_H
12 
20 #include "std_expr.h"
21 
25 {
26 public:
28  {
29  }
30 
31  explicit byte_extract_exprt(irep_idt _id, const typet &_type):
32  binary_exprt(_id, _type)
33  {
34  }
35 
37  irep_idt _id,
38  const exprt &_op, const exprt &_offset, const typet &_type):
39  binary_exprt(_id, _type)
40  {
41  op()=_op;
42  offset()=_offset;
43  }
44 
45  exprt &op() { return op0(); }
46  exprt &offset() { return op1(); }
47 
48  const exprt &op() const { return op0(); }
49  const exprt &offset() const { return op1(); }
50 };
51 
52 inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
53 {
54  assert(expr.operands().size()==2);
55  return static_cast<const byte_extract_exprt &>(expr);
56 }
57 
59 {
60  assert(expr.operands().size()==2);
61  return static_cast<byte_extract_exprt &>(expr);
62 }
63 
66 
70 {
71 public:
73  byte_extract_exprt(ID_byte_extract_little_endian)
74  {
75  }
76 };
77 
80 {
81  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
82  return static_cast<const byte_extract_little_endian_exprt &>(expr);
83 }
84 
87 {
88  assert(expr.id()==ID_byte_extract_little_endian && expr.operands().size()==2);
89  return static_cast<byte_extract_little_endian_exprt &>(expr);
90 }
91 
95 {
96 public:
98  byte_extract_exprt(ID_byte_extract_big_endian)
99  {
100  }
101 
103  const exprt &_op, const exprt &_offset, const typet &_type):
104  byte_extract_exprt(ID_byte_extract_big_endian, _op, _offset, _type)
105  {
106  }
107 };
108 
111 {
112  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
113  return static_cast<const byte_extract_big_endian_exprt &>(expr);
114 }
115 
118 {
119  assert(expr.id()==ID_byte_extract_big_endian && expr.operands().size()==2);
120  return static_cast<byte_extract_big_endian_exprt &>(expr);
121 }
122 
126 {
127 public:
128  explicit byte_update_exprt(irep_idt _id):exprt(_id)
129  {
130  operands().resize(3);
131  }
132 
133  byte_update_exprt(irep_idt _id, const typet &_type):
134  exprt(_id, _type)
135  {
136  operands().resize(3);
137  }
138 
140  irep_idt _id,
141  const exprt &_op, const exprt &_offset, const exprt &_value):
142  exprt(_id, _op.type())
143  {
144  copy_to_operands(_op, _offset, _value);
145  }
146 
147  exprt &op() { return op0(); }
148  exprt &offset() { return op1(); }
149  exprt &value() { return op2(); }
150 
151  const exprt &op() const { return op0(); }
152  const exprt &offset() const { return op1(); }
153  const exprt &value() const { return op2(); }
154 };
155 
156 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
157 {
158  assert(expr.operands().size()==3);
159  return static_cast<const byte_update_exprt &>(expr);
160 }
161 
163 {
164  assert(expr.operands().size()==3);
165  return static_cast<byte_update_exprt &>(expr);
166 }
167 
171 {
172 public:
174  byte_update_exprt(ID_byte_update_little_endian)
175  {
176  }
177 
179  const exprt &_op, const exprt &_offset, const exprt &_value):
180  byte_update_exprt(ID_byte_update_little_endian, _op, _offset, _value)
181  {
182  }
183 };
184 
187 {
188  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
189  return static_cast<const byte_update_little_endian_exprt &>(expr);
190 }
191 
194 {
195  assert(expr.id()==ID_byte_update_little_endian && expr.operands().size()==3);
196  return static_cast<byte_update_little_endian_exprt &>(expr);
197 }
198 
202 {
203 public:
205  byte_update_exprt(ID_byte_update_big_endian)
206  {
207  }
208 
210  const exprt &_op, const exprt &_offset, const exprt &_value):
211  byte_update_exprt(ID_byte_update_big_endian, _op, _offset, _value)
212  {
213  }
214 };
215 
216 inline const byte_update_big_endian_exprt
218 {
219  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
220  return static_cast<const byte_update_big_endian_exprt &>(expr);
221 }
222 
225 {
226  assert(expr.id()==ID_byte_update_big_endian && expr.operands().size()==3);
227  return static_cast<byte_update_big_endian_exprt &>(expr);
228 }
229 
230 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
byte_extract_exprt(irep_idt _id, const typet &_type)
The type of an expression.
Definition: type.h:22
byte_extract_exprt(irep_idt _id)
const byte_update_big_endian_exprt & to_byte_update_big_endian_expr(const exprt &expr)
const exprt & offset() const
const byte_update_little_endian_exprt & to_byte_update_little_endian_expr(const exprt &expr)
irep_idt byte_update_id()
const exprt & op() const
exprt & op0()
Definition: expr.h:72
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const exprt & value() const
typet & type()
Definition: expr.h:56
const exprt & op() const
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const typet &_type)
const irep_idt & id() const
Definition: irep.h:189
byte_extract_big_endian_exprt(const exprt &_op, const exprt &_offset, const typet &_type)
A generic base class for binary expressions.
Definition: std_expr.h:649
const exprt & offset() const
API to expression classes.
exprt & op1()
Definition: expr.h:75
irep_idt byte_extract_id()
byte_update_big_endian_exprt(const exprt &_op, const exprt &_offset, const exprt &_value)
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
const byte_extract_little_endian_exprt & to_byte_extract_little_endian_expr(const exprt &expr)
byte_update_exprt(irep_idt _id, const typet &_type)
const byte_extract_big_endian_exprt & to_byte_extract_big_endian_expr(const exprt &expr)
Base class for all expressions.
Definition: expr.h:42
TO_BE_DOCUMENTED.
exprt & op2()
Definition: expr.h:78
byte_update_exprt(irep_idt _id)
byte_update_little_endian_exprt(const exprt &_op, const exprt &_offset, const exprt &_value)
operandst & operands()
Definition: expr.h:66
TO_BE_DOCUMENTED.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)