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 "invariant.h"
21 #include "std_expr.h"
22 
26 {
27 public:
29  {
30  }
31 
32  explicit byte_extract_exprt(irep_idt _id, const typet &_type):
33  binary_exprt(_id, _type)
34  {
35  }
36 
38  irep_idt _id,
39  const exprt &_op, const exprt &_offset, const typet &_type):
40  binary_exprt(_id, _type)
41  {
42  op()=_op;
43  offset()=_offset;
44  }
45 
46  exprt &op() { return op0(); }
47  exprt &offset() { return op1(); }
48 
49  const exprt &op() const { return op0(); }
50  const exprt &offset() const { return op1(); }
51 };
52 
53 inline const byte_extract_exprt &to_byte_extract_expr(const exprt &expr)
54 {
55  PRECONDITION(expr.operands().size() == 2);
56  return static_cast<const byte_extract_exprt &>(expr);
57 }
58 
60 {
61  PRECONDITION(expr.operands().size() == 2);
62  return static_cast<byte_extract_exprt &>(expr);
63 }
64 
67 
71 {
72 public:
74  irep_idt _id,
75  const exprt &_op,
76  const exprt &_offset,
77  const exprt &_value)
78  : ternary_exprt(_id, _op, _offset, _value, _op.type())
79  {
80  }
81 
82  exprt &op() { return op0(); }
83  exprt &offset() { return op1(); }
84  exprt &value() { return op2(); }
85 
86  const exprt &op() const { return op0(); }
87  const exprt &offset() const { return op1(); }
88  const exprt &value() const { return op2(); }
89 };
90 
91 inline const byte_update_exprt &to_byte_update_expr(const exprt &expr)
92 {
93  PRECONDITION(expr.operands().size() == 3);
94  return static_cast<const byte_update_exprt &>(expr);
95 }
96 
98 {
99  PRECONDITION(expr.operands().size() == 3);
100  return static_cast<byte_update_exprt &>(expr);
101 }
102 
103 #endif // CPROVER_UTIL_BYTE_OPERATORS_H
exprt::op2
exprt & op2()
Definition: expr.h:90
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
byte_update_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:70
byte_extract_exprt::op
const exprt & op() const
Definition: byte_operators.h:49
typet
The type of an expression, extends irept.
Definition: type.h:27
ternary_exprt
An expression with three operands.
Definition: std_expr.h:59
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:53
byte_update_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:87
byte_extract_exprt::byte_extract_exprt
byte_extract_exprt(irep_idt _id)
Definition: byte_operators.h:28
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:738
exprt::op0
exprt & op0()
Definition: expr.h:84
invariant.h
byte_extract_exprt::byte_extract_exprt
byte_extract_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const typet &_type)
Definition: byte_operators.h:37
byte_extract_exprt::offset
const exprt & offset() const
Definition: byte_operators.h:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
byte_extract_exprt::op
exprt & op()
Definition: byte_operators.h:46
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
to_byte_update_expr
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
Definition: byte_operators.h:91
exprt::op1
exprt & op1()
Definition: expr.h:87
byte_update_id
irep_idt byte_update_id()
Definition: byte_operators.cpp:28
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:47
byte_update_exprt::value
const exprt & value() const
Definition: byte_operators.h:88
byte_extract_exprt::byte_extract_exprt
byte_extract_exprt(irep_idt _id, const typet &_type)
Definition: byte_operators.h:32
byte_update_exprt::value
exprt & value()
Definition: byte_operators.h:84
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
byte_update_exprt::offset
exprt & offset()
Definition: byte_operators.h:83
exprt::operands
operandst & operands()
Definition: expr.h:78
byte_update_exprt::op
exprt & op()
Definition: byte_operators.h:82
std_expr.h
byte_update_exprt::op
const exprt & op() const
Definition: byte_operators.h:86
byte_update_exprt::byte_update_exprt
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
Definition: byte_operators.h:73