cprover
std_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_EXPR_H
11 #define CPROVER_UTIL_STD_EXPR_H
12 
15 
16 #include "as_const.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "narrow.h"
20 #include "std_types.h"
21 
24 {
25 public:
26  nullary_exprt(const irep_idt &_id, typet _type)
27  : expr_protectedt(_id, std::move(_type))
28  {
29  }
30 
32  operandst &operands() = delete;
33  const operandst &operands() const = delete;
34 
35  const exprt &op0() const = delete;
36  exprt &op0() = delete;
37  const exprt &op1() const = delete;
38  exprt &op1() = delete;
39  const exprt &op2() const = delete;
40  exprt &op2() = delete;
41  const exprt &op3() const = delete;
42  exprt &op3() = delete;
43 
44  void move_to_operands(exprt &) = delete;
45  void move_to_operands(exprt &, exprt &) = delete;
46  void move_to_operands(exprt &, exprt &, exprt &) = delete;
47 
48  void copy_to_operands(const exprt &expr) = delete;
49  void copy_to_operands(const exprt &, const exprt &) = delete;
50  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
51 };
52 
55 {
56 public:
57  // constructor
59  const irep_idt &_id,
60  exprt _op0,
61  exprt _op1,
62  exprt _op2,
63  typet _type)
65  _id,
66  std::move(_type),
67  {std::move(_op0), std::move(_op1), std::move(_op2)})
68  {
69  }
70 
71  // make op0 to op2 public
72  using exprt::op0;
73  using exprt::op1;
74  using exprt::op2;
75 
76  const exprt &op3() const = delete;
77  exprt &op3() = delete;
78 };
79 
82 {
83 public:
85  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
86  {
87  }
88 
91  symbol_exprt(const irep_idt &identifier, typet type)
92  : nullary_exprt(ID_symbol, std::move(type))
93  {
94  set_identifier(identifier);
95  }
96 
101  static symbol_exprt typeless(const irep_idt &id)
102  {
103  return symbol_exprt(id, typet());
104  }
105 
106  void set_identifier(const irep_idt &identifier)
107  {
108  set(ID_identifier, identifier);
109  }
110 
111  const irep_idt &get_identifier() const
112  {
113  return get(ID_identifier);
114  }
115 };
116 
120 {
121 public:
125  : symbol_exprt(identifier, std::move(type))
126  {
127  }
128 
129  bool is_static_lifetime() const
130  {
131  return get_bool(ID_C_static_lifetime);
132  }
133 
135  {
136  return set(ID_C_static_lifetime, true);
137  }
138 
140  {
141  remove(ID_C_static_lifetime);
142  }
143 
144  bool is_thread_local() const
145  {
146  return get_bool(ID_C_thread_local);
147  }
148 
150  {
151  return set(ID_C_thread_local, true);
152  }
153 
155  {
156  remove(ID_C_thread_local);
157  }
158 };
159 
160 template <>
161 inline bool can_cast_expr<symbol_exprt>(const exprt &base)
162 {
163  return base.id() == ID_symbol;
164 }
165 
166 inline void validate_expr(const symbol_exprt &value)
167 {
168  validate_operands(value, 0, "Symbols must not have operands");
169 }
170 
177 inline const symbol_exprt &to_symbol_expr(const exprt &expr)
178 {
179  PRECONDITION(expr.id()==ID_symbol);
180  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
181  validate_expr(ret);
182  return ret;
183 }
184 
187 {
188  PRECONDITION(expr.id()==ID_symbol);
189  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
190  validate_expr(ret);
191  return ret;
192 }
193 
194 
197 {
198 public:
202  : nullary_exprt(ID_nondet_symbol, std::move(type))
203  {
204  set_identifier(identifier);
205  }
206 
211  irep_idt identifier,
212  typet type,
213  source_locationt location)
214  : nullary_exprt(ID_nondet_symbol, std::move(type))
215  {
216  set_identifier(std::move(identifier));
217  add_source_location() = std::move(location);
218  }
219 
220  void set_identifier(const irep_idt &identifier)
221  {
222  set(ID_identifier, identifier);
223  }
224 
225  const irep_idt &get_identifier() const
226  {
227  return get(ID_identifier);
228  }
229 };
230 
231 template <>
233 {
234  return base.id() == ID_nondet_symbol;
235 }
236 
237 inline void validate_expr(const nondet_symbol_exprt &value)
238 {
239  validate_operands(value, 0, "Symbols must not have operands");
240 }
241 
249 {
250  PRECONDITION(expr.id()==ID_nondet_symbol);
251  const nondet_symbol_exprt &ret =
252  static_cast<const nondet_symbol_exprt &>(expr);
253  validate_expr(ret);
254  return ret;
255 }
256 
259 {
260  PRECONDITION(expr.id()==ID_symbol);
261  nondet_symbol_exprt &ret = static_cast<nondet_symbol_exprt &>(expr);
262  validate_expr(ret);
263  return ret;
264 }
265 
266 
269 {
270 public:
271  unary_exprt(const irep_idt &_id, const exprt &_op)
272  : expr_protectedt(_id, _op.type(), {_op})
273  {
274  }
275 
276  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
277  : expr_protectedt(_id, std::move(_type), {std::move(_op)})
278  {
279  }
280 
281  const exprt &op() const
282  {
283  return op0();
284  }
285 
287  {
288  return op0();
289  }
290 
291  const exprt &op1() const = delete;
292  exprt &op1() = delete;
293  const exprt &op2() const = delete;
294  exprt &op2() = delete;
295  const exprt &op3() const = delete;
296  exprt &op3() = delete;
297 };
298 
299 template <>
300 inline bool can_cast_expr<unary_exprt>(const exprt &base)
301 {
302  return base.operands().size() == 1;
303 }
304 
305 inline void validate_expr(const unary_exprt &value)
306 {
307  validate_operands(value, 1, "Unary expressions must have one operand");
308 }
309 
316 inline const unary_exprt &to_unary_expr(const exprt &expr)
317 {
318  const unary_exprt &ret = static_cast<const unary_exprt &>(expr);
319  validate_expr(ret);
320  return ret;
321 }
322 
325 {
326  unary_exprt &ret = static_cast<unary_exprt &>(expr);
327  validate_expr(ret);
328  return ret;
329 }
330 
331 
333 class abs_exprt:public unary_exprt
334 {
335 public:
336  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
337  {
338  }
339 };
340 
341 template <>
342 inline bool can_cast_expr<abs_exprt>(const exprt &base)
343 {
344  return base.id() == ID_abs;
345 }
346 
347 inline void validate_expr(const abs_exprt &value)
348 {
349  validate_operands(value, 1, "Absolute value must have one operand");
350 }
351 
358 inline const abs_exprt &to_abs_expr(const exprt &expr)
359 {
360  PRECONDITION(expr.id()==ID_abs);
361  const abs_exprt &ret = static_cast<const abs_exprt &>(expr);
362  validate_expr(ret);
363  return ret;
364 }
365 
368 {
369  PRECONDITION(expr.id()==ID_abs);
370  abs_exprt &ret = static_cast<abs_exprt &>(expr);
371  validate_expr(ret);
372  return ret;
373 }
374 
375 
378 {
379 public:
381  : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
382  {
383  }
384 
385  explicit unary_minus_exprt(exprt _op)
386  : unary_exprt(ID_unary_minus, std::move(_op))
387  {
388  }
389 };
390 
391 template <>
392 inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
393 {
394  return base.id() == ID_unary_minus;
395 }
396 
397 inline void validate_expr(const unary_minus_exprt &value)
398 {
399  validate_operands(value, 1, "Unary minus must have one operand");
400 }
401 
408 inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
409 {
410  PRECONDITION(expr.id()==ID_unary_minus);
411  const unary_minus_exprt &ret = static_cast<const unary_minus_exprt &>(expr);
412  validate_expr(ret);
413  return ret;
414 }
415 
418 {
419  PRECONDITION(expr.id()==ID_unary_minus);
420  unary_minus_exprt &ret = static_cast<unary_minus_exprt &>(expr);
421  validate_expr(ret);
422  return ret;
423 }
424 
427 {
428 public:
430  : unary_exprt(ID_unary_plus, std::move(op))
431  {
432  }
433 };
434 
435 template <>
436 inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
437 {
438  return base.id() == ID_unary_plus;
439 }
440 
441 inline void validate_expr(const unary_plus_exprt &value)
442 {
443  validate_operands(value, 1, "unary plus must have one operand");
444 }
445 
452 inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
453 {
454  PRECONDITION(expr.id() == ID_unary_plus);
455  const unary_plus_exprt &ret = static_cast<const unary_plus_exprt &>(expr);
456  validate_expr(ret);
457  return ret;
458 }
459 
462 {
463  PRECONDITION(expr.id() == ID_unary_plus);
464  unary_plus_exprt &ret = static_cast<unary_plus_exprt &>(expr);
465  validate_expr(ret);
466  return ret;
467 }
468 
471 {
472 public:
473  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
474  : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
475  {
476  set_bits_per_byte(bits_per_byte);
477  }
478 
479  bswap_exprt(exprt _op, std::size_t bits_per_byte)
480  : unary_exprt(ID_bswap, std::move(_op))
481  {
482  set_bits_per_byte(bits_per_byte);
483  }
484 
485  std::size_t get_bits_per_byte() const
486  {
487  return get_size_t(ID_bits_per_byte);
488  }
489 
490  void set_bits_per_byte(std::size_t bits_per_byte)
491  {
492  set(ID_bits_per_byte, narrow_cast<long long>(bits_per_byte));
493  }
494 };
495 
496 template <>
497 inline bool can_cast_expr<bswap_exprt>(const exprt &base)
498 {
499  return base.id() == ID_bswap;
500 }
501 
502 inline void validate_expr(const bswap_exprt &value)
503 {
504  validate_operands(value, 1, "bswap must have one operand");
506  value.op().type() == value.type(), "bswap type must match operand type");
507 }
508 
515 inline const bswap_exprt &to_bswap_expr(const exprt &expr)
516 {
517  PRECONDITION(expr.id() == ID_bswap);
518  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
519  validate_expr(ret);
520  return ret;
521 }
522 
525 {
526  PRECONDITION(expr.id() == ID_bswap);
527  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
528  validate_expr(ret);
529  return ret;
530 }
531 
535 {
536 public:
537  explicit predicate_exprt(const irep_idt &_id)
538  : expr_protectedt(_id, bool_typet())
539  {
540  }
541 };
542 
546 {
547 public:
549  : unary_exprt(_id, std::move(_op), bool_typet())
550  {
551  }
552 };
553 
557 {
558 public:
559  explicit sign_exprt(exprt _op)
560  : unary_predicate_exprt(ID_sign, std::move(_op))
561  {
562  }
563 };
564 
565 template <>
566 inline bool can_cast_expr<sign_exprt>(const exprt &base)
567 {
568  return base.id() == ID_sign;
569 }
570 
571 inline void validate_expr(const sign_exprt &expr)
572 {
573  validate_operands(expr, 1, "sign expression must have one operand");
574 }
575 
582 inline const sign_exprt &to_sign_expr(const exprt &expr)
583 {
584  PRECONDITION(expr.id() == ID_sign);
585  const sign_exprt &ret = static_cast<const sign_exprt &>(expr);
586  validate_expr(ret);
587  return ret;
588 }
589 
592 {
593  PRECONDITION(expr.id() == ID_sign);
594  sign_exprt &ret = static_cast<sign_exprt &>(expr);
595  validate_expr(ret);
596  return ret;
597 }
598 
601 {
602 public:
603  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
604  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
605  {
606  }
607 
608  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
609  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
610  {
611  }
612 
613  static void check(
614  const exprt &expr,
616  {
617  DATA_CHECK(
618  vm,
619  expr.operands().size() == 2,
620  "binary expression must have two operands");
621  }
622 
623  static void validate(
624  const exprt &expr,
625  const namespacet &,
627  {
628  check(expr, vm);
629  }
630 
632  {
633  return exprt::op0();
634  }
635 
636  const exprt &lhs() const
637  {
638  return exprt::op0();
639  }
640 
642  {
643  return exprt::op1();
644  }
645 
646  const exprt &rhs() const
647  {
648  return exprt::op1();
649  }
650 
651  // make op0 and op1 public
652  using exprt::op0;
653  using exprt::op1;
654 
655  const exprt &op2() const = delete;
656  exprt &op2() = delete;
657  const exprt &op3() const = delete;
658  exprt &op3() = delete;
659 };
660 
661 template <>
662 inline bool can_cast_expr<binary_exprt>(const exprt &base)
663 {
664  return base.operands().size() == 2;
665 }
666 
667 inline void validate_expr(const binary_exprt &value)
668 {
669  binary_exprt::check(value);
670 }
671 
678 inline const binary_exprt &to_binary_expr(const exprt &expr)
679 {
680  binary_exprt::check(expr);
681  return static_cast<const binary_exprt &>(expr);
682 }
683 
686 {
687  binary_exprt::check(expr);
688  return static_cast<binary_exprt &>(expr);
689 }
690 
694 {
695 public:
696  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
697  : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
698  {
699  }
700 
701  static void check(
702  const exprt &expr,
704  {
705  binary_exprt::check(expr, vm);
706  }
707 
708  static void validate(
709  const exprt &expr,
710  const namespacet &ns,
712  {
713  binary_exprt::validate(expr, ns, vm);
714 
715  DATA_CHECK(
716  vm,
717  expr.type().id() == ID_bool,
718  "result of binary predicate expression should be of type bool");
719  }
720 };
721 
725 {
726 public:
727  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
728  : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
729  {
730  }
731 
732  static void check(
733  const exprt &expr,
735  {
737  }
738 
739  static void validate(
740  const exprt &expr,
741  const namespacet &ns,
743  {
744  binary_predicate_exprt::validate(expr, ns, vm);
745 
746  // we now can safely assume that 'expr' is a binary predicate
747  const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
748 
749  // check that the types of the operands are the same
750  DATA_CHECK(
751  vm,
752  expr_binary.op0().type() == expr_binary.op1().type(),
753  "lhs and rhs of binary relation expression should have same type");
754  }
755 };
756 
757 template <>
759 {
760  return can_cast_expr<binary_exprt>(base);
761 }
762 
763 inline void validate_expr(const binary_relation_exprt &value)
764 {
766 }
767 
775 {
777  return static_cast<const binary_relation_exprt &>(expr);
778 }
779 
782 {
784  return static_cast<binary_relation_exprt &>(expr);
785 }
786 
787 
791 {
792 public:
793  DEPRECATED(SINCE(2018, 12, 7, "use multi_ary_exprt(id, op, type) instead"))
794  multi_ary_exprt(const irep_idt &_id, const typet &_type)
795  : expr_protectedt(_id, _type)
796  {
797  }
798 
799  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
800  : expr_protectedt(_id, std::move(_type))
801  {
802  operands() = std::move(_operands);
803  }
804 
805  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
806  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
807  {
808  }
809 
810  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
811  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
812  {
813  }
814 
815  // In contrast to exprt::opX, the methods
816  // below check the size.
818  {
819  PRECONDITION(operands().size() >= 1);
820  return operands().front();
821  }
822 
824  {
825  PRECONDITION(operands().size() >= 2);
826  return operands()[1];
827  }
828 
830  {
831  PRECONDITION(operands().size() >= 3);
832  return operands()[2];
833  }
834 
836  {
837  PRECONDITION(operands().size() >= 4);
838  return operands()[3];
839  }
840 
841  const exprt &op0() const
842  {
843  PRECONDITION(operands().size() >= 1);
844  return operands().front();
845  }
846 
847  const exprt &op1() const
848  {
849  PRECONDITION(operands().size() >= 2);
850  return operands()[1];
851  }
852 
853  const exprt &op2() const
854  {
855  PRECONDITION(operands().size() >= 3);
856  return operands()[2];
857  }
858 
859  const exprt &op3() const
860  {
861  PRECONDITION(operands().size() >= 4);
862  return operands()[3];
863  }
864 };
865 
872 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
873 {
874  return static_cast<const multi_ary_exprt &>(expr);
875 }
876 
879 {
880  return static_cast<multi_ary_exprt &>(expr);
881 }
882 
883 
887 {
888 public:
889  plus_exprt(exprt _lhs, exprt _rhs)
890  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
891  {
892  }
893 
894  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
895  : multi_ary_exprt(
896  std::move(_lhs),
897  ID_plus,
898  std::move(_rhs),
899  std::move(_type))
900  {
901  }
902 
903  plus_exprt(operandst _operands, typet _type)
904  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
905  {
906  }
907 };
908 
909 template <>
910 inline bool can_cast_expr<plus_exprt>(const exprt &base)
911 {
912  return base.id() == ID_plus;
913 }
914 
915 inline void validate_expr(const plus_exprt &value)
916 {
917  validate_operands(value, 2, "Plus must have two or more operands", true);
918 }
919 
926 inline const plus_exprt &to_plus_expr(const exprt &expr)
927 {
928  PRECONDITION(expr.id()==ID_plus);
929  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
930  validate_expr(ret);
931  return ret;
932 }
933 
936 {
937  PRECONDITION(expr.id()==ID_plus);
938  plus_exprt &ret = static_cast<plus_exprt &>(expr);
939  validate_expr(ret);
940  return ret;
941 }
942 
943 
946 {
947 public:
948  minus_exprt(exprt _lhs, exprt _rhs)
949  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
950  {
951  }
952 };
953 
954 template <>
955 inline bool can_cast_expr<minus_exprt>(const exprt &base)
956 {
957  return base.id() == ID_minus;
958 }
959 
960 inline void validate_expr(const minus_exprt &value)
961 {
962  validate_operands(value, 2, "Minus must have two or more operands", true);
963 }
964 
971 inline const minus_exprt &to_minus_expr(const exprt &expr)
972 {
973  PRECONDITION(expr.id()==ID_minus);
974  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
975  validate_expr(ret);
976  return ret;
977 }
978 
981 {
982  PRECONDITION(expr.id()==ID_minus);
983  minus_exprt &ret = static_cast<minus_exprt &>(expr);
984  validate_expr(ret);
985  return ret;
986 }
987 
988 
992 {
993 public:
994  mult_exprt(exprt _lhs, exprt _rhs)
995  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
996  {
997  }
998 };
999 
1000 template <>
1001 inline bool can_cast_expr<mult_exprt>(const exprt &base)
1002 {
1003  return base.id() == ID_mult;
1004 }
1005 
1006 inline void validate_expr(const mult_exprt &value)
1007 {
1008  validate_operands(value, 2, "Multiply must have two or more operands", true);
1009 }
1010 
1017 inline const mult_exprt &to_mult_expr(const exprt &expr)
1018 {
1019  PRECONDITION(expr.id()==ID_mult);
1020  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1021  validate_expr(ret);
1022  return ret;
1023 }
1024 
1027 {
1028  PRECONDITION(expr.id()==ID_mult);
1029  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1030  validate_expr(ret);
1031  return ret;
1032 }
1033 
1034 
1037 {
1038 public:
1039  div_exprt(exprt _lhs, exprt _rhs)
1040  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1041  {
1042  }
1043 
1046  {
1047  return op0();
1048  }
1049 
1051  const exprt &dividend() const
1052  {
1053  return op0();
1054  }
1055 
1058  {
1059  return op1();
1060  }
1061 
1063  const exprt &divisor() const
1064  {
1065  return op1();
1066  }
1067 };
1068 
1069 template <>
1070 inline bool can_cast_expr<div_exprt>(const exprt &base)
1071 {
1072  return base.id() == ID_div;
1073 }
1074 
1075 inline void validate_expr(const div_exprt &value)
1076 {
1077  validate_operands(value, 2, "Divide must have two operands");
1078 }
1079 
1086 inline const div_exprt &to_div_expr(const exprt &expr)
1087 {
1088  PRECONDITION(expr.id()==ID_div);
1089  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1090  validate_expr(ret);
1091  return ret;
1092 }
1093 
1096 {
1097  PRECONDITION(expr.id()==ID_div);
1098  div_exprt &ret = static_cast<div_exprt &>(expr);
1099  validate_expr(ret);
1100  return ret;
1101 }
1102 
1103 
1106 {
1107 public:
1108  mod_exprt(exprt _lhs, exprt _rhs)
1109  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1110  {
1111  }
1112 };
1113 
1114 template <>
1115 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1116 {
1117  return base.id() == ID_mod;
1118 }
1119 
1120 inline void validate_expr(const mod_exprt &value)
1121 {
1122  validate_operands(value, 2, "Modulo must have two operands");
1123 }
1124 
1131 inline const mod_exprt &to_mod_expr(const exprt &expr)
1132 {
1133  PRECONDITION(expr.id()==ID_mod);
1134  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1135  validate_expr(ret);
1136  return ret;
1137 }
1138 
1141 {
1142  PRECONDITION(expr.id()==ID_mod);
1143  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1144  validate_expr(ret);
1145  return ret;
1146 }
1147 
1148 
1151 {
1152 public:
1153  rem_exprt(exprt _lhs, exprt _rhs)
1154  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1155  {
1156  }
1157 };
1158 
1159 template <>
1160 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1161 {
1162  return base.id() == ID_rem;
1163 }
1164 
1165 inline void validate_expr(const rem_exprt &value)
1166 {
1167  validate_operands(value, 2, "Remainder must have two operands");
1168 }
1169 
1176 inline const rem_exprt &to_rem_expr(const exprt &expr)
1177 {
1178  PRECONDITION(expr.id()==ID_rem);
1179  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1180  validate_expr(ret);
1181  return ret;
1182 }
1183 
1186 {
1187  PRECONDITION(expr.id()==ID_rem);
1188  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1189  validate_expr(ret);
1190  return ret;
1191 }
1192 
1193 
1196 {
1197 public:
1199  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1200  {
1201  }
1202 
1203  static void check(
1204  const exprt &expr,
1206  {
1207  binary_relation_exprt::check(expr, vm);
1208  }
1209 
1210  static void validate(
1211  const exprt &expr,
1212  const namespacet &ns,
1214  {
1215  binary_relation_exprt::validate(expr, ns, vm);
1216  }
1217 };
1218 
1219 template <>
1220 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1221 {
1222  return base.id() == ID_equal;
1223 }
1224 
1225 inline void validate_expr(const equal_exprt &value)
1226 {
1227  equal_exprt::check(value);
1228 }
1229 
1236 inline const equal_exprt &to_equal_expr(const exprt &expr)
1237 {
1238  PRECONDITION(expr.id()==ID_equal);
1239  equal_exprt::check(expr);
1240  return static_cast<const equal_exprt &>(expr);
1241 }
1242 
1245 {
1246  PRECONDITION(expr.id()==ID_equal);
1247  equal_exprt::check(expr);
1248  return static_cast<equal_exprt &>(expr);
1249 }
1250 
1251 
1254 {
1255 public:
1257  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1258  {
1259  }
1260 };
1261 
1262 template <>
1263 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1264 {
1265  return base.id() == ID_notequal;
1266 }
1267 
1268 inline void validate_expr(const notequal_exprt &value)
1269 {
1270  validate_operands(value, 2, "Inequality must have two operands");
1271 }
1272 
1279 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1280 {
1281  PRECONDITION(expr.id()==ID_notequal);
1282  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1283  validate_expr(ret);
1284  return ret;
1285 }
1286 
1289 {
1290  PRECONDITION(expr.id()==ID_notequal);
1291  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1292  validate_expr(ret);
1293  return ret;
1294 }
1295 
1296 
1299 {
1300 public:
1301  index_exprt(const exprt &_array, exprt _index)
1302  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1303  {
1304  }
1305 
1306  index_exprt(exprt _array, exprt _index, typet _type)
1307  : binary_exprt(
1308  std::move(_array),
1309  ID_index,
1310  std::move(_index),
1311  std::move(_type))
1312  {
1313  }
1314 
1316  {
1317  return op0();
1318  }
1319 
1320  const exprt &array() const
1321  {
1322  return op0();
1323  }
1324 
1326  {
1327  return op1();
1328  }
1329 
1330  const exprt &index() const
1331  {
1332  return op1();
1333  }
1334 };
1335 
1336 template <>
1337 inline bool can_cast_expr<index_exprt>(const exprt &base)
1338 {
1339  return base.id() == ID_index;
1340 }
1341 
1342 inline void validate_expr(const index_exprt &value)
1343 {
1344  validate_operands(value, 2, "Array index must have two operands");
1345 }
1346 
1353 inline const index_exprt &to_index_expr(const exprt &expr)
1354 {
1355  PRECONDITION(expr.id()==ID_index);
1356  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1357  validate_expr(ret);
1358  return ret;
1359 }
1360 
1363 {
1364  PRECONDITION(expr.id()==ID_index);
1365  index_exprt &ret = static_cast<index_exprt &>(expr);
1366  validate_expr(ret);
1367  return ret;
1368 }
1369 
1370 
1373 {
1374 public:
1375  explicit array_of_exprt(exprt _what, array_typet _type)
1376  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1377  {
1378  }
1379 
1380  const array_typet &type() const
1381  {
1382  return static_cast<const array_typet &>(unary_exprt::type());
1383  }
1384 
1386  {
1387  return static_cast<array_typet &>(unary_exprt::type());
1388  }
1389 
1391  {
1392  return op0();
1393  }
1394 
1395  const exprt &what() const
1396  {
1397  return op0();
1398  }
1399 };
1400 
1401 template <>
1402 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1403 {
1404  return base.id() == ID_array_of;
1405 }
1406 
1407 inline void validate_expr(const array_of_exprt &value)
1408 {
1409  validate_operands(value, 1, "'Array of' must have one operand");
1410 }
1411 
1418 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1419 {
1420  PRECONDITION(expr.id()==ID_array_of);
1421  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1422  validate_expr(ret);
1423  return ret;
1424 }
1425 
1428 {
1429  PRECONDITION(expr.id()==ID_array_of);
1430  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1431  validate_expr(ret);
1432  return ret;
1433 }
1434 
1435 
1438 {
1439 public:
1440  DEPRECATED(SINCE(2019, 1, 12, "use array_exprt(operands, type) instead"))
1441  explicit array_exprt(const array_typet &_type)
1442  : multi_ary_exprt(ID_array, _type)
1443  {
1444  }
1445 
1447  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1448  {
1449  }
1450 
1451  const array_typet &type() const
1452  {
1453  return static_cast<const array_typet &>(multi_ary_exprt::type());
1454  }
1455 
1457  {
1458  return static_cast<array_typet &>(multi_ary_exprt::type());
1459  }
1460 };
1461 
1462 template <>
1463 inline bool can_cast_expr<array_exprt>(const exprt &base)
1464 {
1465  return base.id() == ID_array;
1466 }
1467 
1474 inline const array_exprt &to_array_expr(const exprt &expr)
1475 {
1476  PRECONDITION(expr.id()==ID_array);
1477  return static_cast<const array_exprt &>(expr);
1478 }
1479 
1482 {
1483  PRECONDITION(expr.id()==ID_array);
1484  return static_cast<array_exprt &>(expr);
1485 }
1486 
1490 {
1491 public:
1493  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1494  {
1495  }
1496 
1497  const array_typet &type() const
1498  {
1499  return static_cast<const array_typet &>(multi_ary_exprt::type());
1500  }
1501 
1503  {
1504  return static_cast<array_typet &>(multi_ary_exprt::type());
1505  }
1506 
1508  void add(exprt index, exprt value)
1509  {
1510  add_to_operands(std::move(index), std::move(value));
1511  }
1512 };
1513 
1514 template <>
1515 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1516 {
1517  return base.id() == ID_array_list;
1518 }
1519 
1520 inline void validate_expr(const array_list_exprt &value)
1521 {
1522  PRECONDITION(value.operands().size() % 2 == 0);
1523 }
1524 
1525 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1526 {
1528  auto &ret = static_cast<const array_list_exprt &>(expr);
1529  validate_expr(ret);
1530  return ret;
1531 }
1532 
1534 {
1536  auto &ret = static_cast<array_list_exprt &>(expr);
1537  validate_expr(ret);
1538  return ret;
1539 }
1540 
1543 {
1544 public:
1546  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1547  {
1548  }
1549 };
1550 
1551 template <>
1552 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1553 {
1554  return base.id() == ID_vector;
1555 }
1556 
1563 inline const vector_exprt &to_vector_expr(const exprt &expr)
1564 {
1565  PRECONDITION(expr.id()==ID_vector);
1566  return static_cast<const vector_exprt &>(expr);
1567 }
1568 
1571 {
1572  PRECONDITION(expr.id()==ID_vector);
1573  return static_cast<vector_exprt &>(expr);
1574 }
1575 
1576 
1579 {
1580 public:
1581  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1582  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1583  {
1584  set_component_name(_component_name);
1585  }
1586 
1588  {
1589  return get(ID_component_name);
1590  }
1591 
1592  void set_component_name(const irep_idt &component_name)
1593  {
1594  set(ID_component_name, component_name);
1595  }
1596 
1597  std::size_t get_component_number() const
1598  {
1599  return get_size_t(ID_component_number);
1600  }
1601 
1602  void set_component_number(std::size_t component_number)
1603  {
1604  set(ID_component_number, narrow_cast<long long>(component_number));
1605  }
1606 };
1607 
1608 template <>
1609 inline bool can_cast_expr<union_exprt>(const exprt &base)
1610 {
1611  return base.id() == ID_union;
1612 }
1613 
1614 inline void validate_expr(const union_exprt &value)
1615 {
1616  validate_operands(value, 1, "Union constructor must have one operand");
1617 }
1618 
1625 inline const union_exprt &to_union_expr(const exprt &expr)
1626 {
1627  PRECONDITION(expr.id()==ID_union);
1628  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1629  validate_expr(ret);
1630  return ret;
1631 }
1632 
1635 {
1636  PRECONDITION(expr.id()==ID_union);
1637  union_exprt &ret = static_cast<union_exprt &>(expr);
1638  validate_expr(ret);
1639  return ret;
1640 }
1641 
1642 
1645 {
1646 public:
1647  DEPRECATED(SINCE(2019, 1, 12, "use struct_exprt(operands, type) instead"))
1648  explicit struct_exprt(const typet &_type) : multi_ary_exprt(ID_struct, _type)
1649  {
1650  }
1651 
1652  struct_exprt(operandst _operands, typet _type)
1653  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1654  {
1655  }
1656 
1657  exprt &component(const irep_idt &name, const namespacet &ns);
1658  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1659 };
1660 
1661 template <>
1662 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1663 {
1664  return base.id() == ID_struct;
1665 }
1666 
1673 inline const struct_exprt &to_struct_expr(const exprt &expr)
1674 {
1675  PRECONDITION(expr.id()==ID_struct);
1676  return static_cast<const struct_exprt &>(expr);
1677 }
1678 
1681 {
1682  PRECONDITION(expr.id()==ID_struct);
1683  return static_cast<struct_exprt &>(expr);
1684 }
1685 
1686 
1689 {
1690 public:
1692  : binary_exprt(
1693  std::move(_real),
1694  ID_complex,
1695  std::move(_imag),
1696  std::move(_type))
1697  {
1698  }
1699 
1701  {
1702  return op0();
1703  }
1704 
1705  const exprt &real() const
1706  {
1707  return op0();
1708  }
1709 
1711  {
1712  return op1();
1713  }
1714 
1715  const exprt &imag() const
1716  {
1717  return op1();
1718  }
1719 };
1720 
1721 template <>
1722 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1723 {
1724  return base.id() == ID_complex;
1725 }
1726 
1727 inline void validate_expr(const complex_exprt &value)
1728 {
1729  validate_operands(value, 2, "Complex constructor must have two operands");
1730 }
1731 
1738 inline const complex_exprt &to_complex_expr(const exprt &expr)
1739 {
1740  PRECONDITION(expr.id()==ID_complex);
1741  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1742  validate_expr(ret);
1743  return ret;
1744 }
1745 
1748 {
1749  PRECONDITION(expr.id()==ID_complex);
1750  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1751  validate_expr(ret);
1752  return ret;
1753 }
1754 
1757 {
1758 public:
1759  explicit complex_real_exprt(const exprt &op)
1760  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1761  {
1762  }
1763 };
1764 
1765 template <>
1767 {
1768  return base.id() == ID_complex_real;
1769 }
1770 
1771 inline void validate_expr(const complex_real_exprt &expr)
1772 {
1774  expr, 1, "real part retrieval operation must have one operand");
1775 }
1776 
1784 {
1785  PRECONDITION(expr.id() == ID_complex_real);
1786  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1787  validate_expr(ret);
1788  return ret;
1789 }
1790 
1793 {
1794  PRECONDITION(expr.id() == ID_complex_real);
1795  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1796  validate_expr(ret);
1797  return ret;
1798 }
1799 
1802 {
1803 public:
1804  explicit complex_imag_exprt(const exprt &op)
1805  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1806  {
1807  }
1808 };
1809 
1810 template <>
1812 {
1813  return base.id() == ID_complex_imag;
1814 }
1815 
1816 inline void validate_expr(const complex_imag_exprt &expr)
1817 {
1819  expr, 1, "imaginary part retrieval operation must have one operand");
1820 }
1821 
1829 {
1830  PRECONDITION(expr.id() == ID_complex_imag);
1831  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1832  validate_expr(ret);
1833  return ret;
1834 }
1835 
1838 {
1839  PRECONDITION(expr.id() == ID_complex_imag);
1840  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1841  validate_expr(ret);
1842  return ret;
1843 }
1844 
1845 class namespacet;
1846 
1849 {
1850 public:
1852  : binary_exprt(
1853  exprt(ID_unknown),
1854  ID_object_descriptor,
1855  exprt(ID_unknown),
1856  typet())
1857  {
1858  }
1859 
1860  explicit object_descriptor_exprt(exprt _object)
1861  : binary_exprt(
1862  std::move(_object),
1863  ID_object_descriptor,
1864  exprt(ID_unknown),
1865  typet())
1866  {
1867  }
1868 
1873  void build(const exprt &expr, const namespacet &ns);
1874 
1876  {
1877  return op0();
1878  }
1879 
1880  const exprt &object() const
1881  {
1882  return op0();
1883  }
1884 
1885  const exprt &root_object() const;
1886 
1888  {
1889  return op1();
1890  }
1891 
1892  const exprt &offset() const
1893  {
1894  return op1();
1895  }
1896 };
1897 
1898 template <>
1900 {
1901  return base.id() == ID_object_descriptor;
1902 }
1903 
1904 inline void validate_expr(const object_descriptor_exprt &value)
1905 {
1906  validate_operands(value, 2, "Object descriptor must have two operands");
1907 }
1908 
1916  const exprt &expr)
1917 {
1918  PRECONDITION(expr.id()==ID_object_descriptor);
1919  const object_descriptor_exprt &ret =
1920  static_cast<const object_descriptor_exprt &>(expr);
1921  validate_expr(ret);
1922  return ret;
1923 }
1924 
1927 {
1928  PRECONDITION(expr.id()==ID_object_descriptor);
1929  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
1930  validate_expr(ret);
1931  return ret;
1932 }
1933 
1934 
1937 {
1938 public:
1939  DEPRECATED(SINCE(2019, 2, 11, "use dynamic_object_exprt(type) instead"))
1941  : binary_exprt(exprt(ID_unknown), ID_dynamic_object, exprt(ID_unknown))
1942  {
1943  }
1944 
1946  : binary_exprt(
1947  exprt(ID_unknown),
1948  ID_dynamic_object,
1949  exprt(ID_unknown),
1950  std::move(type))
1951  {
1952  }
1953 
1954  void set_instance(unsigned int instance);
1955 
1956  unsigned int get_instance() const;
1957 
1959  {
1960  return op1();
1961  }
1962 
1963  const exprt &valid() const
1964  {
1965  return op1();
1966  }
1967 };
1968 
1969 template <>
1971 {
1972  return base.id() == ID_dynamic_object;
1973 }
1974 
1975 inline void validate_expr(const dynamic_object_exprt &value)
1976 {
1977  validate_operands(value, 2, "Dynamic object must have two operands");
1978 }
1979 
1987  const exprt &expr)
1988 {
1989  PRECONDITION(expr.id()==ID_dynamic_object);
1990  const dynamic_object_exprt &ret =
1991  static_cast<const dynamic_object_exprt &>(expr);
1992  validate_expr(ret);
1993  return ret;
1994 }
1995 
1998 {
1999  PRECONDITION(expr.id()==ID_dynamic_object);
2000  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
2001  validate_expr(ret);
2002  return ret;
2003 }
2004 
2007 {
2008 public:
2009  DEPRECATED(SINCE(2019, 11, 8, "use is_dynamic_object(op) instead"))
2011  : unary_predicate_exprt(ID_is_dynamic_object, exprt())
2012  {
2013  }
2014 
2016  : unary_predicate_exprt(ID_is_dynamic_object, op)
2017  {
2018  }
2019 };
2020 
2021 inline const is_dynamic_object_exprt &
2023 {
2024  PRECONDITION(expr.id() == ID_is_dynamic_object);
2026  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2027  return static_cast<const is_dynamic_object_exprt &>(expr);
2028 }
2029 
2033 {
2034  PRECONDITION(expr.id() == ID_is_dynamic_object);
2036  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2037  return static_cast<is_dynamic_object_exprt &>(expr);
2038 }
2039 
2042 {
2043 public:
2045  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2046  {
2047  }
2048 
2049  // returns a typecast if the type doesn't already match
2050  static exprt conditional_cast(const exprt &expr, const typet &type)
2051  {
2052  if(expr.type() == type)
2053  return expr;
2054  else
2055  return typecast_exprt(expr, type);
2056  }
2057 };
2058 
2059 template <>
2060 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2061 {
2062  return base.id() == ID_typecast;
2063 }
2064 
2065 inline void validate_expr(const typecast_exprt &value)
2066 {
2067  validate_operands(value, 1, "Typecast must have one operand");
2068 }
2069 
2076 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2077 {
2078  PRECONDITION(expr.id()==ID_typecast);
2079  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2080  validate_expr(ret);
2081  return ret;
2082 }
2083 
2086 {
2087  PRECONDITION(expr.id()==ID_typecast);
2088  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2089  validate_expr(ret);
2090  return ret;
2091 }
2092 
2093 
2096 {
2097 public:
2099  : binary_exprt(
2100  std::move(op),
2101  ID_floatbv_typecast,
2102  std::move(rounding),
2103  std::move(_type))
2104  {
2105  }
2106 
2108  {
2109  return op0();
2110  }
2111 
2112  const exprt &op() const
2113  {
2114  return op0();
2115  }
2116 
2118  {
2119  return op1();
2120  }
2121 
2122  const exprt &rounding_mode() const
2123  {
2124  return op1();
2125  }
2126 };
2127 
2128 template <>
2130 {
2131  return base.id() == ID_floatbv_typecast;
2132 }
2133 
2134 inline void validate_expr(const floatbv_typecast_exprt &value)
2135 {
2136  validate_operands(value, 2, "Float typecast must have two operands");
2137 }
2138 
2146 {
2147  PRECONDITION(expr.id()==ID_floatbv_typecast);
2148  const floatbv_typecast_exprt &ret =
2149  static_cast<const floatbv_typecast_exprt &>(expr);
2150  validate_expr(ret);
2151  return ret;
2152 }
2153 
2156 {
2157  PRECONDITION(expr.id()==ID_floatbv_typecast);
2158  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
2159  validate_expr(ret);
2160  return ret;
2161 }
2162 
2163 
2166 {
2167 public:
2169  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2170  {
2171  }
2172 
2174  : multi_ary_exprt(
2175  ID_and,
2176  {std::move(op0), std::move(op1), std::move(op2)},
2177  bool_typet())
2178  {
2179  }
2180 
2182  : multi_ary_exprt(
2183  ID_and,
2184  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2185  bool_typet())
2186  {
2187  }
2188 
2189  explicit and_exprt(exprt::operandst _operands)
2190  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2191  {
2192  }
2193 };
2194 
2198 
2200 
2201 template <>
2202 inline bool can_cast_expr<and_exprt>(const exprt &base)
2203 {
2204  return base.id() == ID_and;
2205 }
2206 
2213 inline const and_exprt &to_and_expr(const exprt &expr)
2214 {
2215  PRECONDITION(expr.id()==ID_and);
2216  return static_cast<const and_exprt &>(expr);
2217 }
2218 
2221 {
2222  PRECONDITION(expr.id()==ID_and);
2223  return static_cast<and_exprt &>(expr);
2224 }
2225 
2226 
2229 {
2230 public:
2232  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2233  {
2234  }
2235 };
2236 
2237 template <>
2238 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2239 {
2240  return base.id() == ID_implies;
2241 }
2242 
2243 inline void validate_expr(const implies_exprt &value)
2244 {
2245  validate_operands(value, 2, "Implies must have two operands");
2246 }
2247 
2254 inline const implies_exprt &to_implies_expr(const exprt &expr)
2255 {
2256  PRECONDITION(expr.id()==ID_implies);
2257  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2258  validate_expr(ret);
2259  return ret;
2260 }
2261 
2264 {
2265  PRECONDITION(expr.id()==ID_implies);
2266  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2267  validate_expr(ret);
2268  return ret;
2269 }
2270 
2271 
2274 {
2275 public:
2277  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2278  {
2279  }
2280 
2282  : multi_ary_exprt(
2283  ID_or,
2284  {std::move(op0), std::move(op1), std::move(op2)},
2285  bool_typet())
2286  {
2287  }
2288 
2290  : multi_ary_exprt(
2291  ID_or,
2292  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2293  bool_typet())
2294  {
2295  }
2296 
2297  explicit or_exprt(exprt::operandst _operands)
2298  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2299  {
2300  }
2301 };
2302 
2306 
2308 
2309 template <>
2310 inline bool can_cast_expr<or_exprt>(const exprt &base)
2311 {
2312  return base.id() == ID_or;
2313 }
2314 
2321 inline const or_exprt &to_or_expr(const exprt &expr)
2322 {
2323  PRECONDITION(expr.id()==ID_or);
2324  return static_cast<const or_exprt &>(expr);
2325 }
2326 
2328 inline or_exprt &to_or_expr(exprt &expr)
2329 {
2330  PRECONDITION(expr.id()==ID_or);
2331  return static_cast<or_exprt &>(expr);
2332 }
2333 
2334 
2337 {
2338 public:
2339  xor_exprt(exprt _op0, exprt _op1)
2340  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2341  {
2342  }
2343 };
2344 
2345 template <>
2346 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2347 {
2348  return base.id() == ID_xor;
2349 }
2350 
2357 inline const xor_exprt &to_xor_expr(const exprt &expr)
2358 {
2359  PRECONDITION(expr.id()==ID_xor);
2360  return static_cast<const xor_exprt &>(expr);
2361 }
2362 
2365 {
2366  PRECONDITION(expr.id()==ID_xor);
2367  return static_cast<xor_exprt &>(expr);
2368 }
2369 
2370 
2373 {
2374 public:
2375  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
2376  {
2377  }
2378 };
2379 
2380 template <>
2381 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2382 {
2383  return base.id() == ID_bitnot;
2384 }
2385 
2386 inline void validate_expr(const bitnot_exprt &value)
2387 {
2388  validate_operands(value, 1, "Bit-wise not must have one operand");
2389 }
2390 
2397 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2398 {
2399  PRECONDITION(expr.id()==ID_bitnot);
2400  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
2401  validate_expr(ret);
2402  return ret;
2403 }
2404 
2407 {
2408  PRECONDITION(expr.id()==ID_bitnot);
2409  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
2410  validate_expr(ret);
2411  return ret;
2412 }
2413 
2414 
2417 {
2418 public:
2419  bitor_exprt(const exprt &_op0, exprt _op1)
2420  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
2421  {
2422  }
2423 };
2424 
2425 template <>
2426 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2427 {
2428  return base.id() == ID_bitor;
2429 }
2430 
2437 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2438 {
2439  PRECONDITION(expr.id()==ID_bitor);
2440  return static_cast<const bitor_exprt &>(expr);
2441 }
2442 
2445 {
2446  PRECONDITION(expr.id()==ID_bitor);
2447  return static_cast<bitor_exprt &>(expr);
2448 }
2449 
2450 
2453 {
2454 public:
2456  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
2457  {
2458  }
2459 };
2460 
2461 template <>
2462 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2463 {
2464  return base.id() == ID_bitxor;
2465 }
2466 
2473 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2474 {
2475  PRECONDITION(expr.id()==ID_bitxor);
2476  return static_cast<const bitxor_exprt &>(expr);
2477 }
2478 
2481 {
2482  PRECONDITION(expr.id()==ID_bitxor);
2483  return static_cast<bitxor_exprt &>(expr);
2484 }
2485 
2486 
2489 {
2490 public:
2491  bitand_exprt(const exprt &_op0, exprt _op1)
2492  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
2493  {
2494  }
2495 };
2496 
2497 template <>
2498 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2499 {
2500  return base.id() == ID_bitand;
2501 }
2502 
2509 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2510 {
2511  PRECONDITION(expr.id()==ID_bitand);
2512  return static_cast<const bitand_exprt &>(expr);
2513 }
2514 
2517 {
2518  PRECONDITION(expr.id()==ID_bitand);
2519  return static_cast<bitand_exprt &>(expr);
2520 }
2521 
2522 
2525 {
2526 public:
2527  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
2528  : binary_exprt(std::move(_src), _id, std::move(_distance))
2529  {
2530  }
2531 
2532  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
2533 
2535  {
2536  return op0();
2537  }
2538 
2539  const exprt &op() const
2540  {
2541  return op0();
2542  }
2543 
2545  {
2546  return op1();
2547  }
2548 
2549  const exprt &distance() const
2550  {
2551  return op1();
2552  }
2553 };
2554 
2555 template <>
2556 inline bool can_cast_expr<shift_exprt>(const exprt &base)
2557 {
2558  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
2559 }
2560 
2561 inline void validate_expr(const shift_exprt &value)
2562 {
2563  validate_operands(value, 2, "Shifts must have two operands");
2564 }
2565 
2572 inline const shift_exprt &to_shift_expr(const exprt &expr)
2573 {
2574  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
2575  validate_expr(ret);
2576  return ret;
2577 }
2578 
2581 {
2582  shift_exprt &ret = static_cast<shift_exprt &>(expr);
2583  validate_expr(ret);
2584  return ret;
2585 }
2586 
2587 
2590 {
2591 public:
2592  shl_exprt(exprt _src, exprt _distance)
2593  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2594  {
2595  }
2596 
2597  shl_exprt(exprt _src, const std::size_t _distance)
2598  : shift_exprt(std::move(_src), ID_shl, _distance)
2599  {
2600  }
2601 };
2602 
2609 inline const shl_exprt &to_shl_expr(const exprt &expr)
2610 {
2611  PRECONDITION(expr.id() == ID_shl);
2612  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
2613  validate_expr(ret);
2614  return ret;
2615 }
2616 
2619 {
2620  PRECONDITION(expr.id() == ID_shl);
2621  shl_exprt &ret = static_cast<shl_exprt &>(expr);
2622  validate_expr(ret);
2623  return ret;
2624 }
2625 
2628 {
2629 public:
2630  ashr_exprt(exprt _src, exprt _distance)
2631  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2632  {
2633  }
2634 
2635  ashr_exprt(exprt _src, const std::size_t _distance)
2636  : shift_exprt(std::move(_src), ID_ashr, _distance)
2637  {
2638  }
2639 };
2640 
2643 {
2644 public:
2645  lshr_exprt(exprt _src, exprt _distance)
2646  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2647  {
2648  }
2649 
2650  lshr_exprt(exprt _src, const std::size_t _distance)
2651  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2652  {
2653  }
2654 };
2655 
2658 {
2659 public:
2662  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
2663  {
2664  }
2665 
2666  extractbit_exprt(exprt _src, const std::size_t _index);
2667 
2669  {
2670  return op0();
2671  }
2672 
2674  {
2675  return op1();
2676  }
2677 
2678  const exprt &src() const
2679  {
2680  return op0();
2681  }
2682 
2683  const exprt &index() const
2684  {
2685  return op1();
2686  }
2687 };
2688 
2689 template <>
2690 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
2691 {
2692  return base.id() == ID_extractbit;
2693 }
2694 
2695 inline void validate_expr(const extractbit_exprt &value)
2696 {
2697  validate_operands(value, 2, "Extract bit must have two operands");
2698 }
2699 
2706 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
2707 {
2708  PRECONDITION(expr.id()==ID_extractbit);
2709  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
2710  validate_expr(ret);
2711  return ret;
2712 }
2713 
2716 {
2717  PRECONDITION(expr.id()==ID_extractbit);
2718  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
2719  validate_expr(ret);
2720  return ret;
2721 }
2722 
2723 
2726 {
2727 public:
2733  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
2734  : expr_protectedt(
2735  ID_extractbits,
2736  std::move(_type),
2737  {std::move(_src), std::move(_upper), std::move(_lower)})
2738  {
2739  }
2740 
2742  exprt _src,
2743  const std::size_t _upper,
2744  const std::size_t _lower,
2745  typet _type);
2746 
2748  {
2749  return op0();
2750  }
2751 
2753  {
2754  return op1();
2755  }
2756 
2758  {
2759  return op2();
2760  }
2761 
2762  const exprt &src() const
2763  {
2764  return op0();
2765  }
2766 
2767  const exprt &upper() const
2768  {
2769  return op1();
2770  }
2771 
2772  const exprt &lower() const
2773  {
2774  return op2();
2775  }
2776 };
2777 
2778 template <>
2779 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
2780 {
2781  return base.id() == ID_extractbits;
2782 }
2783 
2784 inline void validate_expr(const extractbits_exprt &value)
2785 {
2786  validate_operands(value, 3, "Extract bits must have three operands");
2787 }
2788 
2795 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
2796 {
2797  PRECONDITION(expr.id()==ID_extractbits);
2798  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
2799  validate_expr(ret);
2800  return ret;
2801 }
2802 
2805 {
2806  PRECONDITION(expr.id()==ID_extractbits);
2807  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
2808  validate_expr(ret);
2809  return ret;
2810 }
2811 
2812 
2815 {
2816 public:
2817  explicit address_of_exprt(const exprt &op);
2818 
2820  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
2821  {
2822  }
2823 
2825  {
2826  return op0();
2827  }
2828 
2829  const exprt &object() const
2830  {
2831  return op0();
2832  }
2833 };
2834 
2835 template <>
2836 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
2837 {
2838  return base.id() == ID_address_of;
2839 }
2840 
2841 inline void validate_expr(const address_of_exprt &value)
2842 {
2843  validate_operands(value, 1, "Address of must have one operand");
2844 }
2845 
2852 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
2853 {
2854  PRECONDITION(expr.id()==ID_address_of);
2855  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
2856  validate_expr(ret);
2857  return ret;
2858 }
2859 
2862 {
2863  PRECONDITION(expr.id()==ID_address_of);
2864  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
2865  validate_expr(ret);
2866  return ret;
2867 }
2868 
2869 
2872 {
2873 public:
2874  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2875  {
2876  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2877  }
2878 };
2879 
2880 template <>
2881 inline bool can_cast_expr<not_exprt>(const exprt &base)
2882 {
2883  return base.id() == ID_not;
2884 }
2885 
2886 inline void validate_expr(const not_exprt &value)
2887 {
2888  validate_operands(value, 1, "Not must have one operand");
2889 }
2890 
2897 inline const not_exprt &to_not_expr(const exprt &expr)
2898 {
2899  PRECONDITION(expr.id()==ID_not);
2900  const not_exprt &ret = static_cast<const not_exprt &>(expr);
2901  validate_expr(ret);
2902  return ret;
2903 }
2904 
2907 {
2908  PRECONDITION(expr.id()==ID_not);
2909  not_exprt &ret = static_cast<not_exprt &>(expr);
2910  validate_expr(ret);
2911  return ret;
2912 }
2913 
2914 
2917 {
2918 public:
2919  explicit dereference_exprt(const exprt &op):
2920  unary_exprt(ID_dereference, op, op.type().subtype())
2921  {
2922  PRECONDITION(op.type().id()==ID_pointer);
2923  }
2924 
2926  : unary_exprt(ID_dereference, std::move(op), std::move(type))
2927  {
2928  }
2929 
2931  {
2932  return op0();
2933  }
2934 
2935  const exprt &pointer() const
2936  {
2937  return op0();
2938  }
2939 
2940  static void check(
2941  const exprt &expr,
2943  {
2944  DATA_CHECK(
2945  vm,
2946  expr.operands().size() == 1,
2947  "dereference expression must have one operand");
2948  }
2949 
2950  static void validate(
2951  const exprt &expr,
2952  const namespacet &ns,
2954 };
2955 
2956 template <>
2957 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
2958 {
2959  return base.id() == ID_dereference;
2960 }
2961 
2962 inline void validate_expr(const dereference_exprt &value)
2963 {
2964  validate_operands(value, 1, "Dereference must have one operand");
2965 }
2966 
2973 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
2974 {
2975  PRECONDITION(expr.id()==ID_dereference);
2976  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
2977  validate_expr(ret);
2978  return ret;
2979 }
2980 
2983 {
2984  PRECONDITION(expr.id()==ID_dereference);
2985  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
2986  validate_expr(ret);
2987  return ret;
2988 }
2989 
2990 
2992 class if_exprt : public ternary_exprt
2993 {
2994 public:
2996  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2997  {
2998  }
2999 
3001  : ternary_exprt(
3002  ID_if,
3003  std::move(cond),
3004  std::move(t),
3005  std::move(f),
3006  std::move(type))
3007  {
3008  }
3009 
3011  {
3012  return op0();
3013  }
3014 
3015  const exprt &cond() const
3016  {
3017  return op0();
3018  }
3019 
3021  {
3022  return op1();
3023  }
3024 
3025  const exprt &true_case() const
3026  {
3027  return op1();
3028  }
3029 
3031  {
3032  return op2();
3033  }
3034 
3035  const exprt &false_case() const
3036  {
3037  return op2();
3038  }
3039 };
3040 
3041 template <>
3042 inline bool can_cast_expr<if_exprt>(const exprt &base)
3043 {
3044  return base.id() == ID_if;
3045 }
3046 
3047 inline void validate_expr(const if_exprt &value)
3048 {
3049  validate_operands(value, 3, "If-then-else must have three operands");
3050 }
3051 
3058 inline const if_exprt &to_if_expr(const exprt &expr)
3059 {
3060  PRECONDITION(expr.id()==ID_if);
3061  const if_exprt &ret = static_cast<const if_exprt &>(expr);
3062  validate_expr(ret);
3063  return ret;
3064 }
3065 
3067 inline if_exprt &to_if_expr(exprt &expr)
3068 {
3069  PRECONDITION(expr.id()==ID_if);
3070  if_exprt &ret = static_cast<if_exprt &>(expr);
3071  validate_expr(ret);
3072  return ret;
3073 }
3074 
3079 {
3080 public:
3081  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
3082  : expr_protectedt(
3083  ID_with,
3084  _old.type(),
3085  {_old, std::move(_where), std::move(_new_value)})
3086  {
3087  }
3088 
3090  {
3091  return op0();
3092  }
3093 
3094  const exprt &old() const
3095  {
3096  return op0();
3097  }
3098 
3100  {
3101  return op1();
3102  }
3103 
3104  const exprt &where() const
3105  {
3106  return op1();
3107  }
3108 
3110  {
3111  return op2();
3112  }
3113 
3114  const exprt &new_value() const
3115  {
3116  return op2();
3117  }
3118 };
3119 
3120 template <>
3121 inline bool can_cast_expr<with_exprt>(const exprt &base)
3122 {
3123  return base.id() == ID_with;
3124 }
3125 
3126 inline void validate_expr(const with_exprt &value)
3127 {
3129  value, 3, "array/structure update must have at least 3 operands", true);
3131  value.operands().size() % 2 == 1,
3132  "array/structure update must have an odd number of operands");
3133 }
3134 
3141 inline const with_exprt &to_with_expr(const exprt &expr)
3142 {
3143  PRECONDITION(expr.id()==ID_with);
3144  const with_exprt &ret = static_cast<const with_exprt &>(expr);
3145  validate_expr(ret);
3146  return ret;
3147 }
3148 
3151 {
3152  PRECONDITION(expr.id()==ID_with);
3153  with_exprt &ret = static_cast<with_exprt &>(expr);
3154  validate_expr(ret);
3155  return ret;
3156 }
3157 
3159 {
3160 public:
3161  explicit index_designatort(exprt _index)
3162  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
3163  {
3164  }
3165 
3166  const exprt &index() const
3167  {
3168  return op0();
3169  }
3170 
3172  {
3173  return op0();
3174  }
3175 };
3176 
3177 template <>
3178 inline bool can_cast_expr<index_designatort>(const exprt &base)
3179 {
3180  return base.id() == ID_index_designator;
3181 }
3182 
3183 inline void validate_expr(const index_designatort &value)
3184 {
3185  validate_operands(value, 1, "Index designator must have one operand");
3186 }
3187 
3194 inline const index_designatort &to_index_designator(const exprt &expr)
3195 {
3196  PRECONDITION(expr.id()==ID_index_designator);
3197  const index_designatort &ret = static_cast<const index_designatort &>(expr);
3198  validate_expr(ret);
3199  return ret;
3200 }
3201 
3204 {
3205  PRECONDITION(expr.id()==ID_index_designator);
3206  index_designatort &ret = static_cast<index_designatort &>(expr);
3207  validate_expr(ret);
3208  return ret;
3209 }
3210 
3212 {
3213 public:
3214  explicit member_designatort(const irep_idt &_component_name)
3215  : expr_protectedt(ID_member_designator, typet())
3216  {
3217  set(ID_component_name, _component_name);
3218  }
3219 
3221  {
3222  return get(ID_component_name);
3223  }
3224 };
3225 
3226 template <>
3228 {
3229  return base.id() == ID_member_designator;
3230 }
3231 
3232 inline void validate_expr(const member_designatort &value)
3233 {
3234  validate_operands(value, 0, "Member designator must not have operands");
3235 }
3236 
3244 {
3245  PRECONDITION(expr.id()==ID_member_designator);
3246  const member_designatort &ret = static_cast<const member_designatort &>(expr);
3247  validate_expr(ret);
3248  return ret;
3249 }
3250 
3253 {
3254  PRECONDITION(expr.id()==ID_member_designator);
3255  member_designatort &ret = static_cast<member_designatort &>(expr);
3256  validate_expr(ret);
3257  return ret;
3258 }
3259 
3260 
3263 {
3264 public:
3265  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
3266  : ternary_exprt(
3267  ID_update,
3268  _old,
3269  std::move(_designator),
3270  std::move(_new_value),
3271  _old.type())
3272  {
3273  }
3274 
3276  {
3277  return op0();
3278  }
3279 
3280  const exprt &old() const
3281  {
3282  return op0();
3283  }
3284 
3285  // the designator operands are either
3286  // 1) member_designator or
3287  // 2) index_designator
3288  // as defined above
3290  {
3291  return op1().operands();
3292  }
3293 
3295  {
3296  return op1().operands();
3297  }
3298 
3300  {
3301  return op2();
3302  }
3303 
3304  const exprt &new_value() const
3305  {
3306  return op2();
3307  }
3308 };
3309 
3310 template <>
3311 inline bool can_cast_expr<update_exprt>(const exprt &base)
3312 {
3313  return base.id() == ID_update;
3314 }
3315 
3316 inline void validate_expr(const update_exprt &value)
3317 {
3319  value, 3, "Array/structure update must have three operands");
3320 }
3321 
3328 inline const update_exprt &to_update_expr(const exprt &expr)
3329 {
3330  PRECONDITION(expr.id()==ID_update);
3331  const update_exprt &ret = static_cast<const update_exprt &>(expr);
3332  validate_expr(ret);
3333  return ret;
3334 }
3335 
3338 {
3339  PRECONDITION(expr.id()==ID_update);
3340  update_exprt &ret = static_cast<update_exprt &>(expr);
3341  validate_expr(ret);
3342  return ret;
3343 }
3344 
3345 
3346 #if 0
3347 class array_update_exprt:public expr_protectedt
3349 {
3350 public:
3351  array_update_exprt(
3352  const exprt &_array,
3353  const exprt &_index,
3354  const exprt &_new_value):
3355  exprt(ID_array_update, _array.type())
3356  {
3357  add_to_operands(_array, _index, _new_value);
3358  }
3359 
3360  array_update_exprt():expr_protectedt(ID_array_update)
3361  {
3362  operands().resize(3);
3363  }
3364 
3365  exprt &array()
3366  {
3367  return op0();
3368  }
3369 
3370  const exprt &array() const
3371  {
3372  return op0();
3373  }
3374 
3375  exprt &index()
3376  {
3377  return op1();
3378  }
3379 
3380  const exprt &index() const
3381  {
3382  return op1();
3383  }
3384 
3385  exprt &new_value()
3386  {
3387  return op2();
3388  }
3389 
3390  const exprt &new_value() const
3391  {
3392  return op2();
3393  }
3394 };
3395 
3396 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3397 {
3398  return base.id()==ID_array_update;
3399 }
3400 
3401 inline void validate_expr(const array_update_exprt &value)
3402 {
3403  validate_operands(value, 3, "Array update must have three operands");
3404 }
3405 
3412 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3413 {
3414  PRECONDITION(expr.id()==ID_array_update);
3415  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
3416  validate_expr(ret);
3417  return ret;
3418 }
3419 
3421 inline array_update_exprt &to_array_update_expr(exprt &expr)
3422 {
3423  PRECONDITION(expr.id()==ID_array_update);
3424  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
3425  validate_expr(ret);
3426  return ret;
3427 }
3428 
3429 #endif
3430 
3431 
3434 {
3435 public:
3436  member_exprt(exprt op, const irep_idt &component_name, typet _type)
3437  : unary_exprt(ID_member, std::move(op), std::move(_type))
3438  {
3439  set_component_name(component_name);
3440  }
3441 
3443  : unary_exprt(ID_member, std::move(op), c.type())
3444  {
3446  }
3447 
3449  {
3450  return get(ID_component_name);
3451  }
3452 
3453  void set_component_name(const irep_idt &component_name)
3454  {
3455  set(ID_component_name, component_name);
3456  }
3457 
3458  std::size_t get_component_number() const
3459  {
3460  return get_size_t(ID_component_number);
3461  }
3462 
3463  // will go away, use compound()
3464  const exprt &struct_op() const
3465  {
3466  return op0();
3467  }
3468 
3469  // will go away, use compound()
3471  {
3472  return op0();
3473  }
3474 
3475  const exprt &compound() const
3476  {
3477  return op0();
3478  }
3479 
3481  {
3482  return op0();
3483  }
3484 
3485  static void check(
3486  const exprt &expr,
3488  {
3489  DATA_CHECK(
3490  vm,
3491  expr.operands().size() == 1,
3492  "member expression must have one operand");
3493  }
3494 
3495  static void validate(
3496  const exprt &expr,
3497  const namespacet &ns,
3499 };
3500 
3501 template <>
3502 inline bool can_cast_expr<member_exprt>(const exprt &base)
3503 {
3504  return base.id() == ID_member;
3505 }
3506 
3507 inline void validate_expr(const member_exprt &value)
3508 {
3509  validate_operands(value, 1, "Extract member must have one operand");
3510 }
3511 
3518 inline const member_exprt &to_member_expr(const exprt &expr)
3519 {
3520  PRECONDITION(expr.id()==ID_member);
3521  const member_exprt &ret = static_cast<const member_exprt &>(expr);
3522  validate_expr(ret);
3523  return ret;
3524 }
3525 
3528 {
3529  PRECONDITION(expr.id()==ID_member);
3530  member_exprt &ret = static_cast<member_exprt &>(expr);
3531  validate_expr(ret);
3532  return ret;
3533 }
3534 
3535 
3538 {
3539 public:
3541  : unary_predicate_exprt(ID_isnan, std::move(op))
3542  {
3543  }
3544 };
3545 
3546 template <>
3547 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
3548 {
3549  return base.id() == ID_isnan;
3550 }
3551 
3552 inline void validate_expr(const isnan_exprt &value)
3553 {
3554  validate_operands(value, 1, "Is NaN must have one operand");
3555 }
3556 
3563 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3564 {
3565  PRECONDITION(expr.id()==ID_isnan);
3566  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
3567  validate_expr(ret);
3568  return ret;
3569 }
3570 
3573 {
3574  PRECONDITION(expr.id()==ID_isnan);
3575  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
3576  validate_expr(ret);
3577  return ret;
3578 }
3579 
3580 
3583 {
3584 public:
3586  : unary_predicate_exprt(ID_isinf, std::move(op))
3587  {
3588  }
3589 };
3590 
3591 template <>
3592 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
3593 {
3594  return base.id() == ID_isinf;
3595 }
3596 
3597 inline void validate_expr(const isinf_exprt &value)
3598 {
3599  validate_operands(value, 1, "Is infinite must have one operand");
3600 }
3601 
3608 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3609 {
3610  PRECONDITION(expr.id()==ID_isinf);
3611  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
3612  validate_expr(ret);
3613  return ret;
3614 }
3615 
3618 {
3619  PRECONDITION(expr.id()==ID_isinf);
3620  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
3621  validate_expr(ret);
3622  return ret;
3623 }
3624 
3625 
3628 {
3629 public:
3631  : unary_predicate_exprt(ID_isfinite, std::move(op))
3632  {
3633  }
3634 };
3635 
3636 template <>
3637 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
3638 {
3639  return base.id() == ID_isfinite;
3640 }
3641 
3642 inline void validate_expr(const isfinite_exprt &value)
3643 {
3644  validate_operands(value, 1, "Is finite must have one operand");
3645 }
3646 
3653 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
3654 {
3655  PRECONDITION(expr.id()==ID_isfinite);
3656  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
3657  validate_expr(ret);
3658  return ret;
3659 }
3660 
3663 {
3664  PRECONDITION(expr.id()==ID_isfinite);
3665  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
3666  validate_expr(ret);
3667  return ret;
3668 }
3669 
3670 
3673 {
3674 public:
3676  : unary_predicate_exprt(ID_isnormal, std::move(op))
3677  {
3678  }
3679 };
3680 
3681 template <>
3682 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
3683 {
3684  return base.id() == ID_isnormal;
3685 }
3686 
3687 inline void validate_expr(const isnormal_exprt &value)
3688 {
3689  validate_operands(value, 1, "Is normal must have one operand");
3690 }
3691 
3698 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
3699 {
3700  PRECONDITION(expr.id()==ID_isnormal);
3701  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
3702  validate_expr(ret);
3703  return ret;
3704 }
3705 
3708 {
3709  PRECONDITION(expr.id()==ID_isnormal);
3710  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
3711  validate_expr(ret);
3712  return ret;
3713 }
3714 
3715 
3718 {
3719 public:
3722  std::move(_lhs),
3723  ID_ieee_float_equal,
3724  std::move(_rhs))
3725  {
3726  }
3727 };
3728 
3729 template <>
3731 {
3732  return base.id() == ID_ieee_float_equal;
3733 }
3734 
3735 inline void validate_expr(const ieee_float_equal_exprt &value)
3736 {
3737  validate_operands(value, 2, "IEEE equality must have two operands");
3738 }
3739 
3747 {
3748  PRECONDITION(expr.id()==ID_ieee_float_equal);
3749  const ieee_float_equal_exprt &ret =
3750  static_cast<const ieee_float_equal_exprt &>(expr);
3751  validate_expr(ret);
3752  return ret;
3753 }
3754 
3757 {
3758  PRECONDITION(expr.id()==ID_ieee_float_equal);
3759  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
3760  validate_expr(ret);
3761  return ret;
3762 }
3763 
3764 
3767 {
3768 public:
3771  std::move(_lhs),
3772  ID_ieee_float_notequal,
3773  std::move(_rhs))
3774  {
3775  }
3776 };
3777 
3778 template <>
3780 {
3781  return base.id() == ID_ieee_float_notequal;
3782 }
3783 
3784 inline void validate_expr(const ieee_float_notequal_exprt &value)
3785 {
3786  validate_operands(value, 2, "IEEE inequality must have two operands");
3787 }
3788 
3796  const exprt &expr)
3797 {
3798  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3799  const ieee_float_notequal_exprt &ret =
3800  static_cast<const ieee_float_notequal_exprt &>(expr);
3801  validate_expr(ret);
3802  return ret;
3803 }
3804 
3807 {
3808  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3810  static_cast<ieee_float_notequal_exprt &>(expr);
3811  validate_expr(ret);
3812  return ret;
3813 }
3814 
3819 {
3820 public:
3822  const exprt &_lhs,
3823  const irep_idt &_id,
3824  exprt _rhs,
3825  exprt _rm)
3826  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
3827  {
3828  }
3829 
3831  {
3832  return op0();
3833  }
3834 
3835  const exprt &lhs() const
3836  {
3837  return op0();
3838  }
3839 
3841  {
3842  return op1();
3843  }
3844 
3845  const exprt &rhs() const
3846  {
3847  return op1();
3848  }
3849 
3851  {
3852  return op2();
3853  }
3854 
3855  const exprt &rounding_mode() const
3856  {
3857  return op2();
3858  }
3859 };
3860 
3861 template <>
3863 {
3864  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
3865  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
3866 }
3867 
3868 inline void validate_expr(const ieee_float_op_exprt &value)
3869 {
3871  value, 3, "IEEE float operations must have three arguments");
3872 }
3873 
3881 {
3882  const ieee_float_op_exprt &ret =
3883  static_cast<const ieee_float_op_exprt &>(expr);
3884  validate_expr(ret);
3885  return ret;
3886 }
3887 
3890 {
3891  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
3892  validate_expr(ret);
3893  return ret;
3894 }
3895 
3896 
3899 {
3900 public:
3901  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
3902  {
3903  }
3904 };
3905 
3906 template <>
3907 inline bool can_cast_expr<type_exprt>(const exprt &base)
3908 {
3909  return base.id() == ID_type;
3910 }
3911 
3918 inline const type_exprt &to_type_expr(const exprt &expr)
3919 {
3921  const type_exprt &ret = static_cast<const type_exprt &>(expr);
3922  return ret;
3923 }
3924 
3927 {
3929  type_exprt &ret = static_cast<type_exprt &>(expr);
3930  return ret;
3931 }
3932 
3935 {
3936 public:
3937  constant_exprt(const irep_idt &_value, typet _type)
3938  : expr_protectedt(ID_constant, std::move(_type))
3939  {
3940  set_value(_value);
3941  }
3942 
3943  const irep_idt &get_value() const
3944  {
3945  return get(ID_value);
3946  }
3947 
3948  void set_value(const irep_idt &value)
3949  {
3950  set(ID_value, value);
3951  }
3952 
3953  bool value_is_zero_string() const;
3954 };
3955 
3956 template <>
3957 inline bool can_cast_expr<constant_exprt>(const exprt &base)
3958 {
3959  return base.id() == ID_constant;
3960 }
3961 
3968 inline const constant_exprt &to_constant_expr(const exprt &expr)
3969 {
3970  PRECONDITION(expr.id()==ID_constant);
3971  return static_cast<const constant_exprt &>(expr);
3972 }
3973 
3976 {
3977  PRECONDITION(expr.id()==ID_constant);
3978  return static_cast<constant_exprt &>(expr);
3979 }
3980 
3981 
3984 {
3985 public:
3987  {
3988  }
3989 };
3990 
3993 {
3994 public:
3996  {
3997  }
3998 };
3999 
4001 class nil_exprt : public nullary_exprt
4002 {
4003 public:
4005  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
4006  {
4007  }
4008 };
4009 
4010 template <>
4011 inline bool can_cast_expr<nil_exprt>(const exprt &base)
4012 {
4013  return base.id() == ID_nil;
4014 }
4015 
4018 {
4019 public:
4021  : constant_exprt(ID_NULL, std::move(type))
4022  {
4023  }
4024 };
4025 
4028 {
4029 public:
4030  replication_exprt(const constant_exprt &_times, const exprt &_src)
4031  : binary_exprt(_times, ID_replication, _src)
4032  {
4033  }
4034 
4036  {
4037  return static_cast<constant_exprt &>(op0());
4038  }
4039 
4040  const constant_exprt &times() const
4041  {
4042  return static_cast<const constant_exprt &>(op0());
4043  }
4044 
4046  {
4047  return op1();
4048  }
4049 
4050  const exprt &op() const
4051  {
4052  return op1();
4053  }
4054 };
4055 
4056 template <>
4057 inline bool can_cast_expr<replication_exprt>(const exprt &base)
4058 {
4059  return base.id() == ID_replication;
4060 }
4061 
4062 inline void validate_expr(const replication_exprt &value)
4063 {
4064  validate_operands(value, 2, "Bit-wise replication must have two operands");
4065 }
4066 
4073 inline const replication_exprt &to_replication_expr(const exprt &expr)
4074 {
4075  PRECONDITION(expr.id() == ID_replication);
4076  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
4077  validate_expr(ret);
4078  return ret;
4079 }
4080 
4083 {
4084  PRECONDITION(expr.id() == ID_replication);
4085  replication_exprt &ret = static_cast<replication_exprt &>(expr);
4086  validate_expr(ret);
4087  return ret;
4088 }
4089 
4096 {
4097 public:
4099  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4100  {
4101  }
4102 
4104  : multi_ary_exprt(
4105  ID_concatenation,
4106  {std::move(_op0), std::move(_op1)},
4107  std::move(_type))
4108  {
4109  }
4110 };
4111 
4112 template <>
4114 {
4115  return base.id() == ID_concatenation;
4116 }
4117 
4125 {
4126  PRECONDITION(expr.id()==ID_concatenation);
4127  return static_cast<const concatenation_exprt &>(expr);
4128 }
4129 
4132 {
4133  PRECONDITION(expr.id()==ID_concatenation);
4134  return static_cast<concatenation_exprt &>(expr);
4135 }
4136 
4137 
4140 {
4141 public:
4142  explicit infinity_exprt(typet _type)
4143  : nullary_exprt(ID_infinity, std::move(_type))
4144  {
4145  }
4146 };
4147 
4150 {
4151 public:
4152  using variablest = std::vector<symbol_exprt>;
4153 
4156  irep_idt _id,
4157  const variablest &_variables,
4158  exprt _where,
4159  typet _type)
4160  : binary_exprt(
4162  ID_tuple,
4163  (const operandst &)_variables,
4164  typet(ID_tuple)),
4165  _id,
4166  std::move(_where),
4167  std::move(_type))
4168  {
4169  }
4170 
4172  {
4173  return (variablest &)to_multi_ary_expr(op0()).operands();
4174  }
4175 
4176  const variablest &variables() const
4177  {
4178  return (variablest &)to_multi_ary_expr(op0()).operands();
4179  }
4180 
4182  {
4183  return op1();
4184  }
4185 
4186  const exprt &where() const
4187  {
4188  return op1();
4189  }
4190 };
4191 
4193 class let_exprt : public binary_exprt
4194 {
4195 public:
4198  operandst values,
4199  const exprt &where)
4200  : binary_exprt(
4201  binding_exprt(
4202  ID_let_binding,
4203  std::move(variables),
4204  where,
4205  where.type()),
4206  ID_let,
4207  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
4208  where.type())
4209  {
4210  PRECONDITION(this->variables().size() == this->values().size());
4211  }
4212 
4215  : let_exprt(
4216  binding_exprt::variablest{std::move(symbol)},
4217  operandst{std::move(value)},
4218  where)
4219  {
4220  }
4221 
4223  {
4224  return static_cast<binding_exprt &>(op0());
4225  }
4226 
4227  const binding_exprt &binding() const
4228  {
4229  return static_cast<const binding_exprt &>(op0());
4230  }
4231 
4234  {
4235  auto &variables = binding().variables();
4236  PRECONDITION(variables.size() == 1);
4237  return variables.front();
4238  }
4239 
4241  const symbol_exprt &symbol() const
4242  {
4243  const auto &variables = binding().variables();
4244  PRECONDITION(variables.size() == 1);
4245  return variables.front();
4246  }
4247 
4250  {
4251  auto &values = this->values();
4252  PRECONDITION(values.size() == 1);
4253  return values.front();
4254  }
4255 
4257  const exprt &value() const
4258  {
4259  const auto &values = this->values();
4260  PRECONDITION(values.size() == 1);
4261  return values.front();
4262  }
4263 
4265  {
4266  return static_cast<multi_ary_exprt &>(op1()).operands();
4267  }
4268 
4269  const operandst &values() const
4270  {
4271  return static_cast<const multi_ary_exprt &>(op1()).operands();
4272  }
4273 
4276  {
4277  return binding().variables();
4278  }
4279 
4282  {
4283  return binding().variables();
4284  }
4285 
4288  {
4289  return binding().where();
4290  }
4291 
4293  const exprt &where() const
4294  {
4295  return binding().where();
4296  }
4297 
4298  static void validate(const exprt &, validation_modet);
4299 };
4300 
4301 template <>
4302 inline bool can_cast_expr<let_exprt>(const exprt &base)
4303 {
4304  return base.id() == ID_let;
4305 }
4306 
4307 inline void validate_expr(const let_exprt &let_expr)
4308 {
4309  validate_operands(let_expr, 2, "Let must have two operands");
4310 }
4311 
4318 inline const let_exprt &to_let_expr(const exprt &expr)
4319 {
4320  PRECONDITION(expr.id()==ID_let);
4321  const let_exprt &ret = static_cast<const let_exprt &>(expr);
4322  validate_expr(ret);
4323  return ret;
4324 }
4325 
4328 {
4329  PRECONDITION(expr.id()==ID_let);
4330  let_exprt &ret = static_cast<let_exprt &>(expr);
4331  validate_expr(ret);
4332  return ret;
4333 }
4334 
4337 {
4338 public:
4340  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4341  {
4342  }
4343 
4344  explicit popcount_exprt(const exprt &_op)
4345  : unary_exprt(ID_popcount, _op, _op.type())
4346  {
4347  }
4348 };
4349 
4350 template <>
4351 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4352 {
4353  return base.id() == ID_popcount;
4354 }
4355 
4356 inline void validate_expr(const popcount_exprt &value)
4357 {
4358  validate_operands(value, 1, "popcount must have one operand");
4359 }
4360 
4367 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4368 {
4369  PRECONDITION(expr.id() == ID_popcount);
4370  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
4371  validate_expr(ret);
4372  return ret;
4373 }
4374 
4377 {
4378  PRECONDITION(expr.id() == ID_popcount);
4379  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
4380  validate_expr(ret);
4381  return ret;
4382 }
4383 
4388 {
4389 public:
4390  cond_exprt(operandst _operands, typet _type)
4391  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
4392  {
4393  }
4394 
4398  void add_case(const exprt &condition, const exprt &value)
4399  {
4400  PRECONDITION(condition.type().id() == ID_bool);
4401  operands().reserve(operands().size() + 2);
4402  operands().push_back(condition);
4403  operands().push_back(value);
4404  }
4405 };
4406 
4407 template <>
4408 inline bool can_cast_expr<cond_exprt>(const exprt &base)
4409 {
4410  return base.id() == ID_cond;
4411 }
4412 
4413 inline void validate_expr(const cond_exprt &value)
4414 {
4416  value.operands().size() % 2 == 0, "cond must have even number of operands");
4417 }
4418 
4425 inline const cond_exprt &to_cond_expr(const exprt &expr)
4426 {
4427  PRECONDITION(expr.id() == ID_cond);
4428  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
4429  validate_expr(ret);
4430  return ret;
4431 }
4432 
4435 {
4436  PRECONDITION(expr.id() == ID_cond);
4437  cond_exprt &ret = static_cast<cond_exprt &>(expr);
4438  validate_expr(ret);
4439  return ret;
4440 }
4441 
4451 {
4452 public:
4454  symbol_exprt arg,
4455  exprt body,
4456  array_typet _type)
4457  : binary_exprt(
4458  std::move(arg),
4459  ID_array_comprehension,
4460  std::move(body),
4461  std::move(_type))
4462  {
4463  }
4464 
4465  const array_typet &type() const
4466  {
4467  return static_cast<const array_typet &>(binary_exprt::type());
4468  }
4469 
4471  {
4472  return static_cast<array_typet &>(binary_exprt::type());
4473  }
4474 
4475  const symbol_exprt &arg() const
4476  {
4477  return static_cast<const symbol_exprt &>(op0());
4478  }
4479 
4481  {
4482  return static_cast<symbol_exprt &>(op0());
4483  }
4484 
4485  const exprt &body() const
4486  {
4487  return op1();
4488  }
4489 
4491  {
4492  return op1();
4493  }
4494 };
4495 
4496 template <>
4498 {
4499  return base.id() == ID_array_comprehension;
4500 }
4501 
4502 inline void validate_expr(const array_comprehension_exprt &value)
4503 {
4504  validate_operands(value, 2, "'Array comprehension' must have two operands");
4505 }
4506 
4513 inline const array_comprehension_exprt &
4515 {
4516  PRECONDITION(expr.id() == ID_array_comprehension);
4517  const array_comprehension_exprt &ret =
4518  static_cast<const array_comprehension_exprt &>(expr);
4519  validate_expr(ret);
4520  return ret;
4521 }
4522 
4525 {
4526  PRECONDITION(expr.id() == ID_array_comprehension);
4528  static_cast<array_comprehension_exprt &>(expr);
4529  validate_expr(ret);
4530  return ret;
4531 }
4532 
4533 inline void validate_expr(const class class_method_descriptor_exprt &value);
4534 
4537 {
4538 public:
4554  typet _type,
4558  : nullary_exprt(ID_virtual_function, std::move(_type))
4559  {
4561  set(ID_component_name, std::move(mangled_method_name));
4562  set(ID_C_class, std::move(class_id));
4563  set(ID_C_base_name, std::move(base_method_name));
4564  set(ID_identifier, std::move(id));
4565  validate_expr(*this);
4566  }
4567 
4575  {
4576  return get(ID_component_name);
4577  }
4578 
4582  const irep_idt &class_id() const
4583  {
4584  return get(ID_C_class);
4585  }
4586 
4590  {
4591  return get(ID_C_base_name);
4592  }
4593 
4597  const irep_idt &get_identifier() const
4598  {
4599  return get(ID_identifier);
4600  }
4601 };
4602 
4603 inline void validate_expr(const class class_method_descriptor_exprt &value)
4604 {
4605  validate_operands(value, 0, "class method descriptor must not have operands");
4607  !value.mangled_method_name().empty(),
4608  "class method descriptor must have a mangled method name.");
4610  !value.class_id().empty(), "class method descriptor must have a class id.");
4612  !value.base_method_name().empty(),
4613  "class method descriptor must have a base method name.");
4615  value.get_identifier() == id2string(value.class_id()) + "." +
4616  id2string(value.mangled_method_name()),
4617  "class method descriptor must have an identifier in the expected format.");
4618 }
4619 
4626 inline const class_method_descriptor_exprt &
4628 {
4629  PRECONDITION(expr.id() == ID_virtual_function);
4630  const class_method_descriptor_exprt &ret =
4631  static_cast<const class_method_descriptor_exprt &>(expr);
4632  validate_expr(ret);
4633  return ret;
4634 }
4635 
4636 template <>
4638 {
4639  return base.id() == ID_virtual_function;
4640 }
4641 
4642 #endif // CPROVER_UTIL_STD_EXPR_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3078
index_exprt::array
const exprt & array() const
Definition: std_expr.h:1320
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4367
exprt::op2
exprt & op2()
Definition: expr.h:107
dynamic_object_exprt::dynamic_object_exprt
dynamic_object_exprt(typet type)
Definition: std_expr.h:1945
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
if_exprt::if_exprt
if_exprt(exprt cond, const exprt &t, exprt f)
Definition: std_expr.h:2995
can_cast_expr< symbol_exprt >
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:161
to_array_comprehension_expr
const array_comprehension_exprt & to_array_comprehension_expr(const exprt &expr)
Cast an exprt to a array_comprehension_exprt.
Definition: std_expr.h:4514
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1563
can_cast_expr< union_exprt >
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1609
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3328
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2050
can_cast_expr< rem_exprt >
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1160
index_exprt::index
const exprt & index() const
Definition: std_expr.h:1330
shl_exprt::shl_exprt
shl_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2597
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
can_cast_expr< isnan_exprt >
bool can_cast_expr< isnan_exprt >(const exprt &base)
Definition: std_expr.h:3547
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:790
binary_relation_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:732
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
let_exprt::let_exprt
let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
convenience constructor for the case of a single binding
Definition: std_expr.h:4214
can_cast_expr< cond_exprt >
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:4408
member_exprt::member_exprt
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:3436
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1515
can_cast_expr< mod_exprt >
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1115
extractbits_exprt::lower
exprt & lower()
Definition: std_expr.h:2757
binding_exprt::where
const exprt & where() const
Definition: std_expr.h:4186
if_exprt::if_exprt
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:3000
member_designatort::member_designatort
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3214
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2527
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1086
binary_exprt::rhs
exprt & rhs()
Definition: std_expr.h:641
can_cast_expr< index_designatort >
bool can_cast_expr< index_designatort >(const exprt &base)
Definition: std_expr.h:3178
can_cast_expr< isinf_exprt >
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:3592
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:4574
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2181
array_list_exprt::array_list_exprt
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1492
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1474
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:196
and_exprt::and_exprt
and_exprt(exprt::operandst _operands)
Definition: std_expr.h:2189
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: std_expr.cpp:141
can_cast_expr< complex_imag_exprt >
bool can_cast_expr< complex_imag_exprt >(const exprt &base)
Definition: std_expr.h:1811
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2645
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2824
can_cast_expr< concatenation_exprt >
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4113
nondet_symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:225
array_of_exprt::what
exprt & what()
Definition: std_expr.h:1390
binary_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:646
can_cast_expr< floatbv_typecast_exprt >
bool can_cast_expr< floatbv_typecast_exprt >(const exprt &base)
Definition: std_expr.h:2129
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
complex_exprt::real
const exprt & real() const
Definition: std_expr.h:1705
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op, typet _type)
Definition: std_expr.h:380
to_type_expr
const type_exprt & to_type_expr(const exprt &expr)
Cast an exprt to an type_exprt.
Definition: std_expr.h:3918
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:810
can_cast_expr< bitor_exprt >
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2426
floatbv_typecast_exprt::op
exprt & op()
Definition: std_expr.h:2107
can_cast_expr< not_exprt >
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2881
typet
The type of an expression, extends irept.
Definition: type.h:28
ieee_float_notequal_exprt::ieee_float_notequal_exprt
ieee_float_notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3769
update_exprt::old
exprt & old()
Definition: std_expr.h:3275
binary_relation_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:739
ternary_exprt
An expression with three operands.
Definition: std_expr.h:54
true_exprt::true_exprt
true_exprt()
Definition: std_expr.h:3986
mult_exprt::mult_exprt
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:994
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1353
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3058
isnormal_exprt::isnormal_exprt
isnormal_exprt(exprt op)
Definition: std_expr.h:3675
can_cast_expr< sign_exprt >
bool can_cast_expr< sign_exprt >(const exprt &base)
Definition: std_expr.h:566
ieee_float_equal_exprt::ieee_float_equal_exprt
ieee_float_equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:3720
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2916
extractbits_exprt::src
const exprt & src() const
Definition: std_expr.h:2762
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: std_expr.h:1936
symbol_exprt::symbol_exprt
symbol_exprt(typet type)
Definition: std_expr.h:85
can_cast_expr< unary_exprt >
bool can_cast_expr< unary_exprt >(const exprt &base)
Definition: std_expr.h:300
if_exprt::true_case
const exprt & true_case() const
Definition: std_expr.h:3025
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2992
member_designatort
Definition: std_expr.h:3211
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: std_expr.h:2006
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
can_cast_expr< isfinite_exprt >
bool can_cast_expr< isfinite_exprt >(const exprt &base)
Definition: std_expr.h:3637
replication_exprt::times
constant_exprt & times()
Definition: std_expr.h:4035
div_exprt::div_exprt
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1039
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
array_list_exprt::type
array_typet & type()
Definition: std_expr.h:1502
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1848
xor_exprt
Boolean XOR.
Definition: std_expr.h:2336
dereference_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
Definition: std_expr.cpp:282
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3109
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:889
binary_predicate_exprt::binary_predicate_exprt
binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
Definition: std_expr.h:696
complex_real_exprt
Real part of the expression describing a complex number.
Definition: std_expr.h:1756
invariant.h
address_of_exprt::address_of_exprt
address_of_exprt(const exprt &op)
Definition: std_expr.cpp:185
let_exprt::symbol
symbol_exprt & symbol()
convenience accessor for the symbol of a single binding
Definition: std_expr.h:4233
and_exprt
Boolean AND.
Definition: std_expr.h:2165
union_exprt
Union constructor from single element.
Definition: std_expr.h:1578
array_comprehension_exprt::type
array_typet & type()
Definition: std_expr.h:4470
disjunction
exprt disjunction(const exprt::operandst &)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
bitxor_exprt::bitxor_exprt
bitxor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2455
can_cast_expr< bitxor_exprt >
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2462
to_ieee_float_equal_expr
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
Definition: std_expr.h:3746
to_array_of_expr
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Definition: std_expr.h:1418
can_cast_expr< ieee_float_notequal_exprt >
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:3779
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:886
can_cast_expr< xor_exprt >
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2346
rem_exprt
Remainder of division.
Definition: std_expr.h:1150
equal_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1210
can_cast_expr< unary_minus_exprt >
bool can_cast_expr< unary_minus_exprt >(const exprt &base)
Definition: std_expr.h:392
abs_exprt::abs_exprt
abs_exprt(exprt _op)
Definition: std_expr.h:336
exprt
Base class for all expressions.
Definition: expr.h:52
class_method_descriptor_exprt::class_method_descriptor_exprt
class_method_descriptor_exprt(typet _type, irep_idt mangled_method_name, irep_idt class_id, irep_idt base_method_name)
Definition: std_expr.h:4553
unary_exprt::op1
const exprt & op1() const =delete
to_complex_expr
const complex_exprt & to_complex_expr(const exprt &expr)
Cast an exprt to a complex_exprt.
Definition: std_expr.h:1738
binary_exprt::lhs
exprt & lhs()
Definition: std_expr.h:631
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:268
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2630
array_exprt::array_exprt
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1446
dereference_exprt::dereference_exprt
dereference_exprt(const exprt &op)
Definition: std_expr.h:2919
index_exprt::index_exprt
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1306
decorated_symbol_exprt::clear_static_lifetime
void clear_static_lifetime()
Definition: std_expr.h:139
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:600
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1625
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte)
Definition: std_expr.h:479
array_of_exprt::type
array_typet & type()
Definition: std_expr.h:1385
member_designatort::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3220
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1789
bswap_exprt::get_bits_per_byte
std::size_t get_bits_per_byte() const
Definition: std_expr.h:485
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2289
sign_exprt
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:556
can_cast_expr< binary_exprt >
bool can_cast_expr< binary_exprt >(const exprt &base)
Definition: std_expr.h:662
update_exprt::designator
const exprt::operandst & designator() const
Definition: std_expr.h:3294
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1380
exprt::op0
exprt & op0()
Definition: expr.h:101
predicate_exprt::predicate_exprt
predicate_exprt(const irep_idt &_id)
Definition: std_expr.h:537
update_exprt::old
const exprt & old() const
Definition: std_expr.h:3280
extractbits_exprt::upper
const exprt & upper() const
Definition: std_expr.h:2767
replication_exprt::op
const exprt & op() const
Definition: std_expr.h:4050
let_exprt::validate
static void validate(const exprt &, validation_modet)
Definition: std_expr.cpp:308
array_comprehension_exprt::arg
const symbol_exprt & arg() const
Definition: std_expr.h:4475
cond_exprt::cond_exprt
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4390
can_cast_expr< minus_exprt >
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:955
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1525
vector_typet
The vector type.
Definition: std_types.h:1749
bool_typet
The Boolean type.
Definition: std_types.h:36
concatenation_exprt
Concatenation of bit-vector operands.
Definition: std_expr.h:4095
index_designatort::index_designatort
index_designatort(exprt _index)
Definition: std_expr.h:3161
nullary_exprt::move_to_operands
void move_to_operands(exprt &)=delete
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1542
to_isnormal_expr
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:3698
lshr_exprt
Logical right shift.
Definition: std_expr.h:2642
index_exprt::index_exprt
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1301
type_exprt::type_exprt
type_exprt(typet type)
Definition: std_expr.h:3901
to_complex_type
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1815
can_cast_expr< bitand_exprt >
bool can_cast_expr< bitand_exprt >(const exprt &base)
Definition: std_expr.h:2498
to_bitand_expr
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2509
div_exprt
Division.
Definition: std_expr.h:1036
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
shift_exprt::op
exprt & op()
Definition: std_expr.h:2534
can_cast_expr< array_exprt >
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1463
validate_expr
void validate_expr(const symbol_exprt &value)
Definition: std_expr.h:166
can_cast_expr< member_exprt >
bool can_cast_expr< member_exprt >(const exprt &base)
Definition: std_expr.h:3502
minus_exprt::minus_exprt
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:948
union_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:1597
equal_exprt
Equality.
Definition: std_expr.h:1195
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:4465
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:829
expanding_vectort
Definition: expanding_vector.h:16
to_rem_expr
const rem_exprt & to_rem_expr(const exprt &expr)
Cast an exprt to a rem_exprt.
Definition: std_expr.h:1176
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:971
floatbv_typecast_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:2122
replication_exprt
Bit-vector replication.
Definition: std_expr.h:4027
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1220
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4139
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3030
array_list_exprt::add
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1508
isfinite_exprt
Evaluates to true if the operand is finite.
Definition: std_expr.h:3627
can_cast_expr< implies_exprt >
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2238
notequal_exprt
Disequality.
Definition: std_expr.h:1253
replication_exprt::op
exprt & op()
Definition: std_expr.h:4045
extractbits_exprt::upper
exprt & upper()
Definition: std_expr.h:2752
binary_exprt::op3
const exprt & op3() const =delete
union_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:1592
multi_ary_exprt::op3
exprt & op3()
Definition: std_expr.h:835
nullary_exprt::op3
const exprt & op3() const =delete
to_unary_plus_expr
const unary_plus_exprt & to_unary_plus_expr(const exprt &expr)
Cast an exprt to a unary_plus_exprt.
Definition: std_expr.h:452
array_comprehension_exprt::arg
symbol_exprt & arg()
Definition: std_expr.h:4480
to_complex_real_expr
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Definition: std_expr.h:1783
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:678
binding_exprt::variables
variablest & variables()
Definition: std_expr.h:4171
narrow.h
to_concatenation_expr
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
Definition: std_expr.h:4124
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4536
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1644
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2572
let_exprt::variables
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:4281
union_exprt::union_exprt
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1581
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
complex_exprt::imag
exprt imag()
Definition: std_expr.h:1710
ieee_float_notequal_exprt
IEEE floating-point disequality.
Definition: std_expr.h:3766
to_nondet_symbol_expr
const nondet_symbol_exprt & to_nondet_symbol_expr(const exprt &expr)
Cast an exprt to a nondet_symbol_exprt.
Definition: std_expr.h:248
let_exprt::variables
binding_exprt::variablest & variables()
convenience accessor for binding().variables()
Definition: std_expr.h:4275
class_method_descriptor_exprt::get_identifier
const irep_idt & get_identifier() const
A unique identifier of the combination of class and method overload to which this expression refers.
Definition: std_expr.h:4597
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
let_exprt::value
exprt & value()
convenience accessor for the value of a single binding
Definition: std_expr.h:4249
or_exprt::or_exprt
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2297
nullary_exprt
An expression without operands.
Definition: std_expr.h:23
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
can_cast_expr< let_exprt >
bool can_cast_expr< let_exprt >(const exprt &base)
Definition: std_expr.h:4302
not_exprt::not_exprt
not_exprt(exprt _op)
Definition: std_expr.h:2874
can_cast_expr< bitnot_exprt >
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2381
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2202
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:3458
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1451
with_exprt::where
const exprt & where() const
Definition: std_expr.h:3104
with_exprt::old
exprt & old()
Definition: std_expr.h:3089
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:894
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2173
dynamic_object_exprt::get_instance
unsigned int get_instance() const
Definition: std_expr.cpp:46
address_of_exprt::address_of_exprt
address_of_exprt(exprt op, pointer_typet _type)
Definition: std_expr.h:2819
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4425
with_exprt::with_exprt
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:3081
xor_exprt::xor_exprt
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2339
rem_exprt::rem_exprt
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1153
notequal_exprt::notequal_exprt
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1256
bitxor_exprt
Bit-wise XOR.
Definition: std_expr.h:2452
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2416
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
let_exprt::value
const exprt & value() const
convenience accessor for the value of a single binding
Definition: std_expr.h:4257
dereference_exprt::pointer
const exprt & pointer() const
Definition: std_expr.h:2935
or_exprt
Boolean OR.
Definition: std_expr.h:2273
can_cast_expr< abs_exprt >
bool can_cast_expr< abs_exprt >(const exprt &base)
Definition: std_expr.h:342
array_exprt::type
array_typet & type()
Definition: std_expr.h:1456
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1131
complex_real_exprt::complex_real_exprt
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1759
member_exprt::struct_op
exprt & struct_op()
Definition: std_expr.h:3470
update_exprt::update_exprt
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:3265
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2168
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
class_method_descriptor_exprt::base_method_name
const irep_idt & base_method_name() const
The name of the method to which this expression is applied as would be seen in the source code.
Definition: std_expr.h:4589
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1017
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:4017
array_comprehension_exprt::array_comprehension_exprt
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:4453
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2852
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
member_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:3485
decorated_symbol_exprt::set_static_lifetime
void set_static_lifetime()
Definition: std_expr.h:134
struct_union_typet::componentt::get_name
const irep_idt & get_name() const
Definition: std_types.h:74
symbol_exprt::symbol_exprt
symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:91
to_replication_expr
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
Definition: std_expr.h:4073
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2095
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3475
ternary_exprt::ternary_exprt
ternary_exprt(const irep_idt &_id, exprt _op0, exprt _op1, exprt _op2, typet _type)
Definition: std_expr.h:58
predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:534
bitor_exprt::bitor_exprt
bitor_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2419
multi_ary_exprt::op1
const exprt & op1() const
Definition: std_expr.h:847
can_cast_expr< address_of_exprt >
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:2836
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:910
update_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3304
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3464
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2357
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:693
multi_ary_exprt::op1
exprt & op1()
Definition: std_expr.h:823
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
extractbits_exprt::lower
const exprt & lower() const
Definition: std_expr.h:2772
nullary_exprt::operands
operandst & operands()=delete
remove all operand methods
can_cast_expr< array_of_exprt >
bool can_cast_expr< array_of_exprt >(const exprt &base)
Definition: std_expr.h:1402
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
dereference_exprt::dereference_exprt
dereference_exprt(exprt op, typet type)
Definition: std_expr.h:2925
nil_exprt
The NIL expression.
Definition: std_expr.h:4001
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1372
nondet_symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:220
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2930
index_designatort::index
const exprt & index() const
Definition: std_expr.h:3166
conjunction
exprt conjunction(const exprt::operandst &)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
shl_exprt::shl_exprt
shl_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2592
decorated_symbol_exprt::is_thread_local
bool is_thread_local() const
Definition: std_expr.h:144
std_types.h
to_let_expr
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
Definition: std_expr.h:4318
can_cast_expr< bswap_exprt >
bool can_cast_expr< bswap_exprt >(const exprt &base)
Definition: std_expr.h:497
floatbv_typecast_exprt::floatbv_typecast_exprt
floatbv_typecast_exprt(exprt op, exprt rounding, typet _type)
Definition: std_expr.h:2098
can_cast_expr< notequal_exprt >
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1263
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:926
to_isfinite_expr
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:3653
isfinite_exprt::isfinite_exprt
isfinite_exprt(exprt op)
Definition: std_expr.h:3630
cond_exprt::add_case
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4398
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:1915
can_cast_expr< nil_exprt >
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:4011
extractbits_exprt::src
exprt & src()
Definition: std_expr.h:2747
can_cast_expr< ieee_float_op_exprt >
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: std_expr.h:3862
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:4485
member_exprt::compound
exprt & compound()
Definition: std_expr.h:3480
to_is_dynamic_object_expr
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: std_expr.h:2022
exprt::op1
exprt & op1()
Definition: expr.h:104
null_pointer_exprt::null_pointer_exprt
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:4020
dynamic_object_exprt::valid
const exprt & valid() const
Definition: std_expr.h:1963
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1279
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:991
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:4152
with_exprt::old
const exprt & old() const
Definition: std_expr.h:3094
isnan_exprt::isnan_exprt
isnan_exprt(exprt op)
Definition: std_expr.h:3540
concatenation_exprt::concatenation_exprt
concatenation_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4098
index_exprt::index
exprt & index()
Definition: std_expr.h:1325
nil_exprt::nil_exprt
nil_exprt()
Definition: std_expr.h:4004
to_unary_minus_expr
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
Definition: std_expr.h:408
is_dynamic_object_exprt::is_dynamic_object_exprt
is_dynamic_object_exprt(const exprt &op)
Definition: std_expr.h:2015
decorated_symbol_exprt::set_thread_local
void set_thread_local()
Definition: std_expr.h:149
mod_exprt::mod_exprt
mod_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1108
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(irep_idt identifier, typet type, source_locationt location)
Definition: std_expr.h:210
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:377
index_exprt::array
exprt & array()
Definition: std_expr.h:1315
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: std_expr.h:3880
ternary_exprt::op3
const exprt & op3() const =delete
extractbit_exprt::index
exprt & index()
Definition: std_expr.h:2673
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
binding_exprt::variables
const variablest & variables() const
Definition: std_expr.h:4176
member_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the member expression has the right number of operands, refers to a component that exists ...
Definition: std_expr.cpp:242
struct_exprt::struct_exprt
struct_exprt(operandst _operands, typet _type)
Definition: std_expr.h:1652
validation_modet
validation_modet
Definition: validation_mode.h:12
ieee_float_op_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:3855
irept::id
const irep_idt & id() const
Definition: irep.h:418
binary_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:613
let_exprt::binding
const binding_exprt & binding() const
Definition: std_expr.h:4227
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:93
binding_exprt
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:4149
popcount_exprt::popcount_exprt
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4344
can_cast_expr< div_exprt >
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1070
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1688
dstringt::empty
bool empty() const
Definition: dstring.h:88
abs_exprt
Absolute value.
Definition: std_expr.h:333
false_exprt
The Boolean constant false.
Definition: std_expr.h:3992
let_exprt::values
const operandst & values() const
Definition: std_expr.h:4269
vector_exprt::vector_exprt
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1545
unary_plus_exprt
The unary plus expression.
Definition: std_expr.h:426
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
Definition: std_expr.h:799
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2488
if_exprt::cond
const exprt & cond() const
Definition: std_expr.h:3015
to_dynamic_object_expr
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: std_expr.h:1986
object_descriptor_exprt::object
const exprt & object() const
Definition: std_expr.h:1880
let_exprt::let_exprt
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:4196
div_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1051
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
index_designatort
Definition: std_expr.h:3158
complex_exprt::imag
const exprt & imag() const
Definition: std_expr.h:1715
to_complex_imag_expr
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Definition: std_expr.h:1828
binary_predicate_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:701
to_bswap_expr
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
Definition: std_expr.h:515
to_ieee_float_notequal_expr
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
Definition: std_expr.h:3795
to_isinf_expr
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:3608
array_list_exprt::type
const array_typet & type() const
Definition: std_expr.h:1497
div_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1057
isinf_exprt::isinf_exprt
isinf_exprt(exprt op)
Definition: std_expr.h:3585
binary_relation_exprt::binary_relation_exprt
binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:727
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, exprt _op, typet _type)
Definition: std_expr.h:276
minus_exprt
Binary minus.
Definition: std_expr.h:945
div_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1045
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3141
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3262
nullary_exprt::op0
const exprt & op0() const =delete
can_cast_expr< extractbit_exprt >
bool can_cast_expr< extractbit_exprt >(const exprt &base)
Definition: std_expr.h:2690
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:3289
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt(exprt _object)
Definition: std_expr.h:1860
binary_exprt::validate
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:623
multi_ary_exprt::op0
const exprt & op0() const
Definition: std_expr.h:841
source_locationt
Definition: source_location.h:19
unary_plus_exprt::unary_plus_exprt
unary_plus_exprt(exprt op)
Definition: std_expr.h:429
can_cast_expr< replication_exprt >
bool can_cast_expr< replication_exprt >(const exprt &base)
Definition: std_expr.h:4057
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2321
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1337
unary_exprt::unary_exprt
unary_exprt(const irep_idt &_id, const exprt &_op)
Definition: std_expr.h:271
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1587
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2372
to_isnan_expr
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:3563
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2657
to_bitxor_expr
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2473
sign_exprt::sign_exprt
sign_exprt(exprt _op)
Definition: std_expr.h:559
unary_minus_exprt::unary_minus_exprt
unary_minus_exprt(exprt _op)
Definition: std_expr.h:385
to_bitor_expr
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
Definition: std_expr.h:2437
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3433
struct_union_typet::componentt
Definition: std_types.h:63
can_cast_expr< binary_relation_exprt >
bool can_cast_expr< binary_relation_exprt >(const exprt &base)
Definition: std_expr.h:758
extractbit_exprt::extractbit_exprt
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
Definition: std_expr.h:2661
equal_exprt::equal_exprt
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1198
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2973
decorated_symbol_exprt
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_l...
Definition: std_expr.h:119
shift_exprt
A base class for shift operators.
Definition: std_expr.h:2524
dynamic_object_exprt::set_instance
void set_instance(unsigned int instance)
Definition: std_expr.cpp:41
can_cast_expr< complex_real_exprt >
bool can_cast_expr< complex_real_exprt >(const exprt &base)
Definition: std_expr.h:1766
type_exprt
An expression denoting a type.
Definition: std_expr.h:3898
can_cast_expr< array_comprehension_exprt >
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:4497
plus_exprt::plus_exprt
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:903
cond_exprt
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4387
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:3850
equal_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1203
infinity_exprt::infinity_exprt
infinity_exprt(typet _type)
Definition: std_expr.h:4142
binding_exprt::binding_exprt
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:4155
dynamic_object_exprt::valid
exprt & valid()
Definition: std_expr.h:1958
array_typet
Arrays with given size.
Definition: std_types.h:964
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
object_descriptor_exprt::offset
const exprt & offset() const
Definition: std_expr.h:1892
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3020
binding_exprt::where
exprt & where()
Definition: std_expr.h:4181
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:74
can_cast_expr< or_exprt >
bool can_cast_expr< or_exprt >(const exprt &base)
Definition: std_expr.h:2310
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:2795
nullary_exprt::copy_to_operands
void copy_to_operands(const exprt &expr)=delete
decorated_symbol_exprt::decorated_symbol_exprt
decorated_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:124
floatbv_typecast_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:2117
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2733
bitand_exprt::bitand_exprt
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2491
to_sign_expr
const sign_exprt & to_sign_expr(const exprt &expr)
Cast an exprt to a sign_exprt.
Definition: std_expr.h:582
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2897
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2544
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
can_cast_expr< class_method_descriptor_exprt >
bool can_cast_expr< class_method_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:4637
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3582
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2145
to_class_method_descriptor_expr
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition: std_expr.h:4627
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
update_exprt::new_value
exprt & new_value()
Definition: std_expr.h:3299
replication_exprt::replication_exprt
replication_exprt(const constant_exprt &_times, const exprt &_src)
Definition: std_expr.h:4030
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2254
ieee_float_op_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:3835
member_exprt::member_exprt
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:3442
unary_exprt::op2
const exprt & op2() const =delete
can_cast_expr< type_exprt >
bool can_cast_expr< type_exprt >(const exprt &base)
Definition: std_expr.h:3907
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
extractbit_exprt::src
exprt & src()
Definition: std_expr.h:2668
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2076
can_cast_expr< popcount_exprt >
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4351
ashr_exprt
Arithmetic right shift.
Definition: std_expr.h:2627
if_exprt::false_case
const exprt & false_case() const
Definition: std_expr.h:3035
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2650
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3010
floatbv_typecast_exprt::op
const exprt & op() const
Definition: std_expr.h:2112
binary_exprt::binary_exprt
binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:608
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:724
typecast_exprt::typecast_exprt
typecast_exprt(exprt op, typet _type)
Definition: std_expr.h:2044
extractbit_exprt::index
const exprt & index() const
Definition: std_expr.h:2683
expr_cast.h
Templated functions to cast to specific exprt-derived classes.
nullary_exprt::op1
const exprt & op1() const =delete
complex_imag_exprt
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1801
ieee_float_op_exprt::lhs
exprt & lhs()
Definition: std_expr.h:3830
can_cast_expr< shift_exprt >
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: std_expr.h:2556
can_cast_expr< nondet_symbol_exprt >
bool can_cast_expr< nondet_symbol_exprt >(const exprt &base)
Definition: std_expr.h:232
nullary_exprt::nullary_exprt
nullary_exprt(const irep_idt &_id, typet _type)
Definition: std_expr.h:26
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1236
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:155
binary_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:636
binary_exprt::binary_exprt
binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:603
decorated_symbol_exprt::clear_thread_local
void clear_thread_local()
Definition: std_expr.h:154
can_cast_expr< isnormal_exprt >
bool can_cast_expr< isnormal_exprt >(const exprt &base)
Definition: std_expr.h:3682
bswap_exprt::set_bits_per_byte
void set_bits_per_byte(std::size_t bits_per_byte)
Definition: std_expr.h:490
array_comprehension_exprt::body
exprt & body()
Definition: std_expr.h:4490
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2397
class_method_descriptor_exprt::class_id
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition: std_expr.h:4582
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:3818
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2281
unary_exprt::op
exprt & op()
Definition: std_expr.h:286
multi_ary_exprt::op2
const exprt & op2() const
Definition: std_expr.h:853
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3518
concatenation_exprt::concatenation_exprt
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: std_expr.h:4103
can_cast_expr< object_descriptor_exprt >
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:1899
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2060
bswap_exprt
The byte swap expression.
Definition: std_expr.h:470
shift_exprt::distance
const exprt & distance() const
Definition: std_expr.h:2549
can_cast_expr< vector_exprt >
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1552
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3448
complex_exprt::complex_exprt
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1691
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
implies_exprt
Boolean implication.
Definition: std_expr.h:2228
let_exprt::where
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:4293
shift_exprt::op
const exprt & op() const
Definition: std_expr.h:2539
can_cast_expr< if_exprt >
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3042
array_of_exprt::what
const exprt & what() const
Definition: std_expr.h:1395
struct_exprt::component
exprt & component(const irep_idt &name, const namespacet &ns)
Definition: std_expr.cpp:206
array_list_exprt
Array constructor from a list of index-element pairs Operands are index/value pairs,...
Definition: std_expr.h:1489
constant_exprt::constant_exprt
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:3937
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2725
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:3957
exprt::operands
operandst & operands()
Definition: expr.h:95
decorated_symbol_exprt::is_static_lifetime
bool is_static_lifetime() const
Definition: std_expr.h:129
can_cast_expr< complex_exprt >
bool can_cast_expr< complex_exprt >(const exprt &base)
Definition: std_expr.h:1722
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2276
let_exprt::values
operandst & values()
Definition: std_expr.h:4264
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2635
false_exprt::false_exprt
false_exprt()
Definition: std_expr.h:3995
nullary_exprt::op2
const exprt & op2() const =delete
ieee_float_op_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:3845
index_exprt
Array index operator.
Definition: std_expr.h:1298
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2814
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:257
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4336
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt()
Definition: std_expr.h:1851
address_of_exprt::object
const exprt & object() const
Definition: std_expr.h:2829
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2041
can_cast_expr< unary_plus_exprt >
bool can_cast_expr< unary_plus_exprt >(const exprt &base)
Definition: std_expr.h:436
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1487
unary_predicate_exprt::unary_predicate_exprt
unary_predicate_exprt(const irep_idt &_id, exprt _op)
Definition: std_expr.h:548
binary_predicate_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:708
complex_imag_exprt::complex_imag_exprt
complex_imag_exprt(const exprt &op)
Definition: std_expr.h:1804
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4450
replication_exprt::times
const constant_exprt & times() const
Definition: std_expr.h:4040
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1875
true_exprt
The Boolean constant true.
Definition: std_expr.h:3983
constant_exprt
A constant literal expression.
Definition: std_expr.h:3934
can_cast_expr< extractbits_exprt >
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:2779
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3717
binary_exprt::op2
const exprt & op2() const =delete
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:817
unary_exprt::op3
const exprt & op3() const =delete
implies_exprt::implies_exprt
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2231
index_designatort::index
exprt & index()
Definition: std_expr.h:3171
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1662
bswap_exprt::bswap_exprt
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
Definition: std_expr.h:473
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:872
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:4287
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:4222
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:805
union_exprt::set_component_number
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1602
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
constant_exprt::set_value
void set_value(const irep_idt &value)
Definition: std_expr.h:3948
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3943
let_exprt::symbol
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:4241
with_exprt::where
exprt & where()
Definition: std_expr.h:3099
array_of_exprt::array_of_exprt
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1375
to_member_designator
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3243
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1437
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3121
ieee_float_op_exprt::rhs
exprt & rhs()
Definition: std_expr.h:3840
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3672
member_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3453
unary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:545
popcount_exprt::popcount_exprt
popcount_exprt(exprt _op, typet _type)
Definition: std_expr.h:4339
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
bitnot_exprt::bitnot_exprt
bitnot_exprt(exprt op)
Definition: std_expr.h:2375
with_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3114
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:2706
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2609
as_const.h
extractbit_exprt::src
const exprt & src() const
Definition: std_expr.h:2678
let_exprt
A let expression.
Definition: std_expr.h:4193
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2213
ieee_float_op_exprt::ieee_float_op_exprt
ieee_float_op_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs, exprt _rm)
Definition: std_expr.h:3821
div_exprt::divisor
const exprt & divisor() const
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1063
complex_exprt::real
exprt real()
Definition: std_expr.h:1700
expr_protectedt
Base class for all expressions.
Definition: expr.h:364
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1673
validation_modet::INVARIANT
can_cast_expr< member_designatort >
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3227
to_abs_expr
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
Definition: std_expr.h:358
mod_exprt
Modulo.
Definition: std_expr.h:1105
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2940
can_cast_expr< update_exprt >
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3311
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3194
shl_exprt
Left shift.
Definition: std_expr.h:2589
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:2957
can_cast_expr< ieee_float_equal_exprt >
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:3730
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3537
can_cast_expr< dynamic_object_exprt >
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:1970
can_cast_expr< mult_exprt >
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:1001
not_exprt
Boolean negation.
Definition: std_expr.h:2871
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3968
nondet_symbol_exprt::nondet_symbol_exprt
nondet_symbol_exprt(const irep_idt &identifier, typet type)
Definition: std_expr.h:201
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1887
multi_ary_exprt::op3
const exprt & op3() const
Definition: std_expr.h:859