CBMC
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_size_t(ID_bits_per_byte, 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 
308 template <>
309 inline bool can_cast_expr<shl_exprt>(const exprt &base)
310 {
311  return base.id() == ID_shl;
312 }
313 
320 inline const shl_exprt &to_shl_expr(const exprt &expr)
321 {
322  PRECONDITION(expr.id() == ID_shl);
323  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
324  validate_expr(ret);
325  return ret;
326 }
327 
330 {
331  PRECONDITION(expr.id() == ID_shl);
332  shl_exprt &ret = static_cast<shl_exprt &>(expr);
333  validate_expr(ret);
334  return ret;
335 }
336 
338 class ashr_exprt : public shift_exprt
339 {
340 public:
341  ashr_exprt(exprt _src, exprt _distance)
342  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
343  {
344  }
345 
346  ashr_exprt(exprt _src, const std::size_t _distance)
347  : shift_exprt(std::move(_src), ID_ashr, _distance)
348  {
349  }
350 };
351 
352 template <>
353 inline bool can_cast_expr<ashr_exprt>(const exprt &base)
354 {
355  return base.id() == ID_ashr;
356 }
357 
359 class lshr_exprt : public shift_exprt
360 {
361 public:
362  lshr_exprt(exprt _src, exprt _distance)
363  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
364  {
365  }
366 
367  lshr_exprt(exprt _src, const std::size_t _distance)
368  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
369  {
370  }
371 };
372 
373 template <>
374 inline bool can_cast_expr<lshr_exprt>(const exprt &base)
375 {
376  return base.id() == ID_lshr;
377 }
378 
381 {
382 public:
385  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
386  {
387  }
388 
389  extractbit_exprt(exprt _src, const std::size_t _index);
390 
392  {
393  return op0();
394  }
395 
397  {
398  return op1();
399  }
400 
401  const exprt &src() const
402  {
403  return op0();
404  }
405 
406  const exprt &index() const
407  {
408  return op1();
409  }
410 };
411 
412 template <>
413 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
414 {
415  return base.id() == ID_extractbit;
416 }
417 
418 inline void validate_expr(const extractbit_exprt &value)
419 {
420  validate_operands(value, 2, "Extract bit must have two operands");
421 }
422 
429 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
430 {
431  PRECONDITION(expr.id() == ID_extractbit);
432  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
433  validate_expr(ret);
434  return ret;
435 }
436 
439 {
440  PRECONDITION(expr.id() == ID_extractbit);
441  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
442  validate_expr(ret);
443  return ret;
444 }
445 
448 {
449 public:
455  extractbits_exprt(exprt _src, exprt _index, typet _type)
456  : expr_protectedt(
457  ID_extractbits,
458  std::move(_type),
459  {std::move(_src), std::move(_index)})
460  {
461  }
462 
463  extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
464 
466  {
467  return op0();
468  }
469 
471  {
472  return op1();
473  }
474 
475  const exprt &src() const
476  {
477  return op0();
478  }
479 
480  const exprt &index() const
481  {
482  return op1();
483  }
484 };
485 
486 template <>
487 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
488 {
489  return base.id() == ID_extractbits;
490 }
491 
492 inline void validate_expr(const extractbits_exprt &value)
493 {
494  validate_operands(value, 2, "Extractbits must have two operands");
495 }
496 
503 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
504 {
505  PRECONDITION(expr.id() == ID_extractbits);
506  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
507  validate_expr(ret);
508  return ret;
509 }
510 
513 {
514  PRECONDITION(expr.id() == ID_extractbits);
515  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
516  validate_expr(ret);
517  return ret;
518 }
519 
522 {
523 public:
528  update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
529  : expr_protectedt(
530  ID_update_bit,
531  _src.type(),
532  {_src, std::move(_index), std::move(_new_value)})
533  {
534  PRECONDITION(new_value().type().id() == ID_bool);
535  }
536 
537  update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
538 
540  {
541  return op0();
542  }
543 
545  {
546  return op1();
547  }
548 
550  {
551  return op2();
552  }
553 
554  const exprt &src() const
555  {
556  return op0();
557  }
558 
559  const exprt &index() const
560  {
561  return op1();
562  }
563 
564  const exprt &new_value() const
565  {
566  return op2();
567  }
568 
569  static void check(
570  const exprt &expr,
572  {
573  validate_operands(expr, 3, "update_bit must have three operands");
574  }
575 
577  exprt lower() const;
578 };
579 
580 template <>
581 inline bool can_cast_expr<update_bit_exprt>(const exprt &base)
582 {
583  return base.id() == ID_update_bit;
584 }
585 
592 inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
593 {
594  PRECONDITION(expr.id() == ID_update_bit);
596  return static_cast<const update_bit_exprt &>(expr);
597 }
598 
601 {
602  PRECONDITION(expr.id() == ID_update_bit);
604  return static_cast<update_bit_exprt &>(expr);
605 }
606 
609 {
610 public:
615  update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
616  : expr_protectedt(
617  ID_update_bits,
618  _src.type(),
619  {_src, std::move(_index), std::move(_new_value)})
620  {
621  }
622 
623  update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
624 
626  {
627  return op0();
628  }
629 
631  {
632  return op1();
633  }
634 
636  {
637  return op2();
638  }
639 
640  const exprt &src() const
641  {
642  return op0();
643  }
644 
645  const exprt &index() const
646  {
647  return op1();
648  }
649 
650  const exprt &new_value() const
651  {
652  return op2();
653  }
654 
655  static void check(
656  const exprt &expr,
658  {
659  validate_operands(expr, 3, "update_bits must have three operands");
660  }
661 
663  exprt lower() const;
664 };
665 
666 template <>
667 inline bool can_cast_expr<update_bits_exprt>(const exprt &base)
668 {
669  return base.id() == ID_update_bits;
670 }
671 
678 inline const update_bits_exprt &to_update_bits_expr(const exprt &expr)
679 {
680  PRECONDITION(expr.id() == ID_update_bits);
682  return static_cast<const update_bits_exprt &>(expr);
683 }
684 
687 {
688  PRECONDITION(expr.id() == ID_update_bits);
690  return static_cast<update_bits_exprt &>(expr);
691 }
692 
695 {
696 public:
698  : binary_exprt(
699  std::move(_times),
700  ID_replication,
701  std::move(_src),
702  std::move(_type))
703  {
704  }
705 
707  {
708  return static_cast<constant_exprt &>(op0());
709  }
710 
711  const constant_exprt &times() const
712  {
713  return static_cast<const constant_exprt &>(op0());
714  }
715 
717  {
718  return op1();
719  }
720 
721  const exprt &op() const
722  {
723  return op1();
724  }
725 };
726 
727 template <>
728 inline bool can_cast_expr<replication_exprt>(const exprt &base)
729 {
730  return base.id() == ID_replication;
731 }
732 
733 inline void validate_expr(const replication_exprt &value)
734 {
735  validate_operands(value, 2, "Bit-wise replication must have two operands");
736 }
737 
744 inline const replication_exprt &to_replication_expr(const exprt &expr)
745 {
746  PRECONDITION(expr.id() == ID_replication);
747  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
748  validate_expr(ret);
749  return ret;
750 }
751 
754 {
755  PRECONDITION(expr.id() == ID_replication);
756  replication_exprt &ret = static_cast<replication_exprt &>(expr);
757  validate_expr(ret);
758  return ret;
759 }
760 
767 {
768 public:
770  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
771  {
772  }
773 
775  : multi_ary_exprt(
776  ID_concatenation,
777  {std::move(_op0), std::move(_op1)},
778  std::move(_type))
779  {
780  }
781 };
782 
783 template <>
785 {
786  return base.id() == ID_concatenation;
787 }
788 
796 {
797  PRECONDITION(expr.id() == ID_concatenation);
798  return static_cast<const concatenation_exprt &>(expr);
799 }
800 
803 {
804  PRECONDITION(expr.id() == ID_concatenation);
805  return static_cast<concatenation_exprt &>(expr);
806 }
807 
810 {
811 public:
813  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
814  {
815  }
816 
817  explicit popcount_exprt(const exprt &_op)
818  : unary_exprt(ID_popcount, _op, _op.type())
819  {
820  }
821 
824  exprt lower() const;
825 };
826 
827 template <>
828 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
829 {
830  return base.id() == ID_popcount;
831 }
832 
833 inline void validate_expr(const popcount_exprt &value)
834 {
835  validate_operands(value, 1, "popcount must have one operand");
836 }
837 
844 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
845 {
846  PRECONDITION(expr.id() == ID_popcount);
847  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
848  validate_expr(ret);
849  return ret;
850 }
851 
854 {
855  PRECONDITION(expr.id() == ID_popcount);
856  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
857  validate_expr(ret);
858  return ret;
859 }
860 
864 {
865 public:
866  binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
867  : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
868  {
869  INVARIANT(
870  valid_id(id()),
871  "The kind used to construct binary_overflow_exprt should be in the set "
872  "of expected valid kinds.");
873  }
874 
875  static void check(
876  const exprt &expr,
878  {
879  binary_exprt::check(expr, vm);
880 
881  if(expr.id() != ID_overflow_shl)
882  {
883  const binary_exprt &binary_expr = to_binary_expr(expr);
884  DATA_CHECK(
885  vm,
886  binary_expr.lhs().type() == binary_expr.rhs().type(),
887  "operand types must match");
888  }
889  }
890 
891  static void validate(
892  const exprt &expr,
893  const namespacet &,
895  {
896  check(expr, vm);
897  }
898 
900  static bool valid_id(const irep_idt &id)
901  {
902  return id == ID_overflow_plus || id == ID_overflow_mult ||
903  id == ID_overflow_minus || id == ID_overflow_shl;
904  }
905 
906 private:
907  static irep_idt make_id(const irep_idt &kind)
908  {
909  if(valid_id(kind))
910  return kind;
911  else
912  return "overflow-" + id2string(kind);
913  }
914 };
915 
916 template <>
918 {
919  return binary_overflow_exprt::valid_id(base.id());
920 }
921 
922 inline void validate_expr(const binary_overflow_exprt &value)
923 {
925  value, 2, "binary overflow expression must have two operands");
926 }
927 
935 {
936  PRECONDITION(
937  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
938  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
939  const binary_overflow_exprt &ret =
940  static_cast<const binary_overflow_exprt &>(expr);
941  validate_expr(ret);
942  return ret;
943 }
944 
947 {
948  PRECONDITION(
949  expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
950  expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
951  binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
952  validate_expr(ret);
953  return ret;
954 }
955 
957 {
958 public:
960  : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
961  {
962  }
963 
966  exprt lower() const;
967 };
968 
969 template <>
971 {
972  return base.id() == ID_overflow_plus;
973 }
974 
976 {
977 public:
979  : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
980  {
981  }
982 
985  exprt lower() const;
986 };
987 
988 template <>
990 {
991  return base.id() == ID_overflow_minus;
992 }
993 
995 {
996 public:
998  : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
999  {
1000  }
1001 
1004  exprt lower() const;
1005 };
1006 
1007 template <>
1009 {
1010  return base.id() == ID_overflow_mult;
1011 }
1012 
1014 {
1015 public:
1017  : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
1018  {
1019  }
1020 };
1021 
1022 template <>
1024 {
1025  return base.id() == ID_overflow_shl;
1026 }
1027 
1031 {
1032 public:
1034  : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
1035  {
1036  }
1037 
1038  static void check(
1039  const exprt &expr,
1041  {
1042  unary_exprt::check(expr, vm);
1043  }
1044 
1045  static void validate(
1046  const exprt &expr,
1047  const namespacet &,
1049  {
1050  check(expr, vm);
1051  }
1052 };
1053 
1054 template <>
1056 {
1057  return base.id() == ID_overflow_unary_minus;
1058 }
1059 
1060 inline void validate_expr(const unary_overflow_exprt &value)
1061 {
1063  value, 1, "unary overflow expression must have one operand");
1064 }
1065 
1069 {
1070 public:
1072  : unary_overflow_exprt(ID_unary_minus, std::move(_op))
1073  {
1074  }
1075 
1076  static void check(
1077  const exprt &expr,
1079  {
1080  unary_exprt::check(expr, vm);
1081  }
1082 
1083  static void validate(
1084  const exprt &expr,
1085  const namespacet &,
1087  {
1088  check(expr, vm);
1089  }
1090 };
1091 
1092 template <>
1094 {
1095  return base.id() == ID_overflow_unary_minus;
1096 }
1097 
1099 {
1101  value, 1, "unary minus overflow expression must have one operand");
1102 }
1103 
1111 {
1112  PRECONDITION(expr.id() == ID_overflow_unary_minus);
1113  const unary_overflow_exprt &ret =
1114  static_cast<const unary_overflow_exprt &>(expr);
1115  validate_expr(ret);
1116  return ret;
1117 }
1118 
1121 {
1122  PRECONDITION(expr.id() == ID_overflow_unary_minus);
1123  unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
1124  validate_expr(ret);
1125  return ret;
1126 }
1127 
1134 {
1135 public:
1136  count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1137  : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
1138  {
1139  zero_permitted(_zero_permitted);
1140  }
1141 
1142  explicit count_leading_zeros_exprt(const exprt &_op)
1143  : count_leading_zeros_exprt(_op, true, _op.type())
1144  {
1145  }
1146 
1147  bool zero_permitted() const
1148  {
1149  return !get_bool(ID_C_bounds_check);
1150  }
1151 
1152  void zero_permitted(bool value)
1153  {
1154  set(ID_C_bounds_check, !value);
1155  }
1156 
1157  static void check(
1158  const exprt &expr,
1160  {
1161  DATA_CHECK(
1162  vm,
1163  expr.operands().size() == 1,
1164  "unary expression must have a single operand");
1165  DATA_CHECK(
1166  vm,
1168  "operand must be of bitvector type");
1169  }
1170 
1171  static void validate(
1172  const exprt &expr,
1173  const namespacet &,
1175  {
1176  check(expr, vm);
1177  }
1178 
1181  exprt lower() const;
1182 };
1183 
1184 template <>
1186 {
1187  return base.id() == ID_count_leading_zeros;
1188 }
1189 
1190 inline void validate_expr(const count_leading_zeros_exprt &value)
1191 {
1192  validate_operands(value, 1, "count_leading_zeros must have one operand");
1193 }
1194 
1201 inline const count_leading_zeros_exprt &
1203 {
1204  PRECONDITION(expr.id() == ID_count_leading_zeros);
1205  const count_leading_zeros_exprt &ret =
1206  static_cast<const count_leading_zeros_exprt &>(expr);
1207  validate_expr(ret);
1208  return ret;
1209 }
1210 
1213 {
1214  PRECONDITION(expr.id() == ID_count_leading_zeros);
1216  static_cast<count_leading_zeros_exprt &>(expr);
1217  validate_expr(ret);
1218  return ret;
1219 }
1220 
1227 {
1228 public:
1229  count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
1230  : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
1231  {
1232  zero_permitted(_zero_permitted);
1233  }
1234 
1235  explicit count_trailing_zeros_exprt(const exprt &_op)
1236  : count_trailing_zeros_exprt(_op, true, _op.type())
1237  {
1238  }
1239 
1240  bool zero_permitted() const
1241  {
1242  return !get_bool(ID_C_bounds_check);
1243  }
1244 
1245  void zero_permitted(bool value)
1246  {
1247  set(ID_C_bounds_check, !value);
1248  }
1249 
1250  static void check(
1251  const exprt &expr,
1253  {
1254  DATA_CHECK(
1255  vm,
1256  expr.operands().size() == 1,
1257  "unary expression must have a single operand");
1258  DATA_CHECK(
1259  vm,
1261  "operand must be of bitvector type");
1262  }
1263 
1264  static void validate(
1265  const exprt &expr,
1266  const namespacet &,
1268  {
1269  check(expr, vm);
1270  }
1271 
1274  exprt lower() const;
1275 };
1276 
1277 template <>
1279 {
1280  return base.id() == ID_count_trailing_zeros;
1281 }
1282 
1284 {
1285  validate_operands(value, 1, "count_trailing_zeros must have one operand");
1286 }
1287 
1294 inline const count_trailing_zeros_exprt &
1296 {
1297  PRECONDITION(expr.id() == ID_count_trailing_zeros);
1298  const count_trailing_zeros_exprt &ret =
1299  static_cast<const count_trailing_zeros_exprt &>(expr);
1300  validate_expr(ret);
1301  return ret;
1302 }
1303 
1306 {
1307  PRECONDITION(expr.id() == ID_count_trailing_zeros);
1309  static_cast<count_trailing_zeros_exprt &>(expr);
1310  validate_expr(ret);
1311  return ret;
1312 }
1313 
1316 {
1317 public:
1319  : unary_exprt(ID_bitreverse, std::move(op))
1320  {
1321  }
1322 
1325  exprt lower() const;
1326 };
1327 
1328 template <>
1329 inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
1330 {
1331  return base.id() == ID_bitreverse;
1332 }
1333 
1334 inline void validate_expr(const bitreverse_exprt &value)
1335 {
1336  validate_operands(value, 1, "Bit-wise reverse must have one operand");
1337 }
1338 
1345 inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
1346 {
1347  PRECONDITION(expr.id() == ID_bitreverse);
1348  const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1349  validate_expr(ret);
1350  return ret;
1351 }
1352 
1355 {
1356  PRECONDITION(expr.id() == ID_bitreverse);
1357  bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1358  validate_expr(ret);
1359  return ret;
1360 }
1361 
1364 {
1365 public:
1367  : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
1368  {
1369  }
1370 
1372  : binary_exprt(
1373  std::move(_lhs),
1374  ID_saturating_plus,
1375  std::move(_rhs),
1376  std::move(_type))
1377  {
1378  }
1379 };
1380 
1381 template <>
1383 {
1384  return base.id() == ID_saturating_plus;
1385 }
1386 
1387 inline void validate_expr(const saturating_plus_exprt &value)
1388 {
1389  validate_operands(value, 2, "saturating plus must have two operands");
1390 }
1391 
1399 {
1400  PRECONDITION(expr.id() == ID_saturating_plus);
1401  const saturating_plus_exprt &ret =
1402  static_cast<const saturating_plus_exprt &>(expr);
1403  validate_expr(ret);
1404  return ret;
1405 }
1406 
1409 {
1410  PRECONDITION(expr.id() == ID_saturating_plus);
1411  saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
1412  validate_expr(ret);
1413  return ret;
1414 }
1415 
1418 {
1419 public:
1421  : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
1422  {
1423  }
1424 };
1425 
1426 template <>
1428 {
1429  return base.id() == ID_saturating_minus;
1430 }
1431 
1432 inline void validate_expr(const saturating_minus_exprt &value)
1433 {
1434  validate_operands(value, 2, "saturating minus must have two operands");
1435 }
1436 
1444 {
1445  PRECONDITION(expr.id() == ID_saturating_minus);
1446  const saturating_minus_exprt &ret =
1447  static_cast<const saturating_minus_exprt &>(expr);
1448  validate_expr(ret);
1449  return ret;
1450 }
1451 
1454 {
1455  PRECONDITION(expr.id() == ID_saturating_minus);
1456  saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
1457  validate_expr(ret);
1458  return ret;
1459 }
1460 
1464 {
1465 public:
1466  overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
1467  : expr_protectedt(
1468  make_id(kind),
1469  struct_typet{
1470  {{ID_value, _lhs.type()},
1471  {"overflow-" + id2string(kind), bool_typet{}}}},
1472  {_lhs, std::move(_rhs)})
1473  {
1474  INVARIANT(
1475  valid_id(id()),
1476  "The kind used to construct overflow_result_exprt should be in the set "
1477  "of expected valid kinds.");
1478  }
1479 
1481  : expr_protectedt(
1482  make_id(kind),
1483  struct_typet{
1484  {{ID_value, _op.type()},
1485  {"overflow-" + id2string(kind), bool_typet{}}}},
1486  {_op})
1487  {
1488  INVARIANT(
1489  valid_id(id()),
1490  "The kind used to construct overflow_result_exprt should be in the set "
1491  "of expected valid kinds.");
1492  }
1493 
1494  // make op0 and op1 public
1495  using exprt::op0;
1496  using exprt::op1;
1497 
1498  const exprt &op2() const = delete;
1499  exprt &op2() = delete;
1500  const exprt &op3() const = delete;
1501  exprt &op3() = delete;
1502 
1503  static void check(
1504  const exprt &expr,
1506  {
1507  if(expr.id() != ID_overflow_result_unary_minus)
1508  binary_exprt::check(expr, vm);
1509 
1510  if(
1511  expr.id() != ID_overflow_result_unary_minus &&
1512  expr.id() != ID_overflow_result_shl)
1513  {
1514  const binary_exprt &binary_expr = to_binary_expr(expr);
1515  DATA_CHECK(
1516  vm,
1517  binary_expr.lhs().type() == binary_expr.rhs().type(),
1518  "operand types must match");
1519  }
1520  }
1521 
1522  static void validate(
1523  const exprt &expr,
1524  const namespacet &,
1526  {
1527  check(expr, vm);
1528  }
1529 
1531  static bool valid_id(const irep_idt &id)
1532  {
1533  return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
1534  id == ID_overflow_result_minus || id == ID_overflow_result_shl ||
1535  id == ID_overflow_result_unary_minus;
1536  }
1537 
1538 private:
1539  static irep_idt make_id(const irep_idt &kind)
1540  {
1541  return "overflow_result-" + id2string(kind);
1542  }
1543 };
1544 
1545 template <>
1547 {
1548  return overflow_result_exprt::valid_id(base.id());
1549 }
1550 
1551 inline void validate_expr(const overflow_result_exprt &value)
1552 {
1553  if(value.id() == ID_overflow_result_unary_minus)
1554  {
1556  value, 1, "unary overflow expression must have two operands");
1557  }
1558  else
1559  {
1561  value, 2, "binary overflow expression must have two operands");
1562  }
1563 }
1564 
1572 {
1574  const overflow_result_exprt &ret =
1575  static_cast<const overflow_result_exprt &>(expr);
1576  validate_expr(ret);
1577  return ret;
1578 }
1579 
1582 {
1584  overflow_result_exprt &ret = static_cast<overflow_result_exprt &>(expr);
1585  validate_expr(ret);
1586  return ret;
1587 }
1588 
1592 {
1593 public:
1595  : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
1596  {
1597  }
1598 
1599  explicit find_first_set_exprt(const exprt &_op)
1600  : find_first_set_exprt(_op, _op.type())
1601  {
1602  }
1603 
1604  static void check(
1605  const exprt &expr,
1607  {
1608  DATA_CHECK(
1609  vm,
1610  expr.operands().size() == 1,
1611  "unary expression must have a single operand");
1612  DATA_CHECK(
1613  vm,
1615  "operand must be of bitvector type");
1616  }
1617 
1618  static void validate(
1619  const exprt &expr,
1620  const namespacet &,
1622  {
1623  check(expr, vm);
1624  }
1625 
1628  exprt lower() const;
1629 };
1630 
1631 template <>
1633 {
1634  return base.id() == ID_find_first_set;
1635 }
1636 
1637 inline void validate_expr(const find_first_set_exprt &value)
1638 {
1639  validate_operands(value, 1, "find_first_set must have one operand");
1640 }
1641 
1649 {
1650  PRECONDITION(expr.id() == ID_find_first_set);
1651  const find_first_set_exprt &ret =
1652  static_cast<const find_first_set_exprt &>(expr);
1653  validate_expr(ret);
1654  return ret;
1655 }
1656 
1659 {
1660  PRECONDITION(expr.id() == ID_find_first_set);
1661  find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
1662  validate_expr(ret);
1663  return ret;
1664 }
1665 
1666 #endif // CPROVER_UTIL_BITVECTOR_EXPR_H
const update_bit_exprt & to_update_bit_expr(const exprt &expr)
Cast an exprt to an update_bit_exprt.
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
bool can_cast_expr< mult_overflow_exprt >(const exprt &base)
bool can_cast_expr< replication_exprt >(const exprt &base)
bool can_cast_expr< bswap_exprt >(const exprt &base)
bool can_cast_expr< find_first_set_exprt >(const exprt &base)
bool can_cast_expr< saturating_plus_exprt >(const exprt &base)
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
bool can_cast_expr< update_bits_exprt >(const exprt &base)
bool can_cast_expr< saturating_minus_exprt >(const exprt &base)
const overflow_result_exprt & to_overflow_result_expr(const exprt &expr)
Cast an exprt to a overflow_result_exprt.
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
bool can_cast_expr< update_bit_exprt >(const exprt &base)
bool can_cast_expr< minus_overflow_exprt >(const exprt &base)
void validate_expr(const bswap_exprt &value)
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< ashr_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
bool can_cast_expr< shl_overflow_exprt >(const exprt &base)
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
bool can_cast_expr< overflow_result_exprt >(const exprt &base)
bool can_cast_expr< concatenation_exprt >(const exprt &base)
const find_first_set_exprt & to_find_first_set_expr(const exprt &expr)
Cast an exprt to a find_first_set_exprt.
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
bool can_cast_expr< lshr_exprt >(const exprt &base)
bool can_cast_expr< shl_exprt >(const exprt &base)
bool can_cast_expr< plus_overflow_exprt >(const exprt &base)
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
bool can_cast_expr< unary_minus_overflow_exprt >(const exprt &base)
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
const update_bits_exprt & to_update_bits_expr(const exprt &expr)
Cast an exprt to an update_bits_exprt.
Arithmetic right shift.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:650
exprt & lhs()
Definition: std_expr.h:668
exprt & op0()
Definition: expr.h:133
exprt & rhs()
Definition: std_expr.h:678
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of a binary_overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
Bit-wise AND.
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitnot_exprt(exprt op)
Bit-wise OR.
bitor_exprt(const exprt &_op0, exprt _op1)
Reverse the order of bits in a bit-vector.
bitreverse_exprt(exprt op)
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
Bit-wise XOR.
bitxor_exprt(exprt _op0, exprt _op1)
The Boolean type.
Definition: std_types.h:36
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
Definition: std_expr.h:2990
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
count_leading_zeros_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
count_trailing_zeros_exprt(const exprt &_op)
count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:344
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
exprt & op1()
Definition: expr.h:136
typet & type()
Return the type of the expression.
Definition: expr.h:84
exprt & op0()
Definition: expr.h:133
operandst & operands()
Definition: expr.h:94
Extracts a single bit of a bit-vector operand.
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
const exprt & src() const
const exprt & index() const
Extracts a sub-range of a bit-vector operand.
const exprt & index() const
extractbits_exprt(exprt _src, exprt _index, typet _type)
Extract the bits [_index .
const exprt & src() const
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
find_first_set_exprt(exprt _op, typet _type)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
exprt lower() const
Lower a find_first_set_exprt to arithmetic and logic expressions.
find_first_set_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
std::size_t get_size_t(const irep_idt &name) const
Definition: irep.cpp:67
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition: irep.cpp:82
const irep_idt & id() const
Definition: irep.h:388
Logical right shift.
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
minus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a minus_overflow_exprt to arithmetic and logic expressions.
mult_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a mult_overflow_exprt to arithmetic and logic expressions.
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:912
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
An expression returning both the result of the arithmetic operation under wrap-around semantics as we...
exprt & op2()=delete
const exprt & op3() const =delete
overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
exprt & op3()=delete
overflow_result_exprt(exprt _op, const irep_idt &kind)
const exprt & op2() const =delete
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static bool valid_id(const irep_idt &id)
Returns true iff id is a valid identifier of an overflow_exprt.
static irep_idt make_id(const irep_idt &kind)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
plus_overflow_exprt(exprt _lhs, exprt _rhs)
exprt lower() const
Lower a plus_overflow_exprt to arithmetic and logic expressions.
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
popcount_exprt(exprt _op, typet _type)
popcount_exprt(const exprt &_op)
Bit-vector replication.
const exprt & op() const
const constant_exprt & times() const
constant_exprt & times()
replication_exprt(constant_exprt _times, exprt _src, typet _type)
Saturating subtraction expression.
saturating_minus_exprt(exprt _lhs, exprt _rhs)
The saturating plus expression.
saturating_plus_exprt(exprt _lhs, exprt _rhs, typet _type)
saturating_plus_exprt(exprt _lhs, exprt _rhs)
A base class for shift and rotate operators.
exprt & distance()
exprt & op()
const exprt & distance() const
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const exprt & op() const
Left shift.
shl_exprt(exprt _src, const std::size_t _distance)
shl_exprt(exprt _src, exprt _distance)
shl_overflow_exprt(exprt _lhs, exprt _rhs)
Structure type, corresponds to C style structs.
Definition: std_types.h:231
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:373
const exprt & op() const
Definition: std_expr.h:391
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
unary_overflow_exprt(const irep_idt &kind, exprt _op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
Replaces a sub-range of a bit-vector operand.
const exprt & new_value() const
update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
Replaces the bit [_index] from _src to produce a result of the same type as _src.
const exprt & src() const
exprt lower() const
A lowering to masking, shifting, or.
const exprt & index() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value)
Replaces a sub-range of a bit-vector operand.
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
const exprt & src() const
const exprt & index() const
update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
Replace the bits [_index .
exprt lower() const
A lowering to masking, shifting, or.
update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value)
const exprt & new_value() const
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
Definition: std_types.h:952
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet