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
byte_extract_exprt(irep_idt _id, const typet &_type)
The type of an expression, extends irept.
Definition: type.h:27
byte_extract_exprt(irep_idt _id)
const exprt & offset() const
irep_idt byte_update_id()
const exprt & op() const
exprt & op0()
Definition: expr.h:84
const exprt & value() const
typet & type()
Return the type of the expression.
Definition: expr.h:68
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)
A base class for binary expressions.
Definition: std_expr.h:738
const exprt & offset() const
API to expression classes.
exprt & op1()
Definition: expr.h:87
irep_idt byte_extract_id()
An expression with three operands.
Definition: std_expr.h:59
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
byte_update_exprt(irep_idt _id, const exprt &_op, const exprt &_offset, const exprt &_value)
Base class for all expressions.
Definition: expr.h:54
TO_BE_DOCUMENTED.
exprt & op2()
Definition: expr.h:90
operandst & operands()
Definition: expr.h:78
TO_BE_DOCUMENTED.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)