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  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
794  : expr_protectedt(_id, std::move(_type))
795  {
796  operands() = std::move(_operands);
797  }
798 
799  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
800  : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
801  {
802  }
803 
804  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
805  : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
806  {
807  }
808 
809  // In contrast to exprt::opX, the methods
810  // below check the size.
812  {
813  PRECONDITION(operands().size() >= 1);
814  return operands().front();
815  }
816 
818  {
819  PRECONDITION(operands().size() >= 2);
820  return operands()[1];
821  }
822 
824  {
825  PRECONDITION(operands().size() >= 3);
826  return operands()[2];
827  }
828 
830  {
831  PRECONDITION(operands().size() >= 4);
832  return operands()[3];
833  }
834 
835  const exprt &op0() const
836  {
837  PRECONDITION(operands().size() >= 1);
838  return operands().front();
839  }
840 
841  const exprt &op1() const
842  {
843  PRECONDITION(operands().size() >= 2);
844  return operands()[1];
845  }
846 
847  const exprt &op2() const
848  {
849  PRECONDITION(operands().size() >= 3);
850  return operands()[2];
851  }
852 
853  const exprt &op3() const
854  {
855  PRECONDITION(operands().size() >= 4);
856  return operands()[3];
857  }
858 };
859 
866 inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
867 {
868  return static_cast<const multi_ary_exprt &>(expr);
869 }
870 
873 {
874  return static_cast<multi_ary_exprt &>(expr);
875 }
876 
877 
881 {
882 public:
883  plus_exprt(exprt _lhs, exprt _rhs)
884  : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
885  {
886  }
887 
888  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
889  : multi_ary_exprt(
890  std::move(_lhs),
891  ID_plus,
892  std::move(_rhs),
893  std::move(_type))
894  {
895  }
896 
897  plus_exprt(operandst _operands, typet _type)
898  : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
899  {
900  }
901 };
902 
903 template <>
904 inline bool can_cast_expr<plus_exprt>(const exprt &base)
905 {
906  return base.id() == ID_plus;
907 }
908 
909 inline void validate_expr(const plus_exprt &value)
910 {
911  validate_operands(value, 2, "Plus must have two or more operands", true);
912 }
913 
920 inline const plus_exprt &to_plus_expr(const exprt &expr)
921 {
922  PRECONDITION(expr.id()==ID_plus);
923  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
924  validate_expr(ret);
925  return ret;
926 }
927 
930 {
931  PRECONDITION(expr.id()==ID_plus);
932  plus_exprt &ret = static_cast<plus_exprt &>(expr);
933  validate_expr(ret);
934  return ret;
935 }
936 
937 
940 {
941 public:
942  minus_exprt(exprt _lhs, exprt _rhs)
943  : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
944  {
945  }
946 };
947 
948 template <>
949 inline bool can_cast_expr<minus_exprt>(const exprt &base)
950 {
951  return base.id() == ID_minus;
952 }
953 
954 inline void validate_expr(const minus_exprt &value)
955 {
956  validate_operands(value, 2, "Minus must have two or more operands", true);
957 }
958 
965 inline const minus_exprt &to_minus_expr(const exprt &expr)
966 {
967  PRECONDITION(expr.id()==ID_minus);
968  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
969  validate_expr(ret);
970  return ret;
971 }
972 
975 {
976  PRECONDITION(expr.id()==ID_minus);
977  minus_exprt &ret = static_cast<minus_exprt &>(expr);
978  validate_expr(ret);
979  return ret;
980 }
981 
982 
986 {
987 public:
988  mult_exprt(exprt _lhs, exprt _rhs)
989  : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
990  {
991  }
992 };
993 
994 template <>
995 inline bool can_cast_expr<mult_exprt>(const exprt &base)
996 {
997  return base.id() == ID_mult;
998 }
999 
1000 inline void validate_expr(const mult_exprt &value)
1001 {
1002  validate_operands(value, 2, "Multiply must have two or more operands", true);
1003 }
1004 
1011 inline const mult_exprt &to_mult_expr(const exprt &expr)
1012 {
1013  PRECONDITION(expr.id()==ID_mult);
1014  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
1015  validate_expr(ret);
1016  return ret;
1017 }
1018 
1021 {
1022  PRECONDITION(expr.id()==ID_mult);
1023  mult_exprt &ret = static_cast<mult_exprt &>(expr);
1024  validate_expr(ret);
1025  return ret;
1026 }
1027 
1028 
1031 {
1032 public:
1033  div_exprt(exprt _lhs, exprt _rhs)
1034  : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
1035  {
1036  }
1037 
1040  {
1041  return op0();
1042  }
1043 
1045  const exprt &dividend() const
1046  {
1047  return op0();
1048  }
1049 
1052  {
1053  return op1();
1054  }
1055 
1057  const exprt &divisor() const
1058  {
1059  return op1();
1060  }
1061 };
1062 
1063 template <>
1064 inline bool can_cast_expr<div_exprt>(const exprt &base)
1065 {
1066  return base.id() == ID_div;
1067 }
1068 
1069 inline void validate_expr(const div_exprt &value)
1070 {
1071  validate_operands(value, 2, "Divide must have two operands");
1072 }
1073 
1080 inline const div_exprt &to_div_expr(const exprt &expr)
1081 {
1082  PRECONDITION(expr.id()==ID_div);
1083  const div_exprt &ret = static_cast<const div_exprt &>(expr);
1084  validate_expr(ret);
1085  return ret;
1086 }
1087 
1090 {
1091  PRECONDITION(expr.id()==ID_div);
1092  div_exprt &ret = static_cast<div_exprt &>(expr);
1093  validate_expr(ret);
1094  return ret;
1095 }
1096 
1097 
1100 {
1101 public:
1102  mod_exprt(exprt _lhs, exprt _rhs)
1103  : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
1104  {
1105  }
1106 };
1107 
1108 template <>
1109 inline bool can_cast_expr<mod_exprt>(const exprt &base)
1110 {
1111  return base.id() == ID_mod;
1112 }
1113 
1114 inline void validate_expr(const mod_exprt &value)
1115 {
1116  validate_operands(value, 2, "Modulo must have two operands");
1117 }
1118 
1125 inline const mod_exprt &to_mod_expr(const exprt &expr)
1126 {
1127  PRECONDITION(expr.id()==ID_mod);
1128  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
1129  validate_expr(ret);
1130  return ret;
1131 }
1132 
1135 {
1136  PRECONDITION(expr.id()==ID_mod);
1137  mod_exprt &ret = static_cast<mod_exprt &>(expr);
1138  validate_expr(ret);
1139  return ret;
1140 }
1141 
1142 
1145 {
1146 public:
1147  rem_exprt(exprt _lhs, exprt _rhs)
1148  : binary_exprt(std::move(_lhs), ID_rem, std::move(_rhs))
1149  {
1150  }
1151 };
1152 
1153 template <>
1154 inline bool can_cast_expr<rem_exprt>(const exprt &base)
1155 {
1156  return base.id() == ID_rem;
1157 }
1158 
1159 inline void validate_expr(const rem_exprt &value)
1160 {
1161  validate_operands(value, 2, "Remainder must have two operands");
1162 }
1163 
1170 inline const rem_exprt &to_rem_expr(const exprt &expr)
1171 {
1172  PRECONDITION(expr.id()==ID_rem);
1173  const rem_exprt &ret = static_cast<const rem_exprt &>(expr);
1174  validate_expr(ret);
1175  return ret;
1176 }
1177 
1180 {
1181  PRECONDITION(expr.id()==ID_rem);
1182  rem_exprt &ret = static_cast<rem_exprt &>(expr);
1183  validate_expr(ret);
1184  return ret;
1185 }
1186 
1187 
1190 {
1191 public:
1193  : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
1194  {
1195  }
1196 
1197  static void check(
1198  const exprt &expr,
1200  {
1201  binary_relation_exprt::check(expr, vm);
1202  }
1203 
1204  static void validate(
1205  const exprt &expr,
1206  const namespacet &ns,
1208  {
1209  binary_relation_exprt::validate(expr, ns, vm);
1210  }
1211 };
1212 
1213 template <>
1214 inline bool can_cast_expr<equal_exprt>(const exprt &base)
1215 {
1216  return base.id() == ID_equal;
1217 }
1218 
1219 inline void validate_expr(const equal_exprt &value)
1220 {
1221  equal_exprt::check(value);
1222 }
1223 
1230 inline const equal_exprt &to_equal_expr(const exprt &expr)
1231 {
1232  PRECONDITION(expr.id()==ID_equal);
1233  equal_exprt::check(expr);
1234  return static_cast<const equal_exprt &>(expr);
1235 }
1236 
1239 {
1240  PRECONDITION(expr.id()==ID_equal);
1241  equal_exprt::check(expr);
1242  return static_cast<equal_exprt &>(expr);
1243 }
1244 
1245 
1248 {
1249 public:
1251  : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
1252  {
1253  }
1254 };
1255 
1256 template <>
1257 inline bool can_cast_expr<notequal_exprt>(const exprt &base)
1258 {
1259  return base.id() == ID_notequal;
1260 }
1261 
1262 inline void validate_expr(const notequal_exprt &value)
1263 {
1264  validate_operands(value, 2, "Inequality must have two operands");
1265 }
1266 
1273 inline const notequal_exprt &to_notequal_expr(const exprt &expr)
1274 {
1275  PRECONDITION(expr.id()==ID_notequal);
1276  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
1277  validate_expr(ret);
1278  return ret;
1279 }
1280 
1283 {
1284  PRECONDITION(expr.id()==ID_notequal);
1285  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
1286  validate_expr(ret);
1287  return ret;
1288 }
1289 
1290 
1293 {
1294 public:
1295  index_exprt(const exprt &_array, exprt _index)
1296  : binary_exprt(_array, ID_index, std::move(_index), _array.type().subtype())
1297  {
1298  }
1299 
1300  index_exprt(exprt _array, exprt _index, typet _type)
1301  : binary_exprt(
1302  std::move(_array),
1303  ID_index,
1304  std::move(_index),
1305  std::move(_type))
1306  {
1307  }
1308 
1310  {
1311  return op0();
1312  }
1313 
1314  const exprt &array() const
1315  {
1316  return op0();
1317  }
1318 
1320  {
1321  return op1();
1322  }
1323 
1324  const exprt &index() const
1325  {
1326  return op1();
1327  }
1328 };
1329 
1330 template <>
1331 inline bool can_cast_expr<index_exprt>(const exprt &base)
1332 {
1333  return base.id() == ID_index;
1334 }
1335 
1336 inline void validate_expr(const index_exprt &value)
1337 {
1338  validate_operands(value, 2, "Array index must have two operands");
1339 }
1340 
1347 inline const index_exprt &to_index_expr(const exprt &expr)
1348 {
1349  PRECONDITION(expr.id()==ID_index);
1350  const index_exprt &ret = static_cast<const index_exprt &>(expr);
1351  validate_expr(ret);
1352  return ret;
1353 }
1354 
1357 {
1358  PRECONDITION(expr.id()==ID_index);
1359  index_exprt &ret = static_cast<index_exprt &>(expr);
1360  validate_expr(ret);
1361  return ret;
1362 }
1363 
1364 
1367 {
1368 public:
1369  explicit array_of_exprt(exprt _what, array_typet _type)
1370  : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
1371  {
1372  }
1373 
1374  const array_typet &type() const
1375  {
1376  return static_cast<const array_typet &>(unary_exprt::type());
1377  }
1378 
1380  {
1381  return static_cast<array_typet &>(unary_exprt::type());
1382  }
1383 
1385  {
1386  return op0();
1387  }
1388 
1389  const exprt &what() const
1390  {
1391  return op0();
1392  }
1393 };
1394 
1395 template <>
1396 inline bool can_cast_expr<array_of_exprt>(const exprt &base)
1397 {
1398  return base.id() == ID_array_of;
1399 }
1400 
1401 inline void validate_expr(const array_of_exprt &value)
1402 {
1403  validate_operands(value, 1, "'Array of' must have one operand");
1404 }
1405 
1412 inline const array_of_exprt &to_array_of_expr(const exprt &expr)
1413 {
1414  PRECONDITION(expr.id()==ID_array_of);
1415  const array_of_exprt &ret = static_cast<const array_of_exprt &>(expr);
1416  validate_expr(ret);
1417  return ret;
1418 }
1419 
1422 {
1423  PRECONDITION(expr.id()==ID_array_of);
1424  array_of_exprt &ret = static_cast<array_of_exprt &>(expr);
1425  validate_expr(ret);
1426  return ret;
1427 }
1428 
1429 
1432 {
1433 public:
1435  : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
1436  {
1437  }
1438 
1439  const array_typet &type() const
1440  {
1441  return static_cast<const array_typet &>(multi_ary_exprt::type());
1442  }
1443 
1445  {
1446  return static_cast<array_typet &>(multi_ary_exprt::type());
1447  }
1448 };
1449 
1450 template <>
1451 inline bool can_cast_expr<array_exprt>(const exprt &base)
1452 {
1453  return base.id() == ID_array;
1454 }
1455 
1462 inline const array_exprt &to_array_expr(const exprt &expr)
1463 {
1464  PRECONDITION(expr.id()==ID_array);
1465  return static_cast<const array_exprt &>(expr);
1466 }
1467 
1470 {
1471  PRECONDITION(expr.id()==ID_array);
1472  return static_cast<array_exprt &>(expr);
1473 }
1474 
1478 {
1479 public:
1481  : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
1482  {
1483  }
1484 
1485  const array_typet &type() const
1486  {
1487  return static_cast<const array_typet &>(multi_ary_exprt::type());
1488  }
1489 
1491  {
1492  return static_cast<array_typet &>(multi_ary_exprt::type());
1493  }
1494 
1496  void add(exprt index, exprt value)
1497  {
1498  add_to_operands(std::move(index), std::move(value));
1499  }
1500 };
1501 
1502 template <>
1503 inline bool can_cast_expr<array_list_exprt>(const exprt &base)
1504 {
1505  return base.id() == ID_array_list;
1506 }
1507 
1508 inline void validate_expr(const array_list_exprt &value)
1509 {
1510  PRECONDITION(value.operands().size() % 2 == 0);
1511 }
1512 
1513 inline const array_list_exprt &to_array_list_expr(const exprt &expr)
1514 {
1516  auto &ret = static_cast<const array_list_exprt &>(expr);
1517  validate_expr(ret);
1518  return ret;
1519 }
1520 
1522 {
1524  auto &ret = static_cast<array_list_exprt &>(expr);
1525  validate_expr(ret);
1526  return ret;
1527 }
1528 
1531 {
1532 public:
1534  : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
1535  {
1536  }
1537 };
1538 
1539 template <>
1540 inline bool can_cast_expr<vector_exprt>(const exprt &base)
1541 {
1542  return base.id() == ID_vector;
1543 }
1544 
1551 inline const vector_exprt &to_vector_expr(const exprt &expr)
1552 {
1553  PRECONDITION(expr.id()==ID_vector);
1554  return static_cast<const vector_exprt &>(expr);
1555 }
1556 
1559 {
1560  PRECONDITION(expr.id()==ID_vector);
1561  return static_cast<vector_exprt &>(expr);
1562 }
1563 
1564 
1567 {
1568 public:
1569  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
1570  : unary_exprt(ID_union, std::move(_value), std::move(_type))
1571  {
1572  set_component_name(_component_name);
1573  }
1574 
1576  {
1577  return get(ID_component_name);
1578  }
1579 
1580  void set_component_name(const irep_idt &component_name)
1581  {
1582  set(ID_component_name, component_name);
1583  }
1584 
1585  std::size_t get_component_number() const
1586  {
1587  return get_size_t(ID_component_number);
1588  }
1589 
1590  void set_component_number(std::size_t component_number)
1591  {
1592  set(ID_component_number, narrow_cast<long long>(component_number));
1593  }
1594 };
1595 
1596 template <>
1597 inline bool can_cast_expr<union_exprt>(const exprt &base)
1598 {
1599  return base.id() == ID_union;
1600 }
1601 
1602 inline void validate_expr(const union_exprt &value)
1603 {
1604  validate_operands(value, 1, "Union constructor must have one operand");
1605 }
1606 
1613 inline const union_exprt &to_union_expr(const exprt &expr)
1614 {
1615  PRECONDITION(expr.id()==ID_union);
1616  const union_exprt &ret = static_cast<const union_exprt &>(expr);
1617  validate_expr(ret);
1618  return ret;
1619 }
1620 
1623 {
1624  PRECONDITION(expr.id()==ID_union);
1625  union_exprt &ret = static_cast<union_exprt &>(expr);
1626  validate_expr(ret);
1627  return ret;
1628 }
1629 
1630 
1633 {
1634 public:
1635  struct_exprt(operandst _operands, typet _type)
1636  : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
1637  {
1638  }
1639 
1640  exprt &component(const irep_idt &name, const namespacet &ns);
1641  const exprt &component(const irep_idt &name, const namespacet &ns) const;
1642 };
1643 
1644 template <>
1645 inline bool can_cast_expr<struct_exprt>(const exprt &base)
1646 {
1647  return base.id() == ID_struct;
1648 }
1649 
1656 inline const struct_exprt &to_struct_expr(const exprt &expr)
1657 {
1658  PRECONDITION(expr.id()==ID_struct);
1659  return static_cast<const struct_exprt &>(expr);
1660 }
1661 
1664 {
1665  PRECONDITION(expr.id()==ID_struct);
1666  return static_cast<struct_exprt &>(expr);
1667 }
1668 
1669 
1672 {
1673 public:
1675  : binary_exprt(
1676  std::move(_real),
1677  ID_complex,
1678  std::move(_imag),
1679  std::move(_type))
1680  {
1681  }
1682 
1684  {
1685  return op0();
1686  }
1687 
1688  const exprt &real() const
1689  {
1690  return op0();
1691  }
1692 
1694  {
1695  return op1();
1696  }
1697 
1698  const exprt &imag() const
1699  {
1700  return op1();
1701  }
1702 };
1703 
1704 template <>
1705 inline bool can_cast_expr<complex_exprt>(const exprt &base)
1706 {
1707  return base.id() == ID_complex;
1708 }
1709 
1710 inline void validate_expr(const complex_exprt &value)
1711 {
1712  validate_operands(value, 2, "Complex constructor must have two operands");
1713 }
1714 
1721 inline const complex_exprt &to_complex_expr(const exprt &expr)
1722 {
1723  PRECONDITION(expr.id()==ID_complex);
1724  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
1725  validate_expr(ret);
1726  return ret;
1727 }
1728 
1731 {
1732  PRECONDITION(expr.id()==ID_complex);
1733  complex_exprt &ret = static_cast<complex_exprt &>(expr);
1734  validate_expr(ret);
1735  return ret;
1736 }
1737 
1740 {
1741 public:
1742  explicit complex_real_exprt(const exprt &op)
1743  : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
1744  {
1745  }
1746 };
1747 
1748 template <>
1750 {
1751  return base.id() == ID_complex_real;
1752 }
1753 
1754 inline void validate_expr(const complex_real_exprt &expr)
1755 {
1757  expr, 1, "real part retrieval operation must have one operand");
1758 }
1759 
1767 {
1768  PRECONDITION(expr.id() == ID_complex_real);
1769  const complex_real_exprt &ret = static_cast<const complex_real_exprt &>(expr);
1770  validate_expr(ret);
1771  return ret;
1772 }
1773 
1776 {
1777  PRECONDITION(expr.id() == ID_complex_real);
1778  complex_real_exprt &ret = static_cast<complex_real_exprt &>(expr);
1779  validate_expr(ret);
1780  return ret;
1781 }
1782 
1785 {
1786 public:
1787  explicit complex_imag_exprt(const exprt &op)
1788  : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
1789  {
1790  }
1791 };
1792 
1793 template <>
1795 {
1796  return base.id() == ID_complex_imag;
1797 }
1798 
1799 inline void validate_expr(const complex_imag_exprt &expr)
1800 {
1802  expr, 1, "imaginary part retrieval operation must have one operand");
1803 }
1804 
1812 {
1813  PRECONDITION(expr.id() == ID_complex_imag);
1814  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
1815  validate_expr(ret);
1816  return ret;
1817 }
1818 
1821 {
1822  PRECONDITION(expr.id() == ID_complex_imag);
1823  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
1824  validate_expr(ret);
1825  return ret;
1826 }
1827 
1828 class namespacet;
1829 
1832 {
1833 public:
1835  : binary_exprt(
1836  exprt(ID_unknown),
1837  ID_object_descriptor,
1838  exprt(ID_unknown),
1839  typet())
1840  {
1841  }
1842 
1843  explicit object_descriptor_exprt(exprt _object)
1844  : binary_exprt(
1845  std::move(_object),
1846  ID_object_descriptor,
1847  exprt(ID_unknown),
1848  typet())
1849  {
1850  }
1851 
1856  void build(const exprt &expr, const namespacet &ns);
1857 
1859  {
1860  return op0();
1861  }
1862 
1863  const exprt &object() const
1864  {
1865  return op0();
1866  }
1867 
1868  const exprt &root_object() const;
1869 
1871  {
1872  return op1();
1873  }
1874 
1875  const exprt &offset() const
1876  {
1877  return op1();
1878  }
1879 };
1880 
1881 template <>
1883 {
1884  return base.id() == ID_object_descriptor;
1885 }
1886 
1887 inline void validate_expr(const object_descriptor_exprt &value)
1888 {
1889  validate_operands(value, 2, "Object descriptor must have two operands");
1890 }
1891 
1899  const exprt &expr)
1900 {
1901  PRECONDITION(expr.id()==ID_object_descriptor);
1902  const object_descriptor_exprt &ret =
1903  static_cast<const object_descriptor_exprt &>(expr);
1904  validate_expr(ret);
1905  return ret;
1906 }
1907 
1910 {
1911  PRECONDITION(expr.id()==ID_object_descriptor);
1912  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
1913  validate_expr(ret);
1914  return ret;
1915 }
1916 
1917 
1920 {
1921 public:
1923  : binary_exprt(
1924  exprt(ID_unknown),
1925  ID_dynamic_object,
1926  exprt(ID_unknown),
1927  std::move(type))
1928  {
1929  }
1930 
1931  void set_instance(unsigned int instance);
1932 
1933  unsigned int get_instance() const;
1934 
1936  {
1937  return op1();
1938  }
1939 
1940  const exprt &valid() const
1941  {
1942  return op1();
1943  }
1944 };
1945 
1946 template <>
1948 {
1949  return base.id() == ID_dynamic_object;
1950 }
1951 
1952 inline void validate_expr(const dynamic_object_exprt &value)
1953 {
1954  validate_operands(value, 2, "Dynamic object must have two operands");
1955 }
1956 
1964  const exprt &expr)
1965 {
1966  PRECONDITION(expr.id()==ID_dynamic_object);
1967  const dynamic_object_exprt &ret =
1968  static_cast<const dynamic_object_exprt &>(expr);
1969  validate_expr(ret);
1970  return ret;
1971 }
1972 
1975 {
1976  PRECONDITION(expr.id()==ID_dynamic_object);
1977  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
1978  validate_expr(ret);
1979  return ret;
1980 }
1981 
1984 {
1985 public:
1987  : unary_predicate_exprt(ID_is_dynamic_object, op)
1988  {
1989  }
1990 };
1991 
1992 inline const is_dynamic_object_exprt &
1994 {
1995  PRECONDITION(expr.id() == ID_is_dynamic_object);
1997  expr.operands().size() == 1, "is_dynamic_object must have one operand");
1998  return static_cast<const is_dynamic_object_exprt &>(expr);
1999 }
2000 
2004 {
2005  PRECONDITION(expr.id() == ID_is_dynamic_object);
2007  expr.operands().size() == 1, "is_dynamic_object must have one operand");
2008  return static_cast<is_dynamic_object_exprt &>(expr);
2009 }
2010 
2013 {
2014 public:
2016  : unary_exprt(ID_typecast, std::move(op), std::move(_type))
2017  {
2018  }
2019 
2020  // returns a typecast if the type doesn't already match
2021  static exprt conditional_cast(const exprt &expr, const typet &type)
2022  {
2023  if(expr.type() == type)
2024  return expr;
2025  else
2026  return typecast_exprt(expr, type);
2027  }
2028 };
2029 
2030 template <>
2031 inline bool can_cast_expr<typecast_exprt>(const exprt &base)
2032 {
2033  return base.id() == ID_typecast;
2034 }
2035 
2036 inline void validate_expr(const typecast_exprt &value)
2037 {
2038  validate_operands(value, 1, "Typecast must have one operand");
2039 }
2040 
2047 inline const typecast_exprt &to_typecast_expr(const exprt &expr)
2048 {
2049  PRECONDITION(expr.id()==ID_typecast);
2050  const typecast_exprt &ret = static_cast<const typecast_exprt &>(expr);
2051  validate_expr(ret);
2052  return ret;
2053 }
2054 
2057 {
2058  PRECONDITION(expr.id()==ID_typecast);
2059  typecast_exprt &ret = static_cast<typecast_exprt &>(expr);
2060  validate_expr(ret);
2061  return ret;
2062 }
2063 
2064 
2067 {
2068 public:
2070  : binary_exprt(
2071  std::move(op),
2072  ID_floatbv_typecast,
2073  std::move(rounding),
2074  std::move(_type))
2075  {
2076  }
2077 
2079  {
2080  return op0();
2081  }
2082 
2083  const exprt &op() const
2084  {
2085  return op0();
2086  }
2087 
2089  {
2090  return op1();
2091  }
2092 
2093  const exprt &rounding_mode() const
2094  {
2095  return op1();
2096  }
2097 };
2098 
2099 template <>
2101 {
2102  return base.id() == ID_floatbv_typecast;
2103 }
2104 
2105 inline void validate_expr(const floatbv_typecast_exprt &value)
2106 {
2107  validate_operands(value, 2, "Float typecast must have two operands");
2108 }
2109 
2117 {
2118  PRECONDITION(expr.id()==ID_floatbv_typecast);
2119  const floatbv_typecast_exprt &ret =
2120  static_cast<const floatbv_typecast_exprt &>(expr);
2121  validate_expr(ret);
2122  return ret;
2123 }
2124 
2127 {
2128  PRECONDITION(expr.id()==ID_floatbv_typecast);
2129  floatbv_typecast_exprt &ret = static_cast<floatbv_typecast_exprt &>(expr);
2130  validate_expr(ret);
2131  return ret;
2132 }
2133 
2134 
2137 {
2138 public:
2140  : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
2141  {
2142  }
2143 
2145  : multi_ary_exprt(
2146  ID_and,
2147  {std::move(op0), std::move(op1), std::move(op2)},
2148  bool_typet())
2149  {
2150  }
2151 
2153  : multi_ary_exprt(
2154  ID_and,
2155  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2156  bool_typet())
2157  {
2158  }
2159 
2160  explicit and_exprt(exprt::operandst _operands)
2161  : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
2162  {
2163  }
2164 };
2165 
2169 
2171 
2172 template <>
2173 inline bool can_cast_expr<and_exprt>(const exprt &base)
2174 {
2175  return base.id() == ID_and;
2176 }
2177 
2184 inline const and_exprt &to_and_expr(const exprt &expr)
2185 {
2186  PRECONDITION(expr.id()==ID_and);
2187  return static_cast<const and_exprt &>(expr);
2188 }
2189 
2192 {
2193  PRECONDITION(expr.id()==ID_and);
2194  return static_cast<and_exprt &>(expr);
2195 }
2196 
2197 
2200 {
2201 public:
2203  : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
2204  {
2205  }
2206 };
2207 
2208 template <>
2209 inline bool can_cast_expr<implies_exprt>(const exprt &base)
2210 {
2211  return base.id() == ID_implies;
2212 }
2213 
2214 inline void validate_expr(const implies_exprt &value)
2215 {
2216  validate_operands(value, 2, "Implies must have two operands");
2217 }
2218 
2225 inline const implies_exprt &to_implies_expr(const exprt &expr)
2226 {
2227  PRECONDITION(expr.id()==ID_implies);
2228  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
2229  validate_expr(ret);
2230  return ret;
2231 }
2232 
2235 {
2236  PRECONDITION(expr.id()==ID_implies);
2237  implies_exprt &ret = static_cast<implies_exprt &>(expr);
2238  validate_expr(ret);
2239  return ret;
2240 }
2241 
2242 
2245 {
2246 public:
2248  : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
2249  {
2250  }
2251 
2253  : multi_ary_exprt(
2254  ID_or,
2255  {std::move(op0), std::move(op1), std::move(op2)},
2256  bool_typet())
2257  {
2258  }
2259 
2261  : multi_ary_exprt(
2262  ID_or,
2263  {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
2264  bool_typet())
2265  {
2266  }
2267 
2268  explicit or_exprt(exprt::operandst _operands)
2269  : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
2270  {
2271  }
2272 };
2273 
2277 
2279 
2280 template <>
2281 inline bool can_cast_expr<or_exprt>(const exprt &base)
2282 {
2283  return base.id() == ID_or;
2284 }
2285 
2292 inline const or_exprt &to_or_expr(const exprt &expr)
2293 {
2294  PRECONDITION(expr.id()==ID_or);
2295  return static_cast<const or_exprt &>(expr);
2296 }
2297 
2299 inline or_exprt &to_or_expr(exprt &expr)
2300 {
2301  PRECONDITION(expr.id()==ID_or);
2302  return static_cast<or_exprt &>(expr);
2303 }
2304 
2305 
2308 {
2309 public:
2310  xor_exprt(exprt _op0, exprt _op1)
2311  : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
2312  {
2313  }
2314 };
2315 
2316 template <>
2317 inline bool can_cast_expr<xor_exprt>(const exprt &base)
2318 {
2319  return base.id() == ID_xor;
2320 }
2321 
2328 inline const xor_exprt &to_xor_expr(const exprt &expr)
2329 {
2330  PRECONDITION(expr.id()==ID_xor);
2331  return static_cast<const xor_exprt &>(expr);
2332 }
2333 
2336 {
2337  PRECONDITION(expr.id()==ID_xor);
2338  return static_cast<xor_exprt &>(expr);
2339 }
2340 
2341 
2344 {
2345 public:
2346  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
2347  {
2348  }
2349 };
2350 
2351 template <>
2352 inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
2353 {
2354  return base.id() == ID_bitnot;
2355 }
2356 
2357 inline void validate_expr(const bitnot_exprt &value)
2358 {
2359  validate_operands(value, 1, "Bit-wise not must have one operand");
2360 }
2361 
2368 inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
2369 {
2370  PRECONDITION(expr.id()==ID_bitnot);
2371  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
2372  validate_expr(ret);
2373  return ret;
2374 }
2375 
2378 {
2379  PRECONDITION(expr.id()==ID_bitnot);
2380  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
2381  validate_expr(ret);
2382  return ret;
2383 }
2384 
2385 
2388 {
2389 public:
2390  bitor_exprt(const exprt &_op0, exprt _op1)
2391  : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
2392  {
2393  }
2394 };
2395 
2396 template <>
2397 inline bool can_cast_expr<bitor_exprt>(const exprt &base)
2398 {
2399  return base.id() == ID_bitor;
2400 }
2401 
2408 inline const bitor_exprt &to_bitor_expr(const exprt &expr)
2409 {
2410  PRECONDITION(expr.id()==ID_bitor);
2411  return static_cast<const bitor_exprt &>(expr);
2412 }
2413 
2416 {
2417  PRECONDITION(expr.id()==ID_bitor);
2418  return static_cast<bitor_exprt &>(expr);
2419 }
2420 
2421 
2424 {
2425 public:
2427  : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
2428  {
2429  }
2430 };
2431 
2432 template <>
2433 inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
2434 {
2435  return base.id() == ID_bitxor;
2436 }
2437 
2444 inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
2445 {
2446  PRECONDITION(expr.id()==ID_bitxor);
2447  return static_cast<const bitxor_exprt &>(expr);
2448 }
2449 
2452 {
2453  PRECONDITION(expr.id()==ID_bitxor);
2454  return static_cast<bitxor_exprt &>(expr);
2455 }
2456 
2457 
2460 {
2461 public:
2462  bitand_exprt(const exprt &_op0, exprt _op1)
2463  : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
2464  {
2465  }
2466 };
2467 
2468 template <>
2469 inline bool can_cast_expr<bitand_exprt>(const exprt &base)
2470 {
2471  return base.id() == ID_bitand;
2472 }
2473 
2480 inline const bitand_exprt &to_bitand_expr(const exprt &expr)
2481 {
2482  PRECONDITION(expr.id()==ID_bitand);
2483  return static_cast<const bitand_exprt &>(expr);
2484 }
2485 
2488 {
2489  PRECONDITION(expr.id()==ID_bitand);
2490  return static_cast<bitand_exprt &>(expr);
2491 }
2492 
2493 
2496 {
2497 public:
2498  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
2499  : binary_exprt(std::move(_src), _id, std::move(_distance))
2500  {
2501  }
2502 
2503  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
2504 
2506  {
2507  return op0();
2508  }
2509 
2510  const exprt &op() const
2511  {
2512  return op0();
2513  }
2514 
2516  {
2517  return op1();
2518  }
2519 
2520  const exprt &distance() const
2521  {
2522  return op1();
2523  }
2524 };
2525 
2526 template <>
2527 inline bool can_cast_expr<shift_exprt>(const exprt &base)
2528 {
2529  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr;
2530 }
2531 
2532 inline void validate_expr(const shift_exprt &value)
2533 {
2534  validate_operands(value, 2, "Shifts must have two operands");
2535 }
2536 
2543 inline const shift_exprt &to_shift_expr(const exprt &expr)
2544 {
2545  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
2546  validate_expr(ret);
2547  return ret;
2548 }
2549 
2552 {
2553  shift_exprt &ret = static_cast<shift_exprt &>(expr);
2554  validate_expr(ret);
2555  return ret;
2556 }
2557 
2558 
2561 {
2562 public:
2563  shl_exprt(exprt _src, exprt _distance)
2564  : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
2565  {
2566  }
2567 
2568  shl_exprt(exprt _src, const std::size_t _distance)
2569  : shift_exprt(std::move(_src), ID_shl, _distance)
2570  {
2571  }
2572 };
2573 
2580 inline const shl_exprt &to_shl_expr(const exprt &expr)
2581 {
2582  PRECONDITION(expr.id() == ID_shl);
2583  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
2584  validate_expr(ret);
2585  return ret;
2586 }
2587 
2590 {
2591  PRECONDITION(expr.id() == ID_shl);
2592  shl_exprt &ret = static_cast<shl_exprt &>(expr);
2593  validate_expr(ret);
2594  return ret;
2595 }
2596 
2599 {
2600 public:
2601  ashr_exprt(exprt _src, exprt _distance)
2602  : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
2603  {
2604  }
2605 
2606  ashr_exprt(exprt _src, const std::size_t _distance)
2607  : shift_exprt(std::move(_src), ID_ashr, _distance)
2608  {
2609  }
2610 };
2611 
2614 {
2615 public:
2616  lshr_exprt(exprt _src, exprt _distance)
2617  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2618  {
2619  }
2620 
2621  lshr_exprt(exprt _src, const std::size_t _distance)
2622  : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
2623  {
2624  }
2625 };
2626 
2629 {
2630 public:
2633  : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
2634  {
2635  }
2636 
2637  extractbit_exprt(exprt _src, const std::size_t _index);
2638 
2640  {
2641  return op0();
2642  }
2643 
2645  {
2646  return op1();
2647  }
2648 
2649  const exprt &src() const
2650  {
2651  return op0();
2652  }
2653 
2654  const exprt &index() const
2655  {
2656  return op1();
2657  }
2658 };
2659 
2660 template <>
2661 inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
2662 {
2663  return base.id() == ID_extractbit;
2664 }
2665 
2666 inline void validate_expr(const extractbit_exprt &value)
2667 {
2668  validate_operands(value, 2, "Extract bit must have two operands");
2669 }
2670 
2677 inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
2678 {
2679  PRECONDITION(expr.id()==ID_extractbit);
2680  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
2681  validate_expr(ret);
2682  return ret;
2683 }
2684 
2687 {
2688  PRECONDITION(expr.id()==ID_extractbit);
2689  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
2690  validate_expr(ret);
2691  return ret;
2692 }
2693 
2694 
2697 {
2698 public:
2704  extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
2705  : expr_protectedt(
2706  ID_extractbits,
2707  std::move(_type),
2708  {std::move(_src), std::move(_upper), std::move(_lower)})
2709  {
2710  }
2711 
2713  exprt _src,
2714  const std::size_t _upper,
2715  const std::size_t _lower,
2716  typet _type);
2717 
2719  {
2720  return op0();
2721  }
2722 
2724  {
2725  return op1();
2726  }
2727 
2729  {
2730  return op2();
2731  }
2732 
2733  const exprt &src() const
2734  {
2735  return op0();
2736  }
2737 
2738  const exprt &upper() const
2739  {
2740  return op1();
2741  }
2742 
2743  const exprt &lower() const
2744  {
2745  return op2();
2746  }
2747 };
2748 
2749 template <>
2750 inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
2751 {
2752  return base.id() == ID_extractbits;
2753 }
2754 
2755 inline void validate_expr(const extractbits_exprt &value)
2756 {
2757  validate_operands(value, 3, "Extract bits must have three operands");
2758 }
2759 
2766 inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
2767 {
2768  PRECONDITION(expr.id()==ID_extractbits);
2769  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
2770  validate_expr(ret);
2771  return ret;
2772 }
2773 
2776 {
2777  PRECONDITION(expr.id()==ID_extractbits);
2778  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
2779  validate_expr(ret);
2780  return ret;
2781 }
2782 
2783 
2786 {
2787 public:
2788  explicit address_of_exprt(const exprt &op);
2789 
2791  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
2792  {
2793  }
2794 
2796  {
2797  return op0();
2798  }
2799 
2800  const exprt &object() const
2801  {
2802  return op0();
2803  }
2804 };
2805 
2806 template <>
2807 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
2808 {
2809  return base.id() == ID_address_of;
2810 }
2811 
2812 inline void validate_expr(const address_of_exprt &value)
2813 {
2814  validate_operands(value, 1, "Address of must have one operand");
2815 }
2816 
2823 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
2824 {
2825  PRECONDITION(expr.id()==ID_address_of);
2826  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
2827  validate_expr(ret);
2828  return ret;
2829 }
2830 
2833 {
2834  PRECONDITION(expr.id()==ID_address_of);
2835  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
2836  validate_expr(ret);
2837  return ret;
2838 }
2839 
2840 
2843 {
2844 public:
2845  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
2846  {
2847  PRECONDITION(as_const(*this).op().type().id() == ID_bool);
2848  }
2849 };
2850 
2851 template <>
2852 inline bool can_cast_expr<not_exprt>(const exprt &base)
2853 {
2854  return base.id() == ID_not;
2855 }
2856 
2857 inline void validate_expr(const not_exprt &value)
2858 {
2859  validate_operands(value, 1, "Not must have one operand");
2860 }
2861 
2868 inline const not_exprt &to_not_expr(const exprt &expr)
2869 {
2870  PRECONDITION(expr.id()==ID_not);
2871  const not_exprt &ret = static_cast<const not_exprt &>(expr);
2872  validate_expr(ret);
2873  return ret;
2874 }
2875 
2878 {
2879  PRECONDITION(expr.id()==ID_not);
2880  not_exprt &ret = static_cast<not_exprt &>(expr);
2881  validate_expr(ret);
2882  return ret;
2883 }
2884 
2885 
2888 {
2889 public:
2890  explicit dereference_exprt(const exprt &op):
2891  unary_exprt(ID_dereference, op, op.type().subtype())
2892  {
2893  PRECONDITION(op.type().id()==ID_pointer);
2894  }
2895 
2897  : unary_exprt(ID_dereference, std::move(op), std::move(type))
2898  {
2899  }
2900 
2902  {
2903  return op0();
2904  }
2905 
2906  const exprt &pointer() const
2907  {
2908  return op0();
2909  }
2910 
2911  static void check(
2912  const exprt &expr,
2914  {
2915  DATA_CHECK(
2916  vm,
2917  expr.operands().size() == 1,
2918  "dereference expression must have one operand");
2919  }
2920 
2921  static void validate(
2922  const exprt &expr,
2923  const namespacet &ns,
2925 };
2926 
2927 template <>
2928 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
2929 {
2930  return base.id() == ID_dereference;
2931 }
2932 
2933 inline void validate_expr(const dereference_exprt &value)
2934 {
2935  validate_operands(value, 1, "Dereference must have one operand");
2936 }
2937 
2944 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
2945 {
2946  PRECONDITION(expr.id()==ID_dereference);
2947  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
2948  validate_expr(ret);
2949  return ret;
2950 }
2951 
2954 {
2955  PRECONDITION(expr.id()==ID_dereference);
2956  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
2957  validate_expr(ret);
2958  return ret;
2959 }
2960 
2961 
2963 class if_exprt : public ternary_exprt
2964 {
2965 public:
2967  : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
2968  {
2969  }
2970 
2972  : ternary_exprt(
2973  ID_if,
2974  std::move(cond),
2975  std::move(t),
2976  std::move(f),
2977  std::move(type))
2978  {
2979  }
2980 
2982  {
2983  return op0();
2984  }
2985 
2986  const exprt &cond() const
2987  {
2988  return op0();
2989  }
2990 
2992  {
2993  return op1();
2994  }
2995 
2996  const exprt &true_case() const
2997  {
2998  return op1();
2999  }
3000 
3002  {
3003  return op2();
3004  }
3005 
3006  const exprt &false_case() const
3007  {
3008  return op2();
3009  }
3010 };
3011 
3012 template <>
3013 inline bool can_cast_expr<if_exprt>(const exprt &base)
3014 {
3015  return base.id() == ID_if;
3016 }
3017 
3018 inline void validate_expr(const if_exprt &value)
3019 {
3020  validate_operands(value, 3, "If-then-else must have three operands");
3021 }
3022 
3029 inline const if_exprt &to_if_expr(const exprt &expr)
3030 {
3031  PRECONDITION(expr.id()==ID_if);
3032  const if_exprt &ret = static_cast<const if_exprt &>(expr);
3033  validate_expr(ret);
3034  return ret;
3035 }
3036 
3038 inline if_exprt &to_if_expr(exprt &expr)
3039 {
3040  PRECONDITION(expr.id()==ID_if);
3041  if_exprt &ret = static_cast<if_exprt &>(expr);
3042  validate_expr(ret);
3043  return ret;
3044 }
3045 
3050 {
3051 public:
3052  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
3053  : expr_protectedt(
3054  ID_with,
3055  _old.type(),
3056  {_old, std::move(_where), std::move(_new_value)})
3057  {
3058  }
3059 
3061  {
3062  return op0();
3063  }
3064 
3065  const exprt &old() const
3066  {
3067  return op0();
3068  }
3069 
3071  {
3072  return op1();
3073  }
3074 
3075  const exprt &where() const
3076  {
3077  return op1();
3078  }
3079 
3081  {
3082  return op2();
3083  }
3084 
3085  const exprt &new_value() const
3086  {
3087  return op2();
3088  }
3089 };
3090 
3091 template <>
3092 inline bool can_cast_expr<with_exprt>(const exprt &base)
3093 {
3094  return base.id() == ID_with;
3095 }
3096 
3097 inline void validate_expr(const with_exprt &value)
3098 {
3100  value, 3, "array/structure update must have at least 3 operands", true);
3102  value.operands().size() % 2 == 1,
3103  "array/structure update must have an odd number of operands");
3104 }
3105 
3112 inline const with_exprt &to_with_expr(const exprt &expr)
3113 {
3114  PRECONDITION(expr.id()==ID_with);
3115  const with_exprt &ret = static_cast<const with_exprt &>(expr);
3116  validate_expr(ret);
3117  return ret;
3118 }
3119 
3122 {
3123  PRECONDITION(expr.id()==ID_with);
3124  with_exprt &ret = static_cast<with_exprt &>(expr);
3125  validate_expr(ret);
3126  return ret;
3127 }
3128 
3130 {
3131 public:
3132  explicit index_designatort(exprt _index)
3133  : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
3134  {
3135  }
3136 
3137  const exprt &index() const
3138  {
3139  return op0();
3140  }
3141 
3143  {
3144  return op0();
3145  }
3146 };
3147 
3148 template <>
3149 inline bool can_cast_expr<index_designatort>(const exprt &base)
3150 {
3151  return base.id() == ID_index_designator;
3152 }
3153 
3154 inline void validate_expr(const index_designatort &value)
3155 {
3156  validate_operands(value, 1, "Index designator must have one operand");
3157 }
3158 
3165 inline const index_designatort &to_index_designator(const exprt &expr)
3166 {
3167  PRECONDITION(expr.id()==ID_index_designator);
3168  const index_designatort &ret = static_cast<const index_designatort &>(expr);
3169  validate_expr(ret);
3170  return ret;
3171 }
3172 
3175 {
3176  PRECONDITION(expr.id()==ID_index_designator);
3177  index_designatort &ret = static_cast<index_designatort &>(expr);
3178  validate_expr(ret);
3179  return ret;
3180 }
3181 
3183 {
3184 public:
3185  explicit member_designatort(const irep_idt &_component_name)
3186  : expr_protectedt(ID_member_designator, typet())
3187  {
3188  set(ID_component_name, _component_name);
3189  }
3190 
3192  {
3193  return get(ID_component_name);
3194  }
3195 };
3196 
3197 template <>
3199 {
3200  return base.id() == ID_member_designator;
3201 }
3202 
3203 inline void validate_expr(const member_designatort &value)
3204 {
3205  validate_operands(value, 0, "Member designator must not have operands");
3206 }
3207 
3215 {
3216  PRECONDITION(expr.id()==ID_member_designator);
3217  const member_designatort &ret = static_cast<const member_designatort &>(expr);
3218  validate_expr(ret);
3219  return ret;
3220 }
3221 
3224 {
3225  PRECONDITION(expr.id()==ID_member_designator);
3226  member_designatort &ret = static_cast<member_designatort &>(expr);
3227  validate_expr(ret);
3228  return ret;
3229 }
3230 
3231 
3234 {
3235 public:
3236  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
3237  : ternary_exprt(
3238  ID_update,
3239  _old,
3240  std::move(_designator),
3241  std::move(_new_value),
3242  _old.type())
3243  {
3244  }
3245 
3247  {
3248  return op0();
3249  }
3250 
3251  const exprt &old() const
3252  {
3253  return op0();
3254  }
3255 
3256  // the designator operands are either
3257  // 1) member_designator or
3258  // 2) index_designator
3259  // as defined above
3261  {
3262  return op1().operands();
3263  }
3264 
3266  {
3267  return op1().operands();
3268  }
3269 
3271  {
3272  return op2();
3273  }
3274 
3275  const exprt &new_value() const
3276  {
3277  return op2();
3278  }
3279 };
3280 
3281 template <>
3282 inline bool can_cast_expr<update_exprt>(const exprt &base)
3283 {
3284  return base.id() == ID_update;
3285 }
3286 
3287 inline void validate_expr(const update_exprt &value)
3288 {
3290  value, 3, "Array/structure update must have three operands");
3291 }
3292 
3299 inline const update_exprt &to_update_expr(const exprt &expr)
3300 {
3301  PRECONDITION(expr.id()==ID_update);
3302  const update_exprt &ret = static_cast<const update_exprt &>(expr);
3303  validate_expr(ret);
3304  return ret;
3305 }
3306 
3309 {
3310  PRECONDITION(expr.id()==ID_update);
3311  update_exprt &ret = static_cast<update_exprt &>(expr);
3312  validate_expr(ret);
3313  return ret;
3314 }
3315 
3316 
3317 #if 0
3318 class array_update_exprt:public expr_protectedt
3320 {
3321 public:
3322  array_update_exprt(
3323  const exprt &_array,
3324  const exprt &_index,
3325  const exprt &_new_value):
3326  exprt(ID_array_update, _array.type())
3327  {
3328  add_to_operands(_array, _index, _new_value);
3329  }
3330 
3331  array_update_exprt():expr_protectedt(ID_array_update)
3332  {
3333  operands().resize(3);
3334  }
3335 
3336  exprt &array()
3337  {
3338  return op0();
3339  }
3340 
3341  const exprt &array() const
3342  {
3343  return op0();
3344  }
3345 
3346  exprt &index()
3347  {
3348  return op1();
3349  }
3350 
3351  const exprt &index() const
3352  {
3353  return op1();
3354  }
3355 
3356  exprt &new_value()
3357  {
3358  return op2();
3359  }
3360 
3361  const exprt &new_value() const
3362  {
3363  return op2();
3364  }
3365 };
3366 
3367 template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
3368 {
3369  return base.id()==ID_array_update;
3370 }
3371 
3372 inline void validate_expr(const array_update_exprt &value)
3373 {
3374  validate_operands(value, 3, "Array update must have three operands");
3375 }
3376 
3383 inline const array_update_exprt &to_array_update_expr(const exprt &expr)
3384 {
3385  PRECONDITION(expr.id()==ID_array_update);
3386  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
3387  validate_expr(ret);
3388  return ret;
3389 }
3390 
3392 inline array_update_exprt &to_array_update_expr(exprt &expr)
3393 {
3394  PRECONDITION(expr.id()==ID_array_update);
3395  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
3396  validate_expr(ret);
3397  return ret;
3398 }
3399 
3400 #endif
3401 
3402 
3405 {
3406 public:
3407  member_exprt(exprt op, const irep_idt &component_name, typet _type)
3408  : unary_exprt(ID_member, std::move(op), std::move(_type))
3409  {
3410  set_component_name(component_name);
3411  }
3412 
3414  : unary_exprt(ID_member, std::move(op), c.type())
3415  {
3417  }
3418 
3420  {
3421  return get(ID_component_name);
3422  }
3423 
3424  void set_component_name(const irep_idt &component_name)
3425  {
3426  set(ID_component_name, component_name);
3427  }
3428 
3429  std::size_t get_component_number() const
3430  {
3431  return get_size_t(ID_component_number);
3432  }
3433 
3434  // will go away, use compound()
3435  const exprt &struct_op() const
3436  {
3437  return op0();
3438  }
3439 
3440  // will go away, use compound()
3442  {
3443  return op0();
3444  }
3445 
3446  const exprt &compound() const
3447  {
3448  return op0();
3449  }
3450 
3452  {
3453  return op0();
3454  }
3455 
3456  static void check(
3457  const exprt &expr,
3459  {
3460  DATA_CHECK(
3461  vm,
3462  expr.operands().size() == 1,
3463  "member expression must have one operand");
3464  }
3465 
3466  static void validate(
3467  const exprt &expr,
3468  const namespacet &ns,
3470 };
3471 
3472 template <>
3473 inline bool can_cast_expr<member_exprt>(const exprt &base)
3474 {
3475  return base.id() == ID_member;
3476 }
3477 
3478 inline void validate_expr(const member_exprt &value)
3479 {
3480  validate_operands(value, 1, "Extract member must have one operand");
3481 }
3482 
3489 inline const member_exprt &to_member_expr(const exprt &expr)
3490 {
3491  PRECONDITION(expr.id()==ID_member);
3492  const member_exprt &ret = static_cast<const member_exprt &>(expr);
3493  validate_expr(ret);
3494  return ret;
3495 }
3496 
3499 {
3500  PRECONDITION(expr.id()==ID_member);
3501  member_exprt &ret = static_cast<member_exprt &>(expr);
3502  validate_expr(ret);
3503  return ret;
3504 }
3505 
3506 
3509 {
3510 public:
3512  : unary_predicate_exprt(ID_isnan, std::move(op))
3513  {
3514  }
3515 };
3516 
3517 template <>
3518 inline bool can_cast_expr<isnan_exprt>(const exprt &base)
3519 {
3520  return base.id() == ID_isnan;
3521 }
3522 
3523 inline void validate_expr(const isnan_exprt &value)
3524 {
3525  validate_operands(value, 1, "Is NaN must have one operand");
3526 }
3527 
3534 inline const isnan_exprt &to_isnan_expr(const exprt &expr)
3535 {
3536  PRECONDITION(expr.id()==ID_isnan);
3537  const isnan_exprt &ret = static_cast<const isnan_exprt &>(expr);
3538  validate_expr(ret);
3539  return ret;
3540 }
3541 
3544 {
3545  PRECONDITION(expr.id()==ID_isnan);
3546  isnan_exprt &ret = static_cast<isnan_exprt &>(expr);
3547  validate_expr(ret);
3548  return ret;
3549 }
3550 
3551 
3554 {
3555 public:
3557  : unary_predicate_exprt(ID_isinf, std::move(op))
3558  {
3559  }
3560 };
3561 
3562 template <>
3563 inline bool can_cast_expr<isinf_exprt>(const exprt &base)
3564 {
3565  return base.id() == ID_isinf;
3566 }
3567 
3568 inline void validate_expr(const isinf_exprt &value)
3569 {
3570  validate_operands(value, 1, "Is infinite must have one operand");
3571 }
3572 
3579 inline const isinf_exprt &to_isinf_expr(const exprt &expr)
3580 {
3581  PRECONDITION(expr.id()==ID_isinf);
3582  const isinf_exprt &ret = static_cast<const isinf_exprt &>(expr);
3583  validate_expr(ret);
3584  return ret;
3585 }
3586 
3589 {
3590  PRECONDITION(expr.id()==ID_isinf);
3591  isinf_exprt &ret = static_cast<isinf_exprt &>(expr);
3592  validate_expr(ret);
3593  return ret;
3594 }
3595 
3596 
3599 {
3600 public:
3602  : unary_predicate_exprt(ID_isfinite, std::move(op))
3603  {
3604  }
3605 };
3606 
3607 template <>
3608 inline bool can_cast_expr<isfinite_exprt>(const exprt &base)
3609 {
3610  return base.id() == ID_isfinite;
3611 }
3612 
3613 inline void validate_expr(const isfinite_exprt &value)
3614 {
3615  validate_operands(value, 1, "Is finite must have one operand");
3616 }
3617 
3624 inline const isfinite_exprt &to_isfinite_expr(const exprt &expr)
3625 {
3626  PRECONDITION(expr.id()==ID_isfinite);
3627  const isfinite_exprt &ret = static_cast<const isfinite_exprt &>(expr);
3628  validate_expr(ret);
3629  return ret;
3630 }
3631 
3634 {
3635  PRECONDITION(expr.id()==ID_isfinite);
3636  isfinite_exprt &ret = static_cast<isfinite_exprt &>(expr);
3637  validate_expr(ret);
3638  return ret;
3639 }
3640 
3641 
3644 {
3645 public:
3647  : unary_predicate_exprt(ID_isnormal, std::move(op))
3648  {
3649  }
3650 };
3651 
3652 template <>
3653 inline bool can_cast_expr<isnormal_exprt>(const exprt &base)
3654 {
3655  return base.id() == ID_isnormal;
3656 }
3657 
3658 inline void validate_expr(const isnormal_exprt &value)
3659 {
3660  validate_operands(value, 1, "Is normal must have one operand");
3661 }
3662 
3669 inline const isnormal_exprt &to_isnormal_expr(const exprt &expr)
3670 {
3671  PRECONDITION(expr.id()==ID_isnormal);
3672  const isnormal_exprt &ret = static_cast<const isnormal_exprt &>(expr);
3673  validate_expr(ret);
3674  return ret;
3675 }
3676 
3679 {
3680  PRECONDITION(expr.id()==ID_isnormal);
3681  isnormal_exprt &ret = static_cast<isnormal_exprt &>(expr);
3682  validate_expr(ret);
3683  return ret;
3684 }
3685 
3686 
3689 {
3690 public:
3693  std::move(_lhs),
3694  ID_ieee_float_equal,
3695  std::move(_rhs))
3696  {
3697  }
3698 };
3699 
3700 template <>
3702 {
3703  return base.id() == ID_ieee_float_equal;
3704 }
3705 
3706 inline void validate_expr(const ieee_float_equal_exprt &value)
3707 {
3708  validate_operands(value, 2, "IEEE equality must have two operands");
3709 }
3710 
3718 {
3719  PRECONDITION(expr.id()==ID_ieee_float_equal);
3720  const ieee_float_equal_exprt &ret =
3721  static_cast<const ieee_float_equal_exprt &>(expr);
3722  validate_expr(ret);
3723  return ret;
3724 }
3725 
3728 {
3729  PRECONDITION(expr.id()==ID_ieee_float_equal);
3730  ieee_float_equal_exprt &ret = static_cast<ieee_float_equal_exprt &>(expr);
3731  validate_expr(ret);
3732  return ret;
3733 }
3734 
3735 
3738 {
3739 public:
3742  std::move(_lhs),
3743  ID_ieee_float_notequal,
3744  std::move(_rhs))
3745  {
3746  }
3747 };
3748 
3749 template <>
3751 {
3752  return base.id() == ID_ieee_float_notequal;
3753 }
3754 
3755 inline void validate_expr(const ieee_float_notequal_exprt &value)
3756 {
3757  validate_operands(value, 2, "IEEE inequality must have two operands");
3758 }
3759 
3767  const exprt &expr)
3768 {
3769  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3770  const ieee_float_notequal_exprt &ret =
3771  static_cast<const ieee_float_notequal_exprt &>(expr);
3772  validate_expr(ret);
3773  return ret;
3774 }
3775 
3778 {
3779  PRECONDITION(expr.id()==ID_ieee_float_notequal);
3781  static_cast<ieee_float_notequal_exprt &>(expr);
3782  validate_expr(ret);
3783  return ret;
3784 }
3785 
3790 {
3791 public:
3793  const exprt &_lhs,
3794  const irep_idt &_id,
3795  exprt _rhs,
3796  exprt _rm)
3797  : ternary_exprt(_id, _lhs, std::move(_rhs), std::move(_rm), _lhs.type())
3798  {
3799  }
3800 
3802  {
3803  return op0();
3804  }
3805 
3806  const exprt &lhs() const
3807  {
3808  return op0();
3809  }
3810 
3812  {
3813  return op1();
3814  }
3815 
3816  const exprt &rhs() const
3817  {
3818  return op1();
3819  }
3820 
3822  {
3823  return op2();
3824  }
3825 
3826  const exprt &rounding_mode() const
3827  {
3828  return op2();
3829  }
3830 };
3831 
3832 template <>
3834 {
3835  return base.id() == ID_floatbv_plus || base.id() == ID_floatbv_minus ||
3836  base.id() == ID_floatbv_div || base.id() == ID_floatbv_mult;
3837 }
3838 
3839 inline void validate_expr(const ieee_float_op_exprt &value)
3840 {
3842  value, 3, "IEEE float operations must have three arguments");
3843 }
3844 
3852 {
3853  const ieee_float_op_exprt &ret =
3854  static_cast<const ieee_float_op_exprt &>(expr);
3855  validate_expr(ret);
3856  return ret;
3857 }
3858 
3861 {
3862  ieee_float_op_exprt &ret = static_cast<ieee_float_op_exprt &>(expr);
3863  validate_expr(ret);
3864  return ret;
3865 }
3866 
3867 
3870 {
3871 public:
3872  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
3873  {
3874  }
3875 };
3876 
3877 template <>
3878 inline bool can_cast_expr<type_exprt>(const exprt &base)
3879 {
3880  return base.id() == ID_type;
3881 }
3882 
3889 inline const type_exprt &to_type_expr(const exprt &expr)
3890 {
3892  const type_exprt &ret = static_cast<const type_exprt &>(expr);
3893  return ret;
3894 }
3895 
3898 {
3900  type_exprt &ret = static_cast<type_exprt &>(expr);
3901  return ret;
3902 }
3903 
3906 {
3907 public:
3908  constant_exprt(const irep_idt &_value, typet _type)
3909  : expr_protectedt(ID_constant, std::move(_type))
3910  {
3911  set_value(_value);
3912  }
3913 
3914  const irep_idt &get_value() const
3915  {
3916  return get(ID_value);
3917  }
3918 
3919  void set_value(const irep_idt &value)
3920  {
3921  set(ID_value, value);
3922  }
3923 
3924  bool value_is_zero_string() const;
3925 };
3926 
3927 template <>
3928 inline bool can_cast_expr<constant_exprt>(const exprt &base)
3929 {
3930  return base.id() == ID_constant;
3931 }
3932 
3939 inline const constant_exprt &to_constant_expr(const exprt &expr)
3940 {
3941  PRECONDITION(expr.id()==ID_constant);
3942  return static_cast<const constant_exprt &>(expr);
3943 }
3944 
3947 {
3948  PRECONDITION(expr.id()==ID_constant);
3949  return static_cast<constant_exprt &>(expr);
3950 }
3951 
3952 
3955 {
3956 public:
3958  {
3959  }
3960 };
3961 
3964 {
3965 public:
3967  {
3968  }
3969 };
3970 
3972 class nil_exprt : public nullary_exprt
3973 {
3974 public:
3976  : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
3977  {
3978  }
3979 };
3980 
3981 template <>
3982 inline bool can_cast_expr<nil_exprt>(const exprt &base)
3983 {
3984  return base.id() == ID_nil;
3985 }
3986 
3989 {
3990 public:
3992  : constant_exprt(ID_NULL, std::move(type))
3993  {
3994  }
3995 };
3996 
3999 {
4000 public:
4001  replication_exprt(const constant_exprt &_times, const exprt &_src)
4002  : binary_exprt(_times, ID_replication, _src)
4003  {
4004  }
4005 
4007  {
4008  return static_cast<constant_exprt &>(op0());
4009  }
4010 
4011  const constant_exprt &times() const
4012  {
4013  return static_cast<const constant_exprt &>(op0());
4014  }
4015 
4017  {
4018  return op1();
4019  }
4020 
4021  const exprt &op() const
4022  {
4023  return op1();
4024  }
4025 };
4026 
4027 template <>
4028 inline bool can_cast_expr<replication_exprt>(const exprt &base)
4029 {
4030  return base.id() == ID_replication;
4031 }
4032 
4033 inline void validate_expr(const replication_exprt &value)
4034 {
4035  validate_operands(value, 2, "Bit-wise replication must have two operands");
4036 }
4037 
4044 inline const replication_exprt &to_replication_expr(const exprt &expr)
4045 {
4046  PRECONDITION(expr.id() == ID_replication);
4047  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
4048  validate_expr(ret);
4049  return ret;
4050 }
4051 
4054 {
4055  PRECONDITION(expr.id() == ID_replication);
4056  replication_exprt &ret = static_cast<replication_exprt &>(expr);
4057  validate_expr(ret);
4058  return ret;
4059 }
4060 
4067 {
4068 public:
4070  : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
4071  {
4072  }
4073 
4075  : multi_ary_exprt(
4076  ID_concatenation,
4077  {std::move(_op0), std::move(_op1)},
4078  std::move(_type))
4079  {
4080  }
4081 };
4082 
4083 template <>
4085 {
4086  return base.id() == ID_concatenation;
4087 }
4088 
4096 {
4097  PRECONDITION(expr.id()==ID_concatenation);
4098  return static_cast<const concatenation_exprt &>(expr);
4099 }
4100 
4103 {
4104  PRECONDITION(expr.id()==ID_concatenation);
4105  return static_cast<concatenation_exprt &>(expr);
4106 }
4107 
4108 
4111 {
4112 public:
4113  explicit infinity_exprt(typet _type)
4114  : nullary_exprt(ID_infinity, std::move(_type))
4115  {
4116  }
4117 };
4118 
4121 {
4122 public:
4123  using variablest = std::vector<symbol_exprt>;
4124 
4127  irep_idt _id,
4128  const variablest &_variables,
4129  exprt _where,
4130  typet _type)
4131  : binary_exprt(
4133  ID_tuple,
4134  (const operandst &)_variables,
4135  typet(ID_tuple)),
4136  _id,
4137  std::move(_where),
4138  std::move(_type))
4139  {
4140  }
4141 
4143  {
4144  return (variablest &)to_multi_ary_expr(op0()).operands();
4145  }
4146 
4147  const variablest &variables() const
4148  {
4149  return (variablest &)to_multi_ary_expr(op0()).operands();
4150  }
4151 
4153  {
4154  return op1();
4155  }
4156 
4157  const exprt &where() const
4158  {
4159  return op1();
4160  }
4161 };
4162 
4164 class let_exprt : public binary_exprt
4165 {
4166 public:
4169  operandst values,
4170  const exprt &where)
4171  : binary_exprt(
4172  binding_exprt(
4173  ID_let_binding,
4174  std::move(variables),
4175  where,
4176  where.type()),
4177  ID_let,
4178  multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
4179  where.type())
4180  {
4181  PRECONDITION(this->variables().size() == this->values().size());
4182  }
4183 
4186  : let_exprt(
4187  binding_exprt::variablest{std::move(symbol)},
4188  operandst{std::move(value)},
4189  where)
4190  {
4191  }
4192 
4194  {
4195  return static_cast<binding_exprt &>(op0());
4196  }
4197 
4198  const binding_exprt &binding() const
4199  {
4200  return static_cast<const binding_exprt &>(op0());
4201  }
4202 
4205  {
4206  auto &variables = binding().variables();
4207  PRECONDITION(variables.size() == 1);
4208  return variables.front();
4209  }
4210 
4212  const symbol_exprt &symbol() const
4213  {
4214  const auto &variables = binding().variables();
4215  PRECONDITION(variables.size() == 1);
4216  return variables.front();
4217  }
4218 
4221  {
4222  auto &values = this->values();
4223  PRECONDITION(values.size() == 1);
4224  return values.front();
4225  }
4226 
4228  const exprt &value() const
4229  {
4230  const auto &values = this->values();
4231  PRECONDITION(values.size() == 1);
4232  return values.front();
4233  }
4234 
4236  {
4237  return static_cast<multi_ary_exprt &>(op1()).operands();
4238  }
4239 
4240  const operandst &values() const
4241  {
4242  return static_cast<const multi_ary_exprt &>(op1()).operands();
4243  }
4244 
4247  {
4248  return binding().variables();
4249  }
4250 
4253  {
4254  return binding().variables();
4255  }
4256 
4259  {
4260  return binding().where();
4261  }
4262 
4264  const exprt &where() const
4265  {
4266  return binding().where();
4267  }
4268 
4269  static void validate(const exprt &, validation_modet);
4270 };
4271 
4272 template <>
4273 inline bool can_cast_expr<let_exprt>(const exprt &base)
4274 {
4275  return base.id() == ID_let;
4276 }
4277 
4278 inline void validate_expr(const let_exprt &let_expr)
4279 {
4280  validate_operands(let_expr, 2, "Let must have two operands");
4281 }
4282 
4289 inline const let_exprt &to_let_expr(const exprt &expr)
4290 {
4291  PRECONDITION(expr.id()==ID_let);
4292  const let_exprt &ret = static_cast<const let_exprt &>(expr);
4293  validate_expr(ret);
4294  return ret;
4295 }
4296 
4299 {
4300  PRECONDITION(expr.id()==ID_let);
4301  let_exprt &ret = static_cast<let_exprt &>(expr);
4302  validate_expr(ret);
4303  return ret;
4304 }
4305 
4308 {
4309 public:
4311  : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
4312  {
4313  }
4314 
4315  explicit popcount_exprt(const exprt &_op)
4316  : unary_exprt(ID_popcount, _op, _op.type())
4317  {
4318  }
4319 };
4320 
4321 template <>
4322 inline bool can_cast_expr<popcount_exprt>(const exprt &base)
4323 {
4324  return base.id() == ID_popcount;
4325 }
4326 
4327 inline void validate_expr(const popcount_exprt &value)
4328 {
4329  validate_operands(value, 1, "popcount must have one operand");
4330 }
4331 
4338 inline const popcount_exprt &to_popcount_expr(const exprt &expr)
4339 {
4340  PRECONDITION(expr.id() == ID_popcount);
4341  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
4342  validate_expr(ret);
4343  return ret;
4344 }
4345 
4348 {
4349  PRECONDITION(expr.id() == ID_popcount);
4350  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
4351  validate_expr(ret);
4352  return ret;
4353 }
4354 
4359 {
4360 public:
4361  cond_exprt(operandst _operands, typet _type)
4362  : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
4363  {
4364  }
4365 
4369  void add_case(const exprt &condition, const exprt &value)
4370  {
4371  PRECONDITION(condition.type().id() == ID_bool);
4372  operands().reserve(operands().size() + 2);
4373  operands().push_back(condition);
4374  operands().push_back(value);
4375  }
4376 };
4377 
4378 template <>
4379 inline bool can_cast_expr<cond_exprt>(const exprt &base)
4380 {
4381  return base.id() == ID_cond;
4382 }
4383 
4384 inline void validate_expr(const cond_exprt &value)
4385 {
4387  value.operands().size() % 2 == 0, "cond must have even number of operands");
4388 }
4389 
4396 inline const cond_exprt &to_cond_expr(const exprt &expr)
4397 {
4398  PRECONDITION(expr.id() == ID_cond);
4399  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
4400  validate_expr(ret);
4401  return ret;
4402 }
4403 
4406 {
4407  PRECONDITION(expr.id() == ID_cond);
4408  cond_exprt &ret = static_cast<cond_exprt &>(expr);
4409  validate_expr(ret);
4410  return ret;
4411 }
4412 
4422 {
4423 public:
4425  symbol_exprt arg,
4426  exprt body,
4427  array_typet _type)
4428  : binary_exprt(
4429  std::move(arg),
4430  ID_array_comprehension,
4431  std::move(body),
4432  std::move(_type))
4433  {
4434  }
4435 
4436  const array_typet &type() const
4437  {
4438  return static_cast<const array_typet &>(binary_exprt::type());
4439  }
4440 
4442  {
4443  return static_cast<array_typet &>(binary_exprt::type());
4444  }
4445 
4446  const symbol_exprt &arg() const
4447  {
4448  return static_cast<const symbol_exprt &>(op0());
4449  }
4450 
4452  {
4453  return static_cast<symbol_exprt &>(op0());
4454  }
4455 
4456  const exprt &body() const
4457  {
4458  return op1();
4459  }
4460 
4462  {
4463  return op1();
4464  }
4465 };
4466 
4467 template <>
4469 {
4470  return base.id() == ID_array_comprehension;
4471 }
4472 
4473 inline void validate_expr(const array_comprehension_exprt &value)
4474 {
4475  validate_operands(value, 2, "'Array comprehension' must have two operands");
4476 }
4477 
4484 inline const array_comprehension_exprt &
4486 {
4487  PRECONDITION(expr.id() == ID_array_comprehension);
4488  const array_comprehension_exprt &ret =
4489  static_cast<const array_comprehension_exprt &>(expr);
4490  validate_expr(ret);
4491  return ret;
4492 }
4493 
4496 {
4497  PRECONDITION(expr.id() == ID_array_comprehension);
4499  static_cast<array_comprehension_exprt &>(expr);
4500  validate_expr(ret);
4501  return ret;
4502 }
4503 
4504 inline void validate_expr(const class class_method_descriptor_exprt &value);
4505 
4508 {
4509 public:
4525  typet _type,
4529  : nullary_exprt(ID_virtual_function, std::move(_type))
4530  {
4532  set(ID_component_name, std::move(mangled_method_name));
4533  set(ID_C_class, std::move(class_id));
4534  set(ID_C_base_name, std::move(base_method_name));
4535  set(ID_identifier, std::move(id));
4536  validate_expr(*this);
4537  }
4538 
4546  {
4547  return get(ID_component_name);
4548  }
4549 
4553  const irep_idt &class_id() const
4554  {
4555  return get(ID_C_class);
4556  }
4557 
4561  {
4562  return get(ID_C_base_name);
4563  }
4564 
4568  const irep_idt &get_identifier() const
4569  {
4570  return get(ID_identifier);
4571  }
4572 };
4573 
4574 inline void validate_expr(const class class_method_descriptor_exprt &value)
4575 {
4576  validate_operands(value, 0, "class method descriptor must not have operands");
4578  !value.mangled_method_name().empty(),
4579  "class method descriptor must have a mangled method name.");
4581  !value.class_id().empty(), "class method descriptor must have a class id.");
4583  !value.base_method_name().empty(),
4584  "class method descriptor must have a base method name.");
4586  value.get_identifier() == id2string(value.class_id()) + "." +
4587  id2string(value.mangled_method_name()),
4588  "class method descriptor must have an identifier in the expected format.");
4589 }
4590 
4597 inline const class_method_descriptor_exprt &
4599 {
4600  PRECONDITION(expr.id() == ID_virtual_function);
4601  const class_method_descriptor_exprt &ret =
4602  static_cast<const class_method_descriptor_exprt &>(expr);
4603  validate_expr(ret);
4604  return ret;
4605 }
4606 
4607 template <>
4609 {
4610  return base.id() == ID_virtual_function;
4611 }
4612 
4613 #endif // CPROVER_UTIL_STD_EXPR_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3049
index_exprt::array
const exprt & array() const
Definition: std_expr.h:1314
to_popcount_expr
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
Definition: std_expr.h:4338
exprt::op2
exprt & op2()
Definition: expr.h:108
dynamic_object_exprt::dynamic_object_exprt
dynamic_object_exprt(typet type)
Definition: std_expr.h:1922
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:2966
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:4485
to_vector_expr
const vector_exprt & to_vector_expr(const exprt &expr)
Cast an exprt to an vector_exprt.
Definition: std_expr.h:1551
can_cast_expr< union_exprt >
bool can_cast_expr< union_exprt >(const exprt &base)
Definition: std_expr.h:1597
to_update_expr
const update_exprt & to_update_expr(const exprt &expr)
Cast an exprt to an update_exprt.
Definition: std_expr.h:3299
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
can_cast_expr< rem_exprt >
bool can_cast_expr< rem_exprt >(const exprt &base)
Definition: std_expr.h:1154
index_exprt::index
const exprt & index() const
Definition: std_expr.h:1324
shl_exprt::shl_exprt
shl_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2568
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:3518
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:4185
can_cast_expr< cond_exprt >
bool can_cast_expr< cond_exprt >(const exprt &base)
Definition: std_expr.h:4379
member_exprt::member_exprt
member_exprt(exprt op, const irep_idt &component_name, typet _type)
Definition: std_expr.h:3407
can_cast_expr< array_list_exprt >
bool can_cast_expr< array_list_exprt >(const exprt &base)
Definition: std_expr.h:1503
can_cast_expr< mod_exprt >
bool can_cast_expr< mod_exprt >(const exprt &base)
Definition: std_expr.h:1109
extractbits_exprt::lower
exprt & lower()
Definition: std_expr.h:2728
binding_exprt::where
const exprt & where() const
Definition: std_expr.h:4157
if_exprt::if_exprt
if_exprt(exprt cond, exprt t, exprt f, typet type)
Definition: std_expr.h:2971
member_designatort::member_designatort
member_designatort(const irep_idt &_component_name)
Definition: std_expr.h:3185
shift_exprt::shift_exprt
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
Definition: std_expr.h:2498
to_div_expr
const div_exprt & to_div_expr(const exprt &expr)
Cast an exprt to a div_exprt.
Definition: std_expr.h:1080
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:3149
can_cast_expr< isinf_exprt >
bool can_cast_expr< isinf_exprt >(const exprt &base)
Definition: std_expr.h:3563
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:4545
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
Definition: std_expr.h:2152
array_list_exprt::array_list_exprt
array_list_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1480
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1462
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:2160
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:1794
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, exprt _distance)
Definition: std_expr.h:2616
address_of_exprt::object
exprt & object()
Definition: std_expr.h:2795
can_cast_expr< concatenation_exprt >
bool can_cast_expr< concatenation_exprt >(const exprt &base)
Definition: std_expr.h:4084
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:1384
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:2100
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:1688
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:3889
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
Definition: std_expr.h:804
can_cast_expr< bitor_exprt >
bool can_cast_expr< bitor_exprt >(const exprt &base)
Definition: std_expr.h:2397
floatbv_typecast_exprt::op
exprt & op()
Definition: std_expr.h:2078
can_cast_expr< not_exprt >
bool can_cast_expr< not_exprt >(const exprt &base)
Definition: std_expr.h:2852
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:3740
update_exprt::old
exprt & old()
Definition: std_expr.h:3246
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:3957
mult_exprt::mult_exprt
mult_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:988
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
isnormal_exprt::isnormal_exprt
isnormal_exprt(exprt op)
Definition: std_expr.h:3646
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:3691
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2887
extractbits_exprt::src
const exprt & src() const
Definition: std_expr.h:2733
dynamic_object_exprt
Representation of heap-allocated objects.
Definition: std_expr.h:1919
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:2996
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2963
member_designatort
Definition: std_expr.h:3182
is_dynamic_object_exprt
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: std_expr.h:1983
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:3608
replication_exprt::times
constant_exprt & times()
Definition: std_expr.h:4006
div_exprt::div_exprt
div_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1033
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:1490
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1831
xor_exprt
Boolean XOR.
Definition: std_expr.h:2307
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:3080
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:883
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:1739
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:4204
and_exprt
Boolean AND.
Definition: std_expr.h:2136
union_exprt
Union constructor from single element.
Definition: std_expr.h:1566
array_comprehension_exprt::type
array_typet & type()
Definition: std_expr.h:4441
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:2426
can_cast_expr< bitxor_exprt >
bool can_cast_expr< bitxor_exprt >(const exprt &base)
Definition: std_expr.h:2433
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:3717
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:1412
can_cast_expr< ieee_float_notequal_exprt >
bool can_cast_expr< ieee_float_notequal_exprt >(const exprt &base)
Definition: std_expr.h:3750
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:880
can_cast_expr< xor_exprt >
bool can_cast_expr< xor_exprt >(const exprt &base)
Definition: std_expr.h:2317
rem_exprt
Remainder of division.
Definition: std_expr.h:1144
equal_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1204
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:4524
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:1721
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:2601
array_exprt::array_exprt
array_exprt(operandst _operands, array_typet _type)
Definition: std_expr.h:1434
dereference_exprt::dereference_exprt
dereference_exprt(const exprt &op)
Definition: std_expr.h:2890
index_exprt::index_exprt
index_exprt(exprt _array, exprt _index, typet _type)
Definition: std_expr.h:1300
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:1613
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:1379
member_designatort::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3191
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:2260
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:3265
array_of_exprt::type
const array_typet & type() const
Definition: std_expr.h:1374
exprt::op0
exprt & op0()
Definition: expr.h:102
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:3251
extractbits_exprt::upper
const exprt & upper() const
Definition: std_expr.h:2738
replication_exprt::op
const exprt & op() const
Definition: std_expr.h:4021
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:4446
cond_exprt::cond_exprt
cond_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4361
can_cast_expr< minus_exprt >
bool can_cast_expr< minus_exprt >(const exprt &base)
Definition: std_expr.h:949
to_array_list_expr
const array_list_exprt & to_array_list_expr(const exprt &expr)
Definition: std_expr.h:1513
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:4066
index_designatort::index_designatort
index_designatort(exprt _index)
Definition: std_expr.h:3132
nullary_exprt::move_to_operands
void move_to_operands(exprt &)=delete
vector_exprt
Vector constructor from list of elements.
Definition: std_expr.h:1530
to_isnormal_expr
const isnormal_exprt & to_isnormal_expr(const exprt &expr)
Cast an exprt to a isnormal_exprt.
Definition: std_expr.h:3669
lshr_exprt
Logical right shift.
Definition: std_expr.h:2613
index_exprt::index_exprt
index_exprt(const exprt &_array, exprt _index)
Definition: std_expr.h:1295
type_exprt::type_exprt
type_exprt(typet type)
Definition: std_expr.h:3872
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:2469
to_bitand_expr
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
Definition: std_expr.h:2480
div_exprt
Division.
Definition: std_expr.h:1030
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
shift_exprt::op
exprt & op()
Definition: std_expr.h:2505
can_cast_expr< array_exprt >
bool can_cast_expr< array_exprt >(const exprt &base)
Definition: std_expr.h:1451
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:3473
minus_exprt::minus_exprt
minus_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:942
union_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:1585
equal_exprt
Equality.
Definition: std_expr.h:1189
array_comprehension_exprt::type
const array_typet & type() const
Definition: std_expr.h:4436
multi_ary_exprt::op2
exprt & op2()
Definition: std_expr.h:823
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:1170
to_minus_expr
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
Definition: std_expr.h:965
floatbv_typecast_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:2093
replication_exprt
Bit-vector replication.
Definition: std_expr.h:3998
can_cast_expr< equal_exprt >
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition: std_expr.h:1214
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4110
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
array_list_exprt::add
void add(exprt index, exprt value)
add an index/value pair
Definition: std_expr.h:1496
isfinite_exprt
Evaluates to true if the operand is finite.
Definition: std_expr.h:3598
can_cast_expr< implies_exprt >
bool can_cast_expr< implies_exprt >(const exprt &base)
Definition: std_expr.h:2209
notequal_exprt
Disequality.
Definition: std_expr.h:1247
replication_exprt::op
exprt & op()
Definition: std_expr.h:4016
extractbits_exprt::upper
exprt & upper()
Definition: std_expr.h:2723
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:1580
multi_ary_exprt::op3
exprt & op3()
Definition: std_expr.h:829
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:4451
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:1766
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:4142
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:4095
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4507
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1632
to_shift_expr
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2543
let_exprt::variables
const binding_exprt::variablest & variables() const
convenience accessor for binding().variables()
Definition: std_expr.h:4252
union_exprt::union_exprt
union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
Definition: std_expr.h:1569
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:1693
ieee_float_notequal_exprt
IEEE floating-point disequality.
Definition: std_expr.h:3737
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:4246
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:4568
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:4220
or_exprt::or_exprt
or_exprt(exprt::operandst _operands)
Definition: std_expr.h:2268
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:4273
not_exprt::not_exprt
not_exprt(exprt _op)
Definition: std_expr.h:2845
can_cast_expr< bitnot_exprt >
bool can_cast_expr< bitnot_exprt >(const exprt &base)
Definition: std_expr.h:2352
can_cast_expr< and_exprt >
bool can_cast_expr< and_exprt >(const exprt &base)
Definition: std_expr.h:2173
member_exprt::get_component_number
std::size_t get_component_number() const
Definition: std_expr.h:3429
array_exprt::type
const array_typet & type() const
Definition: std_expr.h:1439
with_exprt::where
const exprt & where() const
Definition: std_expr.h:3075
with_exprt::old
exprt & old()
Definition: std_expr.h:3060
plus_exprt::plus_exprt
plus_exprt(exprt _lhs, exprt _rhs, typet _type)
Definition: std_expr.h:888
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2144
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:2790
to_cond_expr
const cond_exprt & to_cond_expr(const exprt &expr)
Cast an exprt to a cond_exprt.
Definition: std_expr.h:4396
with_exprt::with_exprt
with_exprt(const exprt &_old, exprt _where, exprt _new_value)
Definition: std_expr.h:3052
xor_exprt::xor_exprt
xor_exprt(exprt _op0, exprt _op1)
Definition: std_expr.h:2310
rem_exprt::rem_exprt
rem_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1147
notequal_exprt::notequal_exprt
notequal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1250
bitxor_exprt
Bit-wise XOR.
Definition: std_expr.h:2423
bitor_exprt
Bit-wise OR.
Definition: std_expr.h:2387
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:4228
dereference_exprt::pointer
const exprt & pointer() const
Definition: std_expr.h:2906
or_exprt
Boolean OR.
Definition: std_expr.h:2244
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:1444
to_mod_expr
const mod_exprt & to_mod_expr(const exprt &expr)
Cast an exprt to a mod_exprt.
Definition: std_expr.h:1125
complex_real_exprt::complex_real_exprt
complex_real_exprt(const exprt &op)
Definition: std_expr.h:1742
member_exprt::struct_op
exprt & struct_op()
Definition: std_expr.h:3441
update_exprt::update_exprt
update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
Definition: std_expr.h:3236
and_exprt::and_exprt
and_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2139
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:4560
to_mult_expr
const mult_exprt & to_mult_expr(const exprt &expr)
Cast an exprt to a mult_exprt.
Definition: std_expr.h:1011
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3988
array_comprehension_exprt::array_comprehension_exprt
array_comprehension_exprt(symbol_exprt arg, exprt body, array_typet _type)
Definition: std_expr.h:4424
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:2823
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:3456
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:4044
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2066
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
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:2390
multi_ary_exprt::op1
const exprt & op1() const
Definition: std_expr.h:841
can_cast_expr< address_of_exprt >
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: std_expr.h:2807
can_cast_expr< plus_exprt >
bool can_cast_expr< plus_exprt >(const exprt &base)
Definition: std_expr.h:904
update_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3275
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
to_xor_expr
const xor_exprt & to_xor_expr(const exprt &expr)
Cast an exprt to a xor_exprt.
Definition: std_expr.h:2328
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:817
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
extractbits_exprt::lower
const exprt & lower() const
Definition: std_expr.h:2743
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:1396
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:2896
nil_exprt
The NIL expression.
Definition: std_expr.h:3972
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1366
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:2901
index_designatort::index
const exprt & index() const
Definition: std_expr.h:3137
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:2563
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:4289
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:2069
can_cast_expr< notequal_exprt >
bool can_cast_expr< notequal_exprt >(const exprt &base)
Definition: std_expr.h:1257
to_plus_expr
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
Definition: std_expr.h:920
to_isfinite_expr
const isfinite_exprt & to_isfinite_expr(const exprt &expr)
Cast an exprt to a isfinite_exprt.
Definition: std_expr.h:3624
isfinite_exprt::isfinite_exprt
isfinite_exprt(exprt op)
Definition: std_expr.h:3601
cond_exprt::add_case
void add_case(const exprt &condition, const exprt &value)
adds a case to a cond expression
Definition: std_expr.h:4369
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:1898
can_cast_expr< nil_exprt >
bool can_cast_expr< nil_exprt >(const exprt &base)
Definition: std_expr.h:3982
extractbits_exprt::src
exprt & src()
Definition: std_expr.h:2718
can_cast_expr< ieee_float_op_exprt >
bool can_cast_expr< ieee_float_op_exprt >(const exprt &base)
Definition: std_expr.h:3833
array_comprehension_exprt::body
const exprt & body() const
Definition: std_expr.h:4456
member_exprt::compound
exprt & compound()
Definition: std_expr.h:3451
to_is_dynamic_object_expr
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: std_expr.h:1993
exprt::op1
exprt & op1()
Definition: expr.h:105
null_pointer_exprt::null_pointer_exprt
null_pointer_exprt(pointer_typet type)
Definition: std_expr.h:3991
dynamic_object_exprt::valid
const exprt & valid() const
Definition: std_expr.h:1940
to_notequal_expr
const notequal_exprt & to_notequal_expr(const exprt &expr)
Cast an exprt to an notequal_exprt.
Definition: std_expr.h:1273
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:985
binding_exprt::variablest
std::vector< symbol_exprt > variablest
Definition: std_expr.h:4123
with_exprt::old
const exprt & old() const
Definition: std_expr.h:3065
isnan_exprt::isnan_exprt
isnan_exprt(exprt op)
Definition: std_expr.h:3511
concatenation_exprt::concatenation_exprt
concatenation_exprt(operandst _operands, typet _type)
Definition: std_expr.h:4069
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
nil_exprt::nil_exprt
nil_exprt()
Definition: std_expr.h:3975
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:1986
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:1102
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:1309
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:3851
ternary_exprt::op3
const exprt & op3() const =delete
extractbit_exprt::index
exprt & index()
Definition: std_expr.h:2644
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:4147
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:1635
validation_modet
validation_modet
Definition: validation_mode.h:12
ieee_float_op_exprt::rounding_mode
const exprt & rounding_mode() const
Definition: std_expr.h:3826
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:4198
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:4120
popcount_exprt::popcount_exprt
popcount_exprt(const exprt &_op)
Definition: std_expr.h:4315
can_cast_expr< div_exprt >
bool can_cast_expr< div_exprt >(const exprt &base)
Definition: std_expr.h:1064
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1671
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:3963
let_exprt::values
const operandst & values() const
Definition: std_expr.h:4240
vector_exprt::vector_exprt
vector_exprt(operandst _operands, vector_typet _type)
Definition: std_expr.h:1533
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:793
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
bitand_exprt
Bit-wise AND.
Definition: std_expr.h:2459
if_exprt::cond
const exprt & cond() const
Definition: std_expr.h:2986
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:1963
object_descriptor_exprt::object
const exprt & object() const
Definition: std_expr.h:1863
let_exprt::let_exprt
let_exprt(binding_exprt::variablest variables, operandst values, const exprt &where)
Definition: std_expr.h:4167
div_exprt::dividend
const exprt & dividend() const
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1045
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
index_designatort
Definition: std_expr.h:3129
complex_exprt::imag
const exprt & imag() const
Definition: std_expr.h:1698
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:1811
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:3766
to_isinf_expr
const isinf_exprt & to_isinf_expr(const exprt &expr)
Cast an exprt to a isinf_exprt.
Definition: std_expr.h:3579
array_list_exprt::type
const array_typet & type() const
Definition: std_expr.h:1485
div_exprt::divisor
exprt & divisor()
The divisor of a division is the number the dividend is being divided by.
Definition: std_expr.h:1051
isinf_exprt::isinf_exprt
isinf_exprt(exprt op)
Definition: std_expr.h:3556
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:939
div_exprt::dividend
exprt & dividend()
The dividend of a division is the number that is being divided.
Definition: std_expr.h:1039
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3112
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3233
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:2661
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:3260
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt(exprt _object)
Definition: std_expr.h:1843
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:835
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:4028
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2292
can_cast_expr< index_exprt >
bool can_cast_expr< index_exprt >(const exprt &base)
Definition: std_expr.h:1331
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:1575
bitnot_exprt
Bit-wise negation of bit-vectors.
Definition: std_expr.h:2343
to_isnan_expr
const isnan_exprt & to_isnan_expr(const exprt &expr)
Cast an exprt to a isnan_exprt.
Definition: std_expr.h:3534
extractbit_exprt
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:2628
to_bitxor_expr
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
Definition: std_expr.h:2444
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:2408
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3404
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:2632
equal_exprt::equal_exprt
equal_exprt(exprt _lhs, exprt _rhs)
Definition: std_expr.h:1192
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
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:2495
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:1749
type_exprt
An expression denoting a type.
Definition: std_expr.h:3869
can_cast_expr< array_comprehension_exprt >
bool can_cast_expr< array_comprehension_exprt >(const exprt &base)
Definition: std_expr.h:4468
plus_exprt::plus_exprt
plus_exprt(operandst _operands, typet _type)
Definition: std_expr.h:897
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:4358
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:3821
equal_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:1197
infinity_exprt::infinity_exprt
infinity_exprt(typet _type)
Definition: std_expr.h:4113
binding_exprt::binding_exprt
binding_exprt(irep_idt _id, const variablest &_variables, exprt _where, typet _type)
construct the binding expression
Definition: std_expr.h:4126
dynamic_object_exprt::valid
exprt & valid()
Definition: std_expr.h:1935
array_typet
Arrays with given size.
Definition: std_types.h:964
object_descriptor_exprt::offset
const exprt & offset() const
Definition: std_expr.h:1875
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
binding_exprt::where
exprt & where()
Definition: std_expr.h:4152
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:2281
to_extractbits_expr
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
Definition: std_expr.h:2766
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:2088
extractbits_exprt::extractbits_exprt
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
Definition: std_expr.h:2704
bitand_exprt::bitand_exprt
bitand_exprt(const exprt &_op0, exprt _op1)
Definition: std_expr.h:2462
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:2868
shift_exprt::distance
exprt & distance()
Definition: std_expr.h:2515
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:4608
isinf_exprt
Evaluates to true if the operand is infinite.
Definition: std_expr.h:3553
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:2116
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:4598
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:3270
replication_exprt::replication_exprt
replication_exprt(const constant_exprt &_times, const exprt &_src)
Definition: std_expr.h:4001
to_implies_expr
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
Definition: std_expr.h:2225
ieee_float_op_exprt::lhs
const exprt & lhs() const
Definition: std_expr.h:3806
member_exprt::member_exprt
member_exprt(exprt op, const struct_typet::componentt &c)
Definition: std_expr.h:3413
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:3878
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:2639
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
can_cast_expr< popcount_exprt >
bool can_cast_expr< popcount_exprt >(const exprt &base)
Definition: std_expr.h:4322
ashr_exprt
Arithmetic right shift.
Definition: std_expr.h:2598
if_exprt::false_case
const exprt & false_case() const
Definition: std_expr.h:3006
lshr_exprt::lshr_exprt
lshr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2621
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
floatbv_typecast_exprt::op
const exprt & op() const
Definition: std_expr.h:2083
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:2015
extractbit_exprt::index
const exprt & index() const
Definition: std_expr.h:2654
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:1784
ieee_float_op_exprt::lhs
exprt & lhs()
Definition: std_expr.h:3801
can_cast_expr< shift_exprt >
bool can_cast_expr< shift_exprt >(const exprt &base)
Definition: std_expr.h:2527
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:1230
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:157
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:3653
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:4461
to_bitnot_expr
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
Definition: std_expr.h:2368
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:4553
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:3789
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1, exprt op2)
Definition: std_expr.h:2252
unary_exprt::op
exprt & op()
Definition: std_expr.h:286
multi_ary_exprt::op2
const exprt & op2() const
Definition: std_expr.h:847
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
concatenation_exprt::concatenation_exprt
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
Definition: std_expr.h:4074
can_cast_expr< object_descriptor_exprt >
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: std_expr.h:1882
can_cast_expr< typecast_exprt >
bool can_cast_expr< typecast_exprt >(const exprt &base)
Definition: std_expr.h:2031
bswap_exprt
The byte swap expression.
Definition: std_expr.h:470
shift_exprt::distance
const exprt & distance() const
Definition: std_expr.h:2520
can_cast_expr< vector_exprt >
bool can_cast_expr< vector_exprt >(const exprt &base)
Definition: std_expr.h:1540
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
complex_exprt::complex_exprt
complex_exprt(exprt _real, exprt _imag, complex_typet _type)
Definition: std_expr.h:1674
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
implies_exprt
Boolean implication.
Definition: std_expr.h:2199
let_exprt::where
const exprt & where() const
convenience accessor for binding().where()
Definition: std_expr.h:4264
shift_exprt::op
const exprt & op() const
Definition: std_expr.h:2510
can_cast_expr< if_exprt >
bool can_cast_expr< if_exprt >(const exprt &base)
Definition: std_expr.h:3013
array_of_exprt::what
const exprt & what() const
Definition: std_expr.h:1389
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:1477
constant_exprt::constant_exprt
constant_exprt(const irep_idt &_value, typet _type)
Definition: std_expr.h:3908
extractbits_exprt
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:2696
can_cast_expr< constant_exprt >
bool can_cast_expr< constant_exprt >(const exprt &base)
Definition: std_expr.h:3928
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:1705
or_exprt::or_exprt
or_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2247
let_exprt::values
operandst & values()
Definition: std_expr.h:4235
ashr_exprt::ashr_exprt
ashr_exprt(exprt _src, const std::size_t _distance)
Definition: std_expr.h:2606
false_exprt::false_exprt
false_exprt()
Definition: std_expr.h:3966
nullary_exprt::op2
const exprt & op2() const =delete
ieee_float_op_exprt::rhs
const exprt & rhs() const
Definition: std_expr.h:3816
index_exprt
Array index operator.
Definition: std_expr.h:1292
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2785
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4307
object_descriptor_exprt::object_descriptor_exprt
object_descriptor_exprt()
Definition: std_expr.h:1834
address_of_exprt::object
const exprt & object() const
Definition: std_expr.h:2800
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2012
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:1787
array_comprehension_exprt
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:4421
replication_exprt::times
const constant_exprt & times() const
Definition: std_expr.h:4011
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1858
true_exprt
The Boolean constant true.
Definition: std_expr.h:3954
constant_exprt
A constant literal expression.
Definition: std_expr.h:3905
can_cast_expr< extractbits_exprt >
bool can_cast_expr< extractbits_exprt >(const exprt &base)
Definition: std_expr.h:2750
ieee_float_equal_exprt
IEEE-floating-point equality.
Definition: std_expr.h:3688
binary_exprt::op2
const exprt & op2() const =delete
multi_ary_exprt::op0
exprt & op0()
Definition: std_expr.h:811
unary_exprt::op3
const exprt & op3() const =delete
implies_exprt::implies_exprt
implies_exprt(exprt op0, exprt op1)
Definition: std_expr.h:2202
index_designatort::index
exprt & index()
Definition: std_expr.h:3142
can_cast_expr< struct_exprt >
bool can_cast_expr< struct_exprt >(const exprt &base)
Definition: std_expr.h:1645
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:866
let_exprt::where
exprt & where()
convenience accessor for binding().where()
Definition: std_expr.h:4258
let_exprt::binding
binding_exprt & binding()
Definition: std_expr.h:4193
multi_ary_exprt::multi_ary_exprt
multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
Definition: std_expr.h:799
union_exprt::set_component_number
void set_component_number(std::size_t component_number)
Definition: std_expr.h:1590
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:3919
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
let_exprt::symbol
const symbol_exprt & symbol() const
convenience accessor for the symbol of a single binding
Definition: std_expr.h:4212
with_exprt::where
exprt & where()
Definition: std_expr.h:3070
array_of_exprt::array_of_exprt
array_of_exprt(exprt _what, array_typet _type)
Definition: std_expr.h:1369
to_member_designator
const member_designatort & to_member_designator(const exprt &expr)
Cast an exprt to an member_designatort.
Definition: std_expr.h:3214
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1431
can_cast_expr< with_exprt >
bool can_cast_expr< with_exprt >(const exprt &base)
Definition: std_expr.h:3092
ieee_float_op_exprt::rhs
exprt & rhs()
Definition: std_expr.h:3811
isnormal_exprt
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:3643
member_exprt::set_component_name
void set_component_name(const irep_idt &component_name)
Definition: std_expr.h:3424
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:4310
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:2346
with_exprt::new_value
const exprt & new_value() const
Definition: std_expr.h:3085
to_extractbit_expr
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
Definition: std_expr.h:2677
to_shl_expr
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
Definition: std_expr.h:2580
as_const.h
extractbit_exprt::src
const exprt & src() const
Definition: std_expr.h:2649
let_exprt
A let expression.
Definition: std_expr.h:4164
to_and_expr
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
Definition: std_expr.h:2184
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:3792
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:1057
complex_exprt::real
exprt real()
Definition: std_expr.h:1683
expr_protectedt
Base class for all expressions.
Definition: expr.h:366
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1656
validation_modet::INVARIANT
can_cast_expr< member_designatort >
bool can_cast_expr< member_designatort >(const exprt &base)
Definition: std_expr.h:3198
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:1099
dereference_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_expr.h:2911
can_cast_expr< update_exprt >
bool can_cast_expr< update_exprt >(const exprt &base)
Definition: std_expr.h:3282
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3165
shl_exprt
Left shift.
Definition: std_expr.h:2560
can_cast_expr< dereference_exprt >
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: std_expr.h:2928
can_cast_expr< ieee_float_equal_exprt >
bool can_cast_expr< ieee_float_equal_exprt >(const exprt &base)
Definition: std_expr.h:3701
isnan_exprt
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3508
can_cast_expr< dynamic_object_exprt >
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: std_expr.h:1947
can_cast_expr< mult_exprt >
bool can_cast_expr< mult_exprt >(const exprt &base)
Definition: std_expr.h:995
not_exprt
Boolean negation.
Definition: std_expr.h:2842
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
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:1870
multi_ary_exprt::op3
const exprt & op3() const
Definition: std_expr.h:853