cprover
bitvector_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for bitvectors
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10 #define CPROVER_UTIL_BITVECTOR_EXPR_H
11 
14 
15 #include "std_expr.h"
16 
18 class bswap_exprt : public unary_exprt
19 {
20 public:
21  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
22  : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
23  {
24  set_bits_per_byte(bits_per_byte);
25  }
26 
27  bswap_exprt(exprt _op, std::size_t bits_per_byte)
28  : unary_exprt(ID_bswap, std::move(_op))
29  {
30  set_bits_per_byte(bits_per_byte);
31  }
32 
33  std::size_t get_bits_per_byte() const
34  {
35  return get_size_t(ID_bits_per_byte);
36  }
37 
38  void set_bits_per_byte(std::size_t bits_per_byte)
39  {
40  set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
41  }
42 };
43 
44 template <>
45 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
46 {
47  return base.id() == ID_bswap;
48 }
49 
50 inline void validate_expr(const bswap_exprt &value)
51 {
52  validate_operands(value, 1, "bswap must have one operand");
54  value.op().type() == value.type(), "bswap type must match operand type");
55 }
56 
63 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
64 {
65  PRECONDITION(expr.id() == ID_bswap);
66  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
67  validate_expr(ret);
68  return ret;
69 }
70 
73 {
74  PRECONDITION(expr.id() == ID_bswap);
75  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
76  validate_expr(ret);
77  return ret;
78 }
79 
81 class bitnot_exprt : public unary_exprt
82 {
83 public:
84  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
85  {
86  }
87 };
88 
89 template <>
90 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
91 {
92  return base.id() == ID_bitnot;
93 }
94 
95 inline void validate_expr(const bitnot_exprt &value)
96 {
97  validate_operands(value, 1, "Bit-wise not must have one operand");
98 }
99 
106 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
107 {
108  PRECONDITION(expr.id() == ID_bitnot);
109  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
110  validate_expr(ret);
111  return ret;
112 }
113 
116 {
117  PRECONDITION(expr.id() == ID_bitnot);
118  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
119  validate_expr(ret);
120  return ret;
121 }
122 
125 {
126 public:
127  bitor_exprt(const exprt &_op0, exprt _op1)
128  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
129  {
130  }
131 };
132 
133 template <>
134 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
135 {
136  return base.id() == ID_bitor;
137 }
138 
145 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
146 {
147  PRECONDITION(expr.id() == ID_bitor);
148  return static_cast<const bitor_exprt &>(expr);
149 }
150 
153 {
154  PRECONDITION(expr.id() == ID_bitor);
155  return static_cast<bitor_exprt &>(expr);
156 }
157 
160 {
161 public:
163  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
164  {
165  }
166 };
167 
168 template <>
169 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
170 {
171  return base.id() == ID_bitxor;
172 }
173 
180 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
181 {
182  PRECONDITION(expr.id() == ID_bitxor);
183  return static_cast<const bitxor_exprt &>(expr);
184 }
185 
188 {
189  PRECONDITION(expr.id() == ID_bitxor);
190  return static_cast<bitxor_exprt &>(expr);
191 }
192 
195 {
196 public:
197  bitand_exprt(const exprt &_op0, exprt _op1)
198  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
199  {
200  }
201 };
202 
203 template <>
204 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
205 {
206  return base.id() == ID_bitand;
207 }
208 
215 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
216 {
217  PRECONDITION(expr.id() == ID_bitand);
218  return static_cast<const bitand_exprt &>(expr);
219 }
220 
223 {
224  PRECONDITION(expr.id() == ID_bitand);
225  return static_cast<bitand_exprt &>(expr);
226 }
227 
229 class shift_exprt : public binary_exprt
230 {
231 public:
232  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
233  : binary_exprt(std::move(_src), _id, std::move(_distance))
234  {
235  }
236 
237  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
238 
240  {
241  return op0();
242  }
243 
244  const exprt &op() const
245  {
246  return op0();
247  }
248 
250  {
251  return op1();
252  }
253 
254  const exprt &distance() const
255  {
256  return op1();
257  }
258 };
259 
260 template <>
261 inline bool can_cast_expr<shift_exprt>(const exprt &base)
262 {
263  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
264  base.id() == ID_ror || base.id() == ID_rol;
265 }
266 
267 inline void validate_expr(const shift_exprt &value)
268 {
269  validate_operands(value, 2, "Shifts must have two operands");
270 }
271 
278 inline const shift_exprt &to_shift_expr(const exprt &expr)
279 {
280  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
281  validate_expr(ret);
282  return ret;
283 }
284 
287 {
288  shift_exprt &ret = static_cast<shift_exprt &>(expr);
289  validate_expr(ret);
290  return ret;
291 }
292 
294 class shl_exprt : public shift_exprt
295 {
296 public:
297  shl_exprt(exprt _src, exprt _distance)
298  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
299  {
300  }
301 
302  shl_exprt(exprt _src, const std::size_t _distance)
303  : shift_exprt(std::move(_src), ID_shl, _distance)
304  {
305  }
306 };
307 
314 inline const shl_exprt &to_shl_expr(const exprt &expr)
315 {
316  PRECONDITION(expr.id() == ID_shl);
317  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
318  validate_expr(ret);
319  return ret;
320 }
321 
324 {
325  PRECONDITION(expr.id() == ID_shl);
326  shl_exprt &ret = static_cast<shl_exprt &>(expr);
327  validate_expr(ret);
328  return ret;
329 }
330 
332 class ashr_exprt : public shift_exprt
333 {
334 public:
335  ashr_exprt(exprt _src, exprt _distance)
336  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
337  {
338  }
339 
340  ashr_exprt(exprt _src, const std::size_t _distance)
341  : shift_exprt(std::move(_src), ID_ashr, _distance)
342  {
343  }
344 };
345 
347 class lshr_exprt : public shift_exprt
348 {
349 public:
350  lshr_exprt(exprt _src, exprt _distance)
351  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
352  {
353  }
354 
355  lshr_exprt(exprt _src, const std::size_t _distance)
356  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
357  {
358  }
359 };
360 
363 {
364 public:
367  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
368  {
369  }
370 
371  extractbit_exprt(exprt _src, const std::size_t _index);
372 
374  {
375  return op0();
376  }
377 
379  {
380  return op1();
381  }
382 
383  const exprt &src() const
384  {
385  return op0();
386  }
387 
388  const exprt &index() const
389  {
390  return op1();
391  }
392 };
393 
394 template <>
395 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
396 {
397  return base.id() == ID_extractbit;
398 }
399 
400 inline void validate_expr(const extractbit_exprt &value)
401 {
402  validate_operands(value, 2, "Extract bit must have two operands");
403 }
404 
411 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
412 {
413  PRECONDITION(expr.id() == ID_extractbit);
414  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
415  validate_expr(ret);
416  return ret;
417 }
418 
421 {
422  PRECONDITION(expr.id() == ID_extractbit);
423  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
424  validate_expr(ret);
425  return ret;
426 }
427 
430 {
431 public:
437  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
438  : expr_protectedt(
439  ID_extractbits,
440  std::move(_type),
441  {std::move(_src), std::move(_upper), std::move(_lower)})
442  {
443  }
444 
446  exprt _src,
447  const std::size_t _upper,
448  const std::size_t _lower,
449  typet _type);
450 
452  {
453  return op0();
454  }
455 
457  {
458  return op1();
459  }
460 
462  {
463  return op2();
464  }
465 
466  const exprt &src() const
467  {
468  return op0();
469  }
470 
471  const exprt &upper() const
472  {
473  return op1();
474  }
475 
476  const exprt &lower() const
477  {
478  return op2();
479  }
480 };
481 
482 template <>
483 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
484 {
485  return base.id() == ID_extractbits;
486 }
487 
488 inline void validate_expr(const extractbits_exprt &value)
489 {
490  validate_operands(value, 3, "Extract bits must have three operands");
491 }
492 
499 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
500 {
501  PRECONDITION(expr.id() == ID_extractbits);
502  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
503  validate_expr(ret);
504  return ret;
505 }
506 
509 {
510  PRECONDITION(expr.id() == ID_extractbits);
511  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
512  validate_expr(ret);
513  return ret;
514 }
515 
518 {
519 public:
521  : binary_exprt(
522  std::move(_times),
523  ID_replication,
524  std::move(_src),
525  std::move(_type))
526  {
527  }
528 
530  {
531  return static_cast<constant_exprt &>(op0());
532  }
533 
534  const constant_exprt &times() const
535  {
536  return static_cast<const constant_exprt &>(op0());
537  }
538 
540  {
541  return op1();
542  }
543 
544  const exprt &op() const
545  {
546  return op1();
547  }
548 };
549 
550 template <>
551 inline bool can_cast_expr<replication_exprt>(const exprt &base)
552 {
553  return base.id() == ID_replication;
554 }
555 
556 inline void validate_expr(const replication_exprt &value)
557 {
558  validate_operands(value, 2, "Bit-wise replication must have two operands");
559 }
560 
567 inline const replication_exprt &to_replication_expr(const exprt &expr)
568 {
569  PRECONDITION(expr.id() == ID_replication);
570  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
571  validate_expr(ret);
572  return ret;
573 }
574 
577 {
578  PRECONDITION(expr.id() == ID_replication);
579  replication_exprt &ret = static_cast<replication_exprt &>(expr);
580  validate_expr(ret);
581  return ret;
582 }
583 
590 {
591 public:
593  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
594  {
595  }
596 
598  : multi_ary_exprt(
599  ID_concatenation,
600  {std::move(_op0), std::move(_op1)},
601  std::move(_type))
602  {
603  }
604 };
605 
606 template <>
608 {
609  return base.id() == ID_concatenation;
610 }
611 
619 {
620  PRECONDITION(expr.id() == ID_concatenation);
621  return static_cast<const concatenation_exprt &>(expr);
622 }
623 
626 {
627  PRECONDITION(expr.id() == ID_concatenation);
628  return static_cast<concatenation_exprt &>(expr);
629 }
630 
633 {
634 public:
636  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
637  {
638  }
639 
640  explicit popcount_exprt(const exprt &_op)
641  : unary_exprt(ID_popcount, _op, _op.type())
642  {
643  }
644 };
645 
646 template <>
647 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
648 {
649  return base.id() == ID_popcount;
650 }
651 
652 inline void validate_expr(const popcount_exprt &value)
653 {
654  validate_operands(value, 1, "popcount must have one operand");
655 }
656 
663 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
664 {
665  PRECONDITION(expr.id() == ID_popcount);
666  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
667  validate_expr(ret);
668  return ret;
669 }
670 
673 {
674  PRECONDITION(expr.id() == ID_popcount);
675  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
676  validate_expr(ret);
677  return ret;
678 }
679 
680 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: bitvector_expr.h:411
shl_exprt::shl_exprt
shl_exprt(exprt _src, const std::size_t _distance)
Definition: bitvector_expr.h:302
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
extractbits_exprt::lower
exprt & lower()
Definition: bitvector_expr.h:461
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: bitvector_expr.h:232
can_cast_expr< bitor_exprt >
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: bitvector_expr.h:134
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, exprt _distance)
Definition: bitvector_expr.h:350
can_cast_expr< replication_exprt >
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: bitvector_expr.h:551
to_bitor_expr
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: bitvector_expr.h:145
typet
The type of an expression, extends irept.
Definition: type.h:28
can_cast_expr< shift_exprt >
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: bitvector_expr.h:261
can_cast_expr< concatenation_exprt >
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: bitvector_expr.h:607
extractbits_exprt::src
const exprt & src() const
Definition: bitvector_expr.h:466
replication_exprt::times
constant_exprt & times()
Definition: bitvector_expr.h:529
validate_operands
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
can_cast_expr< bitand_exprt >
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: bitvector_expr.h:204
bitxor_exprt::bitxor_exprt
bitxor_exprt(exprt _op0, exprt _op1)
Definition: bitvector_expr.h:162
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:282
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, exprt _distance)
Definition: bitvector_expr.h:335
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:551
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte)
Definition: bitvector_expr.h:27
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: bitvector_expr.h:33
extractbits_exprt::upper
const exprt & upper() const
Definition: bitvector_expr.h:471
replication_exprt::op
const exprt & op() const
Definition: bitvector_expr.h:544
expr_protectedt::op1
exprt & op1()
Definition: expr.h:106
concatenation_exprt
Concatenation of bit-vector operands.
Definition: bitvector_expr.h:590
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: bitvector_expr.h:106
replication_exprt::replication_exprt
replication_exprt(constant_exprt _times, exprt _src, typet _type)
Definition: bitvector_expr.h:520
can_cast_expr< bitnot_exprt >
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: bitvector_expr.h:90
lshr_exprt
Logical right shift.
Definition: bitvector_expr.h:348
shift_exprt::op
exprt & op()
Definition: bitvector_expr.h:239
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: bitvector_expr.h:663
replication_exprt
Bit-vector replication.
Definition: bitvector_expr.h:518
replication_exprt::op
exprt & op()
Definition: bitvector_expr.h:539
can_cast_expr< extractbit_exprt >
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: bitvector_expr.h:395
extractbits_exprt::upper
exprt & upper()
Definition: bitvector_expr.h:456
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: bitvector_expr.h:63
validate_expr
void validate_expr(const bswap_exprt &value)
Definition: bitvector_expr.h:50
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
expr_protectedt::op0
exprt & op0()
Definition: expr.h:103
bitxor_exprt
Bit-wise XOR.
Definition: bitvector_expr.h:160
bitor_exprt
Bit-wise OR.
Definition: bitvector_expr.h:125
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
bitor_exprt::bitor_exprt
bitor_exprt(const exprt &_op0, exprt _op1)
Definition: bitvector_expr.h:127
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:644
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
extractbits_exprt::lower
const exprt & lower() const
Definition: bitvector_expr.h:476
shl_exprt::shl_exprt
shl_exprt(exprt _src, exprt _distance)
Definition: bitvector_expr.h:297
extractbits_exprt::src
exprt & src()
Definition: bitvector_expr.h:451
concatenation_exprt::concatenation_exprt
concatenation_exprt(operandst _operands, typet _type)
Definition: bitvector_expr.h:592
extractbit_exprt::index
exprt & index()
Definition: bitvector_expr.h:378
irept::id
const irep_idt & id() const
Definition: irep.h:407
popcount_exprt::popcount_exprt
popcount_exprt(const exprt &_op)
Definition: bitvector_expr.h:640
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
bitand_exprt
Bit-wise AND.
Definition: bitvector_expr.h:195
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: bitvector_expr.h:314
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: bitvector_expr.h:278
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: bitvector_expr.h:82
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: bitvector_expr.h:363
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: bitvector_expr.h:618
extractbit_exprt::extractbit_exprt
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: bitvector_expr.h:366
shift_exprt
A base class for shift and rotate operators.
Definition: bitvector_expr.h:230
can_cast_expr< bitxor_exprt >
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: bitvector_expr.h:169
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: bitvector_expr.h:437
bitand_exprt::bitand_exprt
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: bitvector_expr.h:197
shift_exprt::distance
exprt & distance()
Definition: bitvector_expr.h:249
can_cast_expr< bswap_exprt >
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: bitvector_expr.h:45
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
extractbit_exprt::src
exprt & src()
Definition: bitvector_expr.h:373
ashr_exprt
Arithmetic right shift.
Definition: bitvector_expr.h:333
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: bitvector_expr.h:355
extractbit_exprt::index
const exprt & index() const
Definition: bitvector_expr.h:388
can_cast_expr< extractbits_exprt >
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: bitvector_expr.h:483
bswap_exprt::set_bits_per_byte
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: bitvector_expr.h:38
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: bitvector_expr.h:499
can_cast_expr< popcount_exprt >
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: bitvector_expr.h:647
concatenation_exprt::concatenation_exprt
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: bitvector_expr.h:597
bswap_exprt
The byte swap expression.
Definition: bitvector_expr.h:19
shift_exprt::distance
const exprt & distance() const
Definition: bitvector_expr.h:254
shift_exprt::op
const exprt & op() const
Definition: bitvector_expr.h:244
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: bitvector_expr.h:430
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: bitvector_expr.h:340
to_bitand_expr
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: bitvector_expr.h:215
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: bitvector_expr.h:633
replication_exprt::times
const constant_exprt & times() const
Definition: bitvector_expr.h:534
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
Definition: bitvector_expr.h:21
std_expr.h
API to expression classes.
expr_protectedt::op2
exprt & op2()
Definition: expr.h:109
popcount_exprt::popcount_exprt
popcount_exprt(exprt _op, typet _type)
Definition: bitvector_expr.h:635
bitnot_exprt::bitnot_exprt
bitnot_exprt(exprt op)
Definition: bitvector_expr.h:84
extractbit_exprt::src
const exprt & src() const
Definition: bitvector_expr.h:383
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: bitvector_expr.h:567
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
expr_protectedt
Base class for all expressions.
Definition: expr.h:347
shl_exprt
Left shift.
Definition: bitvector_expr.h:295
to_bitxor_expr
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: bitvector_expr.h:180