cprover
std_code.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing statements in a program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_CODE_H
11 #define CPROVER_UTIL_STD_CODE_H
12 
13 #include <list>
14 
15 #include "expr_cast.h"
16 #include "invariant.h"
17 #include "std_expr.h"
18 #include "validate.h"
19 #include "validate_code.h"
20 
32 class codet:public exprt
33 {
34 public:
38  explicit codet(const irep_idt &statement) : exprt(ID_code, empty_typet())
39  {
40  set_statement(statement);
41  }
42 
43  codet(const irep_idt &statement, source_locationt loc)
44  : exprt(ID_code, empty_typet(), std::move(loc))
45  {
46  set_statement(statement);
47  }
48 
53  explicit codet(const irep_idt &statement, operandst _op) : codet(statement)
54  {
55  operands() = std::move(_op);
56  }
57 
58  codet(const irep_idt &statement, operandst op, source_locationt loc)
59  : codet(statement, std::move(loc))
60  {
61  operands() = std::move(op);
62  }
63 
64  void set_statement(const irep_idt &statement)
65  {
66  set(ID_statement, statement);
67  }
68 
69  const irep_idt &get_statement() const
70  {
71  return get(ID_statement);
72  }
73 
75  const codet &first_statement() const;
77  const codet &last_statement() const;
78 
87  static void check(const codet &, const validation_modet)
88  {
89  }
90 
100  static void validate(
101  const codet &code,
102  const namespacet &,
104  {
105  check_code(code, vm);
106  }
107 
116  static void validate_full(
117  const codet &code,
118  const namespacet &,
120  {
121  check_code(code, vm);
122  }
123 
124  using exprt::op0;
125  using exprt::op1;
126  using exprt::op2;
127  using exprt::op3;
128 };
129 
130 namespace detail // NOLINT
131 {
132 
133 template<typename Tag>
134 inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
135 {
136  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
137  {
138  return ptr->get_statement() == tag;
139  }
140  return false;
141 }
142 
143 } // namespace detail
144 
145 template<> inline bool can_cast_expr<codet>(const exprt &base)
146 {
147  return base.id()==ID_code;
148 }
149 
150 // to_code has no validation other than checking the id(), so no validate_expr
151 // is provided for codet
152 
153 inline const codet &to_code(const exprt &expr)
154 {
155  PRECONDITION(expr.id() == ID_code);
156  return static_cast<const codet &>(expr);
157 }
158 
159 inline codet &to_code(exprt &expr)
160 {
161  PRECONDITION(expr.id() == ID_code);
162  return static_cast<codet &>(expr);
163 }
164 
167 class code_blockt:public codet
168 {
169 public:
170  code_blockt():codet(ID_block)
171  {
172  }
173 
174  typedef std::vector<codet> code_operandst;
175 
177  {
178  return (code_operandst &)get_sub();
179  }
180 
181  const code_operandst &statements() const
182  {
183  return (const code_operandst &)get_sub();
184  }
185 
186  static code_blockt from_list(const std::list<codet> &_list)
187  {
188  code_blockt result;
189  auto &s=result.statements();
190  s.reserve(_list.size());
191  for(const auto &c : _list)
192  s.push_back(c);
193  return result;
194  }
195 
196  explicit code_blockt(const std::vector<codet> &_statements)
197  : codet(ID_block, (const std::vector<exprt> &)_statements)
198  {
199  }
200 
201  explicit code_blockt(std::vector<codet> &&_statements)
202  : codet(ID_block, std::move((std::vector<exprt> &&) _statements))
203  {
204  }
205 
206  void add(const codet &code)
207  {
208  add_to_operands(code);
209  }
210 
211  void add(codet &&code)
212  {
213  add_to_operands(std::move(code));
214  }
215 
216  void add(codet code, source_locationt loc)
217  {
218  code.add_source_location().swap(loc);
219  add(std::move(code));
220  }
221 
222  void append(const code_blockt &extra_block);
223 
224  // This is the closing '}' or 'END' at the end of a block
226  {
227  return static_cast<const source_locationt &>(find(ID_C_end_location));
228  }
229 
231 
232  static void validate_full(
233  const codet &code,
234  const namespacet &ns,
236  {
237  for(const auto &statement : code.operands())
238  {
239  DATA_CHECK(
240  vm, code.id() == ID_code, "code block must be made up of codet");
241  validate_full_code(to_code(statement), ns, vm);
242  }
243  }
244 };
245 
246 template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
247 {
248  return detail::can_cast_code_impl(base, ID_block);
249 }
250 
251 // to_code_block has no validation other than checking the statement(), so no
252 // validate_expr is provided for code_blockt
253 
254 inline const code_blockt &to_code_block(const codet &code)
255 {
256  PRECONDITION(code.get_statement() == ID_block);
257  return static_cast<const code_blockt &>(code);
258 }
259 
261 {
262  PRECONDITION(code.get_statement() == ID_block);
263  return static_cast<code_blockt &>(code);
264 }
265 
267 class code_skipt:public codet
268 {
269 public:
270  code_skipt():codet(ID_skip)
271  {
272  }
273 
274 protected:
275  using codet::op0;
276  using codet::op1;
277  using codet::op2;
278  using codet::op3;
279 };
280 
281 template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
282 {
283  return detail::can_cast_code_impl(base, ID_skip);
284 }
285 
286 // there is no to_code_skip, so no validate_expr is provided for code_skipt
287 
292 class code_assignt:public codet
293 {
294 public:
295  code_assignt():codet(ID_assign)
296  {
297  operands().resize(2);
298  }
299 
301  : codet(ID_assign, {std::move(lhs), std::move(rhs)})
302  {
303  }
304 
306  : codet(ID_assign, {std::move(lhs), std::move(rhs)}, std::move(loc))
307  {
308  }
309 
311  {
312  return op0();
313  }
314 
316  {
317  return op1();
318  }
319 
320  const exprt &lhs() const
321  {
322  return op0();
323  }
324 
325  const exprt &rhs() const
326  {
327  return op1();
328  }
329 
330  static void check(
331  const codet &code,
333  {
334  DATA_CHECK(
335  vm, code.operands().size() == 2, "assignment must have two operands");
336  }
337 
338  static void validate(
339  const codet &code,
340  const namespacet &,
342  {
343  check(code, vm);
344 
345  DATA_CHECK(
346  vm,
347  code.op0().type() == code.op1().type(),
348  "lhs and rhs of assignment must have same type");
349  }
350 
351  static void validate_full(
352  const codet &code,
353  const namespacet &ns,
355  {
356  for(const exprt &op : code.operands())
357  {
358  validate_full_expr(op, ns, vm);
359  }
360 
361  validate(code, ns, vm);
362  }
363 
364 protected:
365  using codet::op0;
366  using codet::op1;
367  using codet::op2;
368  using codet::op3;
369 };
370 
371 template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
372 {
373  return detail::can_cast_code_impl(base, ID_assign);
374 }
375 
376 inline void validate_expr(const code_assignt & x)
377 {
379 }
380 
381 inline const code_assignt &to_code_assign(const codet &code)
382 {
383  PRECONDITION(code.get_statement() == ID_assign);
384  code_assignt::check(code);
385  return static_cast<const code_assignt &>(code);
386 }
387 
389 {
390  PRECONDITION(code.get_statement() == ID_assign);
391  code_assignt::check(code);
392  return static_cast<code_assignt &>(code);
393 }
394 
399 class code_declt:public codet
400 {
401 public:
402  explicit code_declt(symbol_exprt symbol) : codet(ID_decl, {std::move(symbol)})
403  {
404  }
405 
407  {
408  return static_cast<symbol_exprt &>(op0());
409  }
410 
411  const symbol_exprt &symbol() const
412  {
413  return static_cast<const symbol_exprt &>(op0());
414  }
415 
416  const irep_idt &get_identifier() const
417  {
418  return symbol().get_identifier();
419  }
420 
426  {
427  if(operands().size() < 2)
428  return {};
429  return {op1()};
430  }
431 
437  {
438  if(!initial_value)
439  {
440  operands().resize(1);
441  }
442  else if(operands().size() < 2)
443  {
444  PRECONDITION(operands().size() == 1);
445  add_to_operands(std::move(*initial_value));
446  }
447  else
448  {
449  op1() = std::move(*initial_value);
450  }
451  }
452 
453  static void check(
454  const codet &code,
456  {
457  // will be size()==1 in the future
458  DATA_CHECK(
459  vm,
460  code.operands().size() >= 1,
461  "declaration must have one or more operands");
462  DATA_CHECK(
463  vm,
464  code.op0().id() == ID_symbol,
465  "declaring a non-symbol: " +
467  }
468 };
469 
470 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
471 {
472  return detail::can_cast_code_impl(base, ID_decl);
473 }
474 
475 inline void validate_expr(const code_declt &x)
476 {
478 }
479 
480 inline const code_declt &to_code_decl(const codet &code)
481 {
482  PRECONDITION(code.get_statement() == ID_decl);
483  code_declt::check(code);
484  return static_cast<const code_declt &>(code);
485 }
486 
488 {
489  PRECONDITION(code.get_statement() == ID_decl);
490  code_declt::check(code);
491  return static_cast<code_declt &>(code);
492 }
493 
496 class code_deadt:public codet
497 {
498 public:
499  explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)})
500  {
501  }
502 
504  {
505  return static_cast<symbol_exprt &>(op0());
506  }
507 
508  const symbol_exprt &symbol() const
509  {
510  return static_cast<const symbol_exprt &>(op0());
511  }
512 
513  const irep_idt &get_identifier() const
514  {
515  return symbol().get_identifier();
516  }
517 
518  static void check(
519  const codet &code,
521  {
522  DATA_CHECK(
523  vm,
524  code.operands().size() == 1,
525  "removal (code_deadt) must have one operand");
526  DATA_CHECK(
527  vm,
528  code.op0().id() == ID_symbol,
529  "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
530  }
531 
532 protected:
533  using codet::op0;
534  using codet::op1;
535  using codet::op2;
536  using codet::op3;
537 };
538 
539 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
540 {
541  return detail::can_cast_code_impl(base, ID_dead);
542 }
543 
544 inline void validate_expr(const code_deadt &x)
545 {
547 }
548 
549 inline const code_deadt &to_code_dead(const codet &code)
550 {
551  PRECONDITION(code.get_statement() == ID_dead);
552  code_deadt::check(code);
553  return static_cast<const code_deadt &>(code);
554 }
555 
557 {
558  PRECONDITION(code.get_statement() == ID_dead);
559  code_deadt::check(code);
560  return static_cast<code_deadt &>(code);
561 }
562 
564 class code_assumet:public codet
565 {
566 public:
567  explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)})
568  {
569  }
570 
571  const exprt &assumption() const
572  {
573  return op0();
574  }
575 
577  {
578  return op0();
579  }
580 
581 protected:
582  using codet::op0;
583  using codet::op1;
584  using codet::op2;
585  using codet::op3;
586 };
587 
588 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
589 {
590  return detail::can_cast_code_impl(base, ID_assume);
591 }
592 
593 inline void validate_expr(const code_assumet &x)
594 {
595  validate_operands(x, 1, "assume must have one operand");
596 }
597 
598 inline const code_assumet &to_code_assume(const codet &code)
599 {
600  PRECONDITION(code.get_statement() == ID_assume);
601  const code_assumet &ret = static_cast<const code_assumet &>(code);
602  validate_expr(ret);
603  return ret;
604 }
605 
607 {
608  PRECONDITION(code.get_statement() == ID_assume);
609  code_assumet &ret = static_cast<code_assumet &>(code);
610  validate_expr(ret);
611  return ret;
612 }
613 
616 class code_assertt:public codet
617 {
618 public:
619  explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)})
620  {
621  }
622 
623  const exprt &assertion() const
624  {
625  return op0();
626  }
627 
629  {
630  return op0();
631  }
632 
633 protected:
634  using codet::op0;
635  using codet::op1;
636  using codet::op2;
637  using codet::op3;
638 };
639 
640 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
641 {
642  return detail::can_cast_code_impl(base, ID_assert);
643 }
644 
645 inline void validate_expr(const code_assertt &x)
646 {
647  validate_operands(x, 1, "assert must have one operand");
648 }
649 
650 inline const code_assertt &to_code_assert(const codet &code)
651 {
652  PRECONDITION(code.get_statement() == ID_assert);
653  const code_assertt &ret = static_cast<const code_assertt &>(code);
654  validate_expr(ret);
655  return ret;
656 }
657 
659 {
660  PRECONDITION(code.get_statement() == ID_assert);
661  code_assertt &ret = static_cast<code_assertt &>(code);
662  validate_expr(ret);
663  return ret;
664 }
665 
674 class code_inputt : public codet
675 {
676 public:
680  explicit code_inputt(
681  std::vector<exprt> arguments,
682  optionalt<source_locationt> location = {});
683 
692  code_inputt(
693  const irep_idt &description,
694  exprt expression,
695  optionalt<source_locationt> location = {});
696 
697  static void check(
698  const codet &code,
700 };
701 
702 template <>
703 inline bool can_cast_expr<code_inputt>(const exprt &base)
704 {
705  return detail::can_cast_code_impl(base, ID_input);
706 }
707 
708 inline void validate_expr(const code_inputt &input)
709 {
710  code_inputt::check(input);
711 }
712 
721 class code_outputt : public codet
722 {
723 public:
727  explicit code_outputt(
728  std::vector<exprt> arguments,
729  optionalt<source_locationt> location = {});
730 
738  code_outputt(
739  const irep_idt &description,
740  exprt expression,
741  optionalt<source_locationt> location = {});
742 
743  static void check(
744  const codet &code,
746 };
747 
748 template <>
749 inline bool can_cast_expr<code_outputt>(const exprt &base)
750 {
751  return detail::can_cast_code_impl(base, ID_output);
752 }
753 
754 inline void validate_expr(const code_outputt &output)
755 {
756  code_outputt::check(output);
757 }
758 
772  const exprt &condition, const source_locationt &source_location);
773 
776 {
777 public:
779  code_ifthenelset(exprt condition, codet then_code, codet else_code)
780  : codet(
781  ID_ifthenelse,
782  {std::move(condition), std::move(then_code), std::move(else_code)})
783  {
784  }
785 
787  code_ifthenelset(exprt condition, codet then_code)
788  : codet(
789  ID_ifthenelse,
790  {std::move(condition), std::move(then_code), nil_exprt()})
791  {
792  }
793 
794  const exprt &cond() const
795  {
796  return op0();
797  }
798 
800  {
801  return op0();
802  }
803 
804  const codet &then_case() const
805  {
806  return static_cast<const codet &>(op1());
807  }
808 
809  bool has_else_case() const
810  {
811  return op2().is_not_nil();
812  }
813 
814  const codet &else_case() const
815  {
816  return static_cast<const codet &>(op2());
817  }
818 
820  {
821  return static_cast<codet &>(op1());
822  }
823 
825  {
826  return static_cast<codet &>(op2());
827  }
828 
829 protected:
830  using codet::op0;
831  using codet::op1;
832  using codet::op2;
833  using codet::op3;
834 };
835 
836 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
837 {
838  return detail::can_cast_code_impl(base, ID_ifthenelse);
839 }
840 
841 inline void validate_expr(const code_ifthenelset &x)
842 {
843  validate_operands(x, 3, "if-then-else must have three operands");
844 }
845 
846 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
847 {
848  PRECONDITION(code.get_statement() == ID_ifthenelse);
849  const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);
850  validate_expr(ret);
851  return ret;
852 }
853 
855 {
856  PRECONDITION(code.get_statement() == ID_ifthenelse);
857  code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);
858  validate_expr(ret);
859  return ret;
860 }
861 
863 class code_switcht:public codet
864 {
865 public:
866  code_switcht(exprt _value, codet _body)
867  : codet(ID_switch, {std::move(_value), std::move(_body)})
868  {
869  }
870 
871  const exprt &value() const
872  {
873  return op0();
874  }
875 
877  {
878  return op0();
879  }
880 
881  const codet &body() const
882  {
883  return to_code(op1());
884  }
885 
887  {
888  return static_cast<codet &>(op1());
889  }
890 
891 protected:
892  using codet::op0;
893  using codet::op1;
894  using codet::op2;
895  using codet::op3;
896 };
897 
898 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
899 {
900  return detail::can_cast_code_impl(base, ID_switch);
901 }
902 
903 inline void validate_expr(const code_switcht &x)
904 {
905  validate_operands(x, 2, "switch must have two operands");
906 }
907 
908 inline const code_switcht &to_code_switch(const codet &code)
909 {
910  PRECONDITION(code.get_statement() == ID_switch);
911  const code_switcht &ret = static_cast<const code_switcht &>(code);
912  validate_expr(ret);
913  return ret;
914 }
915 
917 {
918  PRECONDITION(code.get_statement() == ID_switch);
919  code_switcht &ret = static_cast<code_switcht &>(code);
920  validate_expr(ret);
921  return ret;
922 }
923 
925 class code_whilet:public codet
926 {
927 public:
928  code_whilet(exprt _cond, codet _body)
929  : codet(ID_while, {std::move(_cond), std::move(_body)})
930  {
931  }
932 
933  const exprt &cond() const
934  {
935  return op0();
936  }
937 
939  {
940  return op0();
941  }
942 
943  const codet &body() const
944  {
945  return to_code(op1());
946  }
947 
949  {
950  return static_cast<codet &>(op1());
951  }
952 
953 protected:
954  using codet::op0;
955  using codet::op1;
956  using codet::op2;
957  using codet::op3;
958 };
959 
960 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
961 {
962  return detail::can_cast_code_impl(base, ID_while);
963 }
964 
965 inline void validate_expr(const code_whilet &x)
966 {
967  validate_operands(x, 2, "while must have two operands");
968 }
969 
970 inline const code_whilet &to_code_while(const codet &code)
971 {
972  PRECONDITION(code.get_statement() == ID_while);
973  const code_whilet &ret = static_cast<const code_whilet &>(code);
974  validate_expr(ret);
975  return ret;
976 }
977 
979 {
980  PRECONDITION(code.get_statement() == ID_while);
981  code_whilet &ret = static_cast<code_whilet &>(code);
982  validate_expr(ret);
983  return ret;
984 }
985 
987 class code_dowhilet:public codet
988 {
989 public:
990  code_dowhilet(exprt _cond, codet _body)
991  : codet(ID_dowhile, {std::move(_cond), std::move(_body)})
992  {
993  }
994 
995  const exprt &cond() const
996  {
997  return op0();
998  }
999 
1001  {
1002  return op0();
1003  }
1004 
1005  const codet &body() const
1006  {
1007  return to_code(op1());
1008  }
1009 
1011  {
1012  return static_cast<codet &>(op1());
1013  }
1014 
1015 protected:
1016  using codet::op0;
1017  using codet::op1;
1018  using codet::op2;
1019  using codet::op3;
1020 };
1021 
1022 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
1023 {
1024  return detail::can_cast_code_impl(base, ID_dowhile);
1025 }
1026 
1027 inline void validate_expr(const code_dowhilet &x)
1028 {
1029  validate_operands(x, 2, "do-while must have two operands");
1030 }
1031 
1032 inline const code_dowhilet &to_code_dowhile(const codet &code)
1033 {
1034  PRECONDITION(code.get_statement() == ID_dowhile);
1035  const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);
1036  validate_expr(ret);
1037  return ret;
1038 }
1039 
1041 {
1042  PRECONDITION(code.get_statement() == ID_dowhile);
1043  code_dowhilet &ret = static_cast<code_dowhilet &>(code);
1044  validate_expr(ret);
1045  return ret;
1046 }
1047 
1049 class code_fort:public codet
1050 {
1051 public:
1054  code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
1055  : codet(
1056  ID_for,
1057  {std::move(_init),
1058  std::move(_cond),
1059  std::move(_iter),
1060  std::move(_body)})
1061  {
1062  }
1063 
1064  // nil or a statement
1065  const exprt &init() const
1066  {
1067  return op0();
1068  }
1069 
1071  {
1072  return op0();
1073  }
1074 
1075  const exprt &cond() const
1076  {
1077  return op1();
1078  }
1079 
1081  {
1082  return op1();
1083  }
1084 
1085  const exprt &iter() const
1086  {
1087  return op2();
1088  }
1089 
1091  {
1092  return op2();
1093  }
1094 
1095  const codet &body() const
1096  {
1097  return to_code(op3());
1098  }
1099 
1101  {
1102  return static_cast<codet &>(op3());
1103  }
1104 
1116  exprt start_index,
1117  exprt end_index,
1118  symbol_exprt loop_index,
1119  codet body,
1120  source_locationt location);
1121 
1122 protected:
1123  using codet::op0;
1124  using codet::op1;
1125  using codet::op2;
1126  using codet::op3;
1127 };
1128 
1129 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
1130 {
1131  return detail::can_cast_code_impl(base, ID_for);
1132 }
1133 
1134 inline void validate_expr(const code_fort &x)
1135 {
1136  validate_operands(x, 4, "for must have four operands");
1137 }
1138 
1139 inline const code_fort &to_code_for(const codet &code)
1140 {
1141  PRECONDITION(code.get_statement() == ID_for);
1142  const code_fort &ret = static_cast<const code_fort &>(code);
1143  validate_expr(ret);
1144  return ret;
1145 }
1146 
1148 {
1149  PRECONDITION(code.get_statement() == ID_for);
1150  code_fort &ret = static_cast<code_fort &>(code);
1151  validate_expr(ret);
1152  return ret;
1153 }
1154 
1156 class code_gotot:public codet
1157 {
1158 public:
1159  explicit code_gotot(const irep_idt &label):codet(ID_goto)
1160  {
1161  set_destination(label);
1162  }
1163 
1164  void set_destination(const irep_idt &label)
1165  {
1166  set(ID_destination, label);
1167  }
1168 
1169  const irep_idt &get_destination() const
1170  {
1171  return get(ID_destination);
1172  }
1173 
1174 protected:
1175  using codet::op0;
1176  using codet::op1;
1177  using codet::op2;
1178  using codet::op3;
1179 };
1180 
1181 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
1182 {
1183  return detail::can_cast_code_impl(base, ID_goto);
1184 }
1185 
1186 inline void validate_expr(const code_gotot &x)
1187 {
1188  validate_operands(x, 0, "goto must not have operands");
1189 }
1190 
1191 inline const code_gotot &to_code_goto(const codet &code)
1192 {
1193  PRECONDITION(code.get_statement() == ID_goto);
1194  const code_gotot &ret = static_cast<const code_gotot &>(code);
1195  validate_expr(ret);
1196  return ret;
1197 }
1198 
1200 {
1201  PRECONDITION(code.get_statement() == ID_goto);
1202  code_gotot &ret = static_cast<code_gotot &>(code);
1203  validate_expr(ret);
1204  return ret;
1205 }
1206 
1213 {
1214 public:
1215  explicit code_function_callt(exprt _function)
1216  : codet(
1217  ID_function_call,
1218  {nil_exprt(), std::move(_function), exprt(ID_arguments)})
1219  {
1220  }
1221 
1223 
1224  code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
1225  : codet(
1226  ID_function_call,
1227  {std::move(_lhs), std::move(_function), exprt(ID_arguments)})
1228  {
1229  arguments() = std::move(_arguments);
1230  }
1231 
1232  code_function_callt(exprt _function, argumentst _arguments)
1233  : code_function_callt(std::move(_function))
1234  {
1235  arguments() = std::move(_arguments);
1236  }
1237 
1239  {
1240  return op0();
1241  }
1242 
1243  const exprt &lhs() const
1244  {
1245  return op0();
1246  }
1247 
1248  exprt &function()
1249  {
1250  return op1();
1251  }
1252 
1253  const exprt &function() const
1254  {
1255  return op1();
1256  }
1257 
1259  {
1260  return op2().operands();
1261  }
1262 
1263  const argumentst &arguments() const
1264  {
1265  return op2().operands();
1266  }
1267 
1268  static void check(
1269  const codet &code,
1271  {
1272  DATA_CHECK(
1273  vm,
1274  code.operands().size() == 3,
1275  "function calls must have three operands:\n1) expression to store the "
1276  "returned values\n2) the function being called\n3) the vector of "
1277  "arguments");
1278  }
1279 
1280  static void validate(
1281  const codet &code,
1282  const namespacet &,
1284  {
1285  check(code, vm);
1286 
1287  if(code.op0().id() != ID_nil)
1288  DATA_CHECK(
1289  vm,
1290  code.op0().type() == to_code_type(code.op1().type()).return_type(),
1291  "function returns expression of wrong type");
1292  }
1293 
1294  static void validate_full(
1295  const codet &code,
1296  const namespacet &ns,
1298  {
1299  for(const exprt &op : code.operands())
1300  {
1301  validate_full_expr(op, ns, vm);
1302  }
1303 
1304  validate(code, ns, vm);
1305  }
1306 
1307 protected:
1308  using codet::op0;
1309  using codet::op1;
1310  using codet::op2;
1311  using codet::op3;
1312 };
1313 
1314 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
1315 {
1316  return detail::can_cast_code_impl(base, ID_function_call);
1317 }
1318 
1319 inline void validate_expr(const code_function_callt &x)
1320 {
1322 }
1323 
1325 {
1326  PRECONDITION(code.get_statement() == ID_function_call);
1328  return static_cast<const code_function_callt &>(code);
1329 }
1330 
1332 {
1333  PRECONDITION(code.get_statement() == ID_function_call);
1335  return static_cast<code_function_callt &>(code);
1336 }
1337 
1339 class code_returnt:public codet
1340 {
1341 public:
1342  code_returnt() : codet(ID_return, {nil_exprt()})
1343  {
1344  }
1345 
1346  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
1347  {
1348  }
1349 
1350  const exprt &return_value() const
1351  {
1352  return op0();
1353  }
1354 
1356  {
1357  return op0();
1358  }
1359 
1360  bool has_return_value() const
1361  {
1362  return return_value().is_not_nil();
1363  }
1364 
1365  static void check(
1366  const codet &code,
1368  {
1369  DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
1370  }
1371 
1372 protected:
1373  using codet::op0;
1374  using codet::op1;
1375  using codet::op2;
1376  using codet::op3;
1377 };
1378 
1379 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
1380 {
1381  return detail::can_cast_code_impl(base, ID_return);
1382 }
1383 
1384 inline void validate_expr(const code_returnt &x)
1385 {
1387 }
1388 
1389 inline const code_returnt &to_code_return(const codet &code)
1390 {
1391  PRECONDITION(code.get_statement() == ID_return);
1392  code_returnt::check(code);
1393  return static_cast<const code_returnt &>(code);
1394 }
1395 
1397 {
1398  PRECONDITION(code.get_statement() == ID_return);
1399  code_returnt::check(code);
1400  return static_cast<code_returnt &>(code);
1401 }
1402 
1404 class code_labelt:public codet
1405 {
1406 public:
1407  code_labelt(const irep_idt &_label, codet _code)
1408  : codet(ID_label, {std::move(_code)})
1409  {
1410  set_label(_label);
1411  }
1412 
1413  const irep_idt &get_label() const
1414  {
1415  return get(ID_label);
1416  }
1417 
1418  void set_label(const irep_idt &label)
1419  {
1420  set(ID_label, label);
1421  }
1422 
1424  {
1425  return static_cast<codet &>(op0());
1426  }
1427 
1428  const codet &code() const
1429  {
1430  return static_cast<const codet &>(op0());
1431  }
1432 
1433 protected:
1434  using codet::op0;
1435  using codet::op1;
1436  using codet::op2;
1437  using codet::op3;
1438 };
1439 
1440 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
1441 {
1442  return detail::can_cast_code_impl(base, ID_label);
1443 }
1444 
1445 inline void validate_expr(const code_labelt &x)
1446 {
1447  validate_operands(x, 1, "label must have one operand");
1448 }
1449 
1450 inline const code_labelt &to_code_label(const codet &code)
1451 {
1452  PRECONDITION(code.get_statement() == ID_label);
1453  const code_labelt &ret = static_cast<const code_labelt &>(code);
1454  validate_expr(ret);
1455  return ret;
1456 }
1457 
1459 {
1460  PRECONDITION(code.get_statement() == ID_label);
1461  code_labelt &ret = static_cast<code_labelt &>(code);
1462  validate_expr(ret);
1463  return ret;
1464 }
1465 
1469 {
1470 public:
1471  code_switch_caset(exprt _case_op, codet _code)
1472  : codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
1473  {
1474  }
1475 
1476  bool is_default() const
1477  {
1478  return get_bool(ID_default);
1479  }
1480 
1482  {
1483  return set(ID_default, true);
1484  }
1485 
1486  const exprt &case_op() const
1487  {
1488  return op0();
1489  }
1490 
1492  {
1493  return op0();
1494  }
1495 
1497  {
1498  return static_cast<codet &>(op1());
1499  }
1500 
1501  const codet &code() const
1502  {
1503  return static_cast<const codet &>(op1());
1504  }
1505 
1506 protected:
1507  using codet::op0;
1508  using codet::op1;
1509  using codet::op2;
1510  using codet::op3;
1511 };
1512 
1513 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1514 {
1515  return detail::can_cast_code_impl(base, ID_switch_case);
1516 }
1517 
1518 inline void validate_expr(const code_switch_caset &x)
1519 {
1520  validate_operands(x, 2, "switch-case must have two operands");
1521 }
1522 
1523 inline const code_switch_caset &to_code_switch_case(const codet &code)
1524 {
1525  PRECONDITION(code.get_statement() == ID_switch_case);
1526  const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);
1527  validate_expr(ret);
1528  return ret;
1529 }
1530 
1532 {
1533  PRECONDITION(code.get_statement() == ID_switch_case);
1534  code_switch_caset &ret = static_cast<code_switch_caset &>(code);
1535  validate_expr(ret);
1536  return ret;
1537 }
1538 
1543 {
1544 public:
1546  : codet(
1547  ID_gcc_switch_case_range,
1548  {std::move(_lower), std::move(_upper), std::move(_code)})
1549  {
1550  }
1551 
1553  const exprt &lower() const
1554  {
1555  return op0();
1556  }
1557 
1560  {
1561  return op0();
1562  }
1563 
1565  const exprt &upper() const
1566  {
1567  return op1();
1568  }
1569 
1572  {
1573  return op1();
1574  }
1575 
1578  {
1579  return static_cast<codet &>(op2());
1580  }
1581 
1583  const codet &code() const
1584  {
1585  return static_cast<const codet &>(op2());
1586  }
1587 
1588 protected:
1589  using codet::op0;
1590  using codet::op1;
1591  using codet::op2;
1592  using codet::op3;
1593 };
1594 
1595 template <>
1597 {
1598  return detail::can_cast_code_impl(base, ID_gcc_switch_case_range);
1599 }
1600 
1602 {
1603  validate_operands(x, 3, "gcc-switch-case-range must have three operands");
1604 }
1605 
1606 inline const code_gcc_switch_case_ranget &
1608 {
1609  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1610  const code_gcc_switch_case_ranget &ret =
1611  static_cast<const code_gcc_switch_case_ranget &>(code);
1612  validate_expr(ret);
1613  return ret;
1614 }
1615 
1617 {
1618  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1620  static_cast<code_gcc_switch_case_ranget &>(code);
1621  validate_expr(ret);
1622  return ret;
1623 }
1624 
1627 class code_breakt:public codet
1628 {
1629 public:
1630  code_breakt():codet(ID_break)
1631  {
1632  }
1633 
1634 protected:
1635  using codet::op0;
1636  using codet::op1;
1637  using codet::op2;
1638  using codet::op3;
1639 };
1640 
1641 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1642 {
1643  return detail::can_cast_code_impl(base, ID_break);
1644 }
1645 
1646 // to_code_break only checks the code statement, so no validate_expr is
1647 // provided for code_breakt
1648 
1649 inline const code_breakt &to_code_break(const codet &code)
1650 {
1651  PRECONDITION(code.get_statement() == ID_break);
1652  return static_cast<const code_breakt &>(code);
1653 }
1654 
1656 {
1657  PRECONDITION(code.get_statement() == ID_break);
1658  return static_cast<code_breakt &>(code);
1659 }
1660 
1663 class code_continuet:public codet
1664 {
1665 public:
1666  code_continuet():codet(ID_continue)
1667  {
1668  }
1669 
1670 protected:
1671  using codet::op0;
1672  using codet::op1;
1673  using codet::op2;
1674  using codet::op3;
1675 };
1676 
1677 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1678 {
1679  return detail::can_cast_code_impl(base, ID_continue);
1680 }
1681 
1682 // to_code_continue only checks the code statement, so no validate_expr is
1683 // provided for code_continuet
1684 
1685 inline const code_continuet &to_code_continue(const codet &code)
1686 {
1687  PRECONDITION(code.get_statement() == ID_continue);
1688  return static_cast<const code_continuet &>(code);
1689 }
1690 
1692 {
1693  PRECONDITION(code.get_statement() == ID_continue);
1694  return static_cast<code_continuet &>(code);
1695 }
1696 
1698 class code_asmt:public codet
1699 {
1700 public:
1701  code_asmt():codet(ID_asm)
1702  {
1703  }
1704 
1705  explicit code_asmt(exprt expr) : codet(ID_asm, {std::move(expr)})
1706  {
1707  }
1708 
1709  const irep_idt &get_flavor() const
1710  {
1711  return get(ID_flavor);
1712  }
1713 
1714  void set_flavor(const irep_idt &f)
1715  {
1716  set(ID_flavor, f);
1717  }
1718 };
1719 
1720 template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1721 {
1722  return detail::can_cast_code_impl(base, ID_asm);
1723 }
1724 
1725 // to_code_asm only checks the code statement, so no validate_expr is
1726 // provided for code_asmt
1727 
1729 {
1730  PRECONDITION(code.get_statement() == ID_asm);
1731  return static_cast<code_asmt &>(code);
1732 }
1733 
1734 inline const code_asmt &to_code_asm(const codet &code)
1735 {
1736  PRECONDITION(code.get_statement() == ID_asm);
1737  return static_cast<const code_asmt &>(code);
1738 }
1739 
1742 class code_asm_gcct : public code_asmt
1743 {
1744 public:
1746  {
1747  set_flavor(ID_gcc);
1748  operands().resize(5);
1749  }
1750 
1752  {
1753  return op0();
1754  }
1755 
1756  const exprt &asm_text() const
1757  {
1758  return op0();
1759  }
1760 
1762  {
1763  return op1();
1764  }
1765 
1766  const exprt &outputs() const
1767  {
1768  return op1();
1769  }
1770 
1772  {
1773  return op2();
1774  }
1775 
1776  const exprt &inputs() const
1777  {
1778  return op2();
1779  }
1780 
1782  {
1783  return op3();
1784  }
1785 
1786  const exprt &clobbers() const
1787  {
1788  return op3();
1789  }
1790 
1792  {
1793  return operands()[4];
1794  }
1795 
1796  const exprt &labels() const
1797  {
1798  return operands()[4];
1799  }
1800 
1801 protected:
1802  using code_asmt::op0;
1803  using code_asmt::op1;
1804  using code_asmt::op2;
1805  using code_asmt::op3;
1806 };
1807 
1808 template <>
1809 inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
1810 {
1811  return detail::can_cast_code_impl(base, ID_asm);
1812 }
1813 
1814 inline void validate_expr(const code_asm_gcct &x)
1815 {
1816  validate_operands(x, 5, "code_asm_gcc must have five operands");
1817 }
1818 
1820 {
1821  PRECONDITION(code.get_statement() == ID_asm);
1822  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1823  code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
1824  validate_expr(ret);
1825  return ret;
1826 }
1827 
1828 inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
1829 {
1830  PRECONDITION(code.get_statement() == ID_asm);
1831  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1832  const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
1833  validate_expr(ret);
1834  return ret;
1835 }
1836 
1840 {
1841 public:
1842  explicit code_expressiont(exprt expr)
1843  : codet(ID_expression, {std::move(expr)})
1844  {
1845  }
1846 
1847  const exprt &expression() const
1848  {
1849  return op0();
1850  }
1851 
1853  {
1854  return op0();
1855  }
1856 
1857 protected:
1858  using codet::op0;
1859  using codet::op1;
1860  using codet::op2;
1861  using codet::op3;
1862 };
1863 
1864 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1865 {
1866  return detail::can_cast_code_impl(base, ID_expression);
1867 }
1868 
1869 inline void validate_expr(const code_expressiont &x)
1870 {
1871  validate_operands(x, 1, "expression statement must have one operand");
1872 }
1873 
1875 {
1876  PRECONDITION(code.get_statement() == ID_expression);
1877  code_expressiont &ret = static_cast<code_expressiont &>(code);
1878  validate_expr(ret);
1879  return ret;
1880 }
1881 
1882 inline const code_expressiont &to_code_expression(const codet &code)
1883 {
1884  PRECONDITION(code.get_statement() == ID_expression);
1885  const code_expressiont &ret = static_cast<const code_expressiont &>(code);
1886  validate_expr(ret);
1887  return ret;
1888 }
1889 
1895 class side_effect_exprt : public exprt
1896 {
1897 public:
1899  const irep_idt &statement,
1900  operandst _operands,
1901  typet _type,
1902  source_locationt loc)
1903  : exprt(ID_side_effect, std::move(_type), std::move(loc))
1904  {
1905  set_statement(statement);
1906  operands() = std::move(_operands);
1907  }
1908 
1910  const irep_idt &statement,
1911  typet _type,
1912  source_locationt loc)
1913  : exprt(ID_side_effect, std::move(_type), std::move(loc))
1914  {
1915  set_statement(statement);
1916  }
1917 
1918  const irep_idt &get_statement() const
1919  {
1920  return get(ID_statement);
1921  }
1922 
1923  void set_statement(const irep_idt &statement)
1924  {
1925  return set(ID_statement, statement);
1926  }
1927 };
1928 
1929 namespace detail // NOLINT
1930 {
1931 
1932 template<typename Tag>
1933 inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1934 {
1935  if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1936  {
1937  return ptr->get_statement() == tag;
1938  }
1939  return false;
1940 }
1941 
1942 } // namespace detail
1943 
1944 template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1945 {
1946  return base.id()==ID_side_effect;
1947 }
1948 
1949 // to_side_effect_expr only checks the id, so no validate_expr is provided for
1950 // side_effect_exprt
1951 
1953 {
1954  PRECONDITION(expr.id() == ID_side_effect);
1955  return static_cast<side_effect_exprt &>(expr);
1956 }
1957 
1958 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1959 {
1960  PRECONDITION(expr.id() == ID_side_effect);
1961  return static_cast<const side_effect_exprt &>(expr);
1962 }
1963 
1966 {
1967 public:
1969  : side_effect_exprt(ID_nondet, std::move(_type), std::move(loc))
1970  {
1971  set_nullable(true);
1972  }
1973 
1974  void set_nullable(bool nullable)
1975  {
1976  set(ID_is_nondet_nullable, nullable);
1977  }
1978 
1979  bool get_nullable() const
1980  {
1981  return get_bool(ID_is_nondet_nullable);
1982  }
1983 };
1984 
1985 template<>
1987 {
1988  return detail::can_cast_side_effect_expr_impl(base, ID_nondet);
1989 }
1990 
1991 // to_side_effect_expr_nondet only checks the id, so no validate_expr is
1992 // provided for side_effect_expr_nondett
1993 
1995 {
1996  auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1997  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1998  return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
1999 }
2000 
2002  const exprt &expr)
2003 {
2004  const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
2005  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2006  return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
2007 }
2008 
2011 {
2012 public:
2016  const exprt &_lhs,
2017  const exprt &_rhs,
2018  const source_locationt &loc)
2019  : side_effect_exprt(ID_assign, {_lhs, _rhs}, _lhs.type(), loc)
2020  {
2021  }
2022 
2025  exprt _lhs,
2026  exprt _rhs,
2027  typet _type,
2028  source_locationt loc)
2030  ID_assign,
2031  {std::move(_lhs), std::move(_rhs)},
2032  std::move(_type),
2033  std::move(loc))
2034  {
2035  }
2036 
2038  {
2039  return op0();
2040  }
2041 
2042  const exprt &lhs() const
2043  {
2044  return op0();
2045  }
2046 
2048  {
2049  return op1();
2050  }
2051 
2052  const exprt &rhs() const
2053  {
2054  return op1();
2055  }
2056 };
2057 
2058 template <>
2060 {
2061  return detail::can_cast_side_effect_expr_impl(base, ID_assign);
2062 }
2063 
2065 {
2066  auto &side_effect_expr_assign = to_side_effect_expr(expr);
2067  PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2068  return static_cast<side_effect_expr_assignt &>(side_effect_expr_assign);
2069 }
2070 
2071 inline const side_effect_expr_assignt &
2073 {
2074  const auto &side_effect_expr_assign = to_side_effect_expr(expr);
2075  PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2076  return static_cast<const side_effect_expr_assignt &>(side_effect_expr_assign);
2077 }
2078 
2081 {
2082 public:
2085  codet _code,
2086  typet _type,
2087  source_locationt loc)
2089  ID_statement_expression,
2090  {std::move(_code)},
2091  std::move(_type),
2092  std::move(loc))
2093  {
2094  }
2095 
2097  {
2098  return to_code(op0());
2099  }
2100 
2101  const codet &statement() const
2102  {
2103  return to_code(op0());
2104  }
2105 };
2106 
2107 template <>
2108 inline bool
2110 {
2111  return detail::can_cast_side_effect_expr_impl(base, ID_statement_expression);
2112 }
2113 
2116 {
2117  auto &side_effect_expr_statement_expression = to_side_effect_expr(expr);
2118  PRECONDITION(
2119  side_effect_expr_statement_expression.get_statement() ==
2120  ID_statement_expression);
2121  return static_cast<side_effect_expr_statement_expressiont &>(
2122  side_effect_expr_statement_expression);
2123 }
2124 
2127 {
2128  const auto &side_effect_expr_statement_expression = to_side_effect_expr(expr);
2129  PRECONDITION(
2130  side_effect_expr_statement_expression.get_statement() ==
2131  ID_statement_expression);
2132  return static_cast<const side_effect_expr_statement_expressiont &>(
2133  side_effect_expr_statement_expression);
2134 }
2135 
2138 {
2139 public:
2141  exprt _function,
2142  exprt::operandst _arguments,
2143  typet _type,
2144  source_locationt loc)
2146  ID_function_call,
2147  {std::move(_function),
2148  multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}}},
2149  std::move(_type),
2150  std::move(loc))
2151  {
2152  }
2153 
2154  exprt &function()
2155  {
2156  return op0();
2157  }
2158 
2159  const exprt &function() const
2160  {
2161  return op0();
2162  }
2163 
2165  {
2166  return op1().operands();
2167  }
2168 
2170  {
2171  return op1().operands();
2172  }
2173 };
2174 
2175 template<>
2177 {
2178  return detail::can_cast_side_effect_expr_impl(base, ID_function_call);
2179 }
2180 
2181 // to_side_effect_expr_function_call only checks the id, so no validate_expr is
2182 // provided for side_effect_expr_function_callt
2183 
2186 {
2187  PRECONDITION(expr.id() == ID_side_effect);
2188  PRECONDITION(expr.get(ID_statement) == ID_function_call);
2189  return static_cast<side_effect_expr_function_callt &>(expr);
2190 }
2191 
2194 {
2195  PRECONDITION(expr.id() == ID_side_effect);
2196  PRECONDITION(expr.get(ID_statement) == ID_function_call);
2197  return static_cast<const side_effect_expr_function_callt &>(expr);
2198 }
2199 
2203 {
2204 public:
2206  irept exception_list,
2207  typet type,
2208  source_locationt loc)
2209  : side_effect_exprt(ID_throw, std::move(type), std::move(loc))
2210  {
2211  set(ID_exception_list, std::move(exception_list));
2212  }
2213 };
2214 
2215 template<>
2217 {
2218  return detail::can_cast_side_effect_expr_impl(base, ID_throw);
2219 }
2220 
2221 // to_side_effect_expr_throw only checks the id, so no validate_expr is
2222 // provided for side_effect_expr_throwt
2223 
2225 {
2226  PRECONDITION(expr.id() == ID_side_effect);
2227  PRECONDITION(expr.get(ID_statement) == ID_throw);
2228  return static_cast<side_effect_expr_throwt &>(expr);
2229 }
2230 
2232  const exprt &expr)
2233 {
2234  PRECONDITION(expr.id() == ID_side_effect);
2235  PRECONDITION(expr.get(ID_statement) == ID_throw);
2236  return static_cast<const side_effect_expr_throwt &>(expr);
2237 }
2238 
2251 {
2252 public:
2253  code_push_catcht():codet(ID_push_catch)
2254  {
2255  set(ID_exception_list, irept(ID_exception_list));
2256  }
2257 
2259  {
2260  public:
2262  {
2263  }
2264 
2265  explicit exception_list_entryt(const irep_idt &tag)
2266  {
2267  set(ID_tag, tag);
2268  }
2269 
2270  exception_list_entryt(const irep_idt &tag, const irep_idt &label)
2271  {
2272  set(ID_tag, tag);
2273  set(ID_label, label);
2274  }
2275 
2276  void set_tag(const irep_idt &tag)
2277  {
2278  set(ID_tag, tag);
2279  }
2280 
2281  const irep_idt &get_tag() const {
2282  return get(ID_tag);
2283  }
2284 
2285  void set_label(const irep_idt &label)
2286  {
2287  set(ID_label, label);
2288  }
2289 
2290  const irep_idt &get_label() const {
2291  return get(ID_label);
2292  }
2293  };
2294 
2295  typedef std::vector<exception_list_entryt> exception_listt;
2296 
2298  const irep_idt &tag,
2299  const irep_idt &label):
2300  codet(ID_push_catch)
2301  {
2302  set(ID_exception_list, irept(ID_exception_list));
2303  exception_list().push_back(exception_list_entryt(tag, label));
2304  }
2305 
2307  return (exception_listt &)find(ID_exception_list).get_sub();
2308  }
2309 
2311  return (const exception_listt &)find(ID_exception_list).get_sub();
2312  }
2313 
2314 protected:
2315  using codet::op0;
2316  using codet::op1;
2317  using codet::op2;
2318  using codet::op3;
2319 };
2320 
2321 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
2322 {
2323  return detail::can_cast_code_impl(base, ID_push_catch);
2324 }
2325 
2326 // to_code_push_catch only checks the code statement, so no validate_expr is
2327 // provided for code_push_catcht
2328 
2330 {
2331  PRECONDITION(code.get_statement() == ID_push_catch);
2332  return static_cast<code_push_catcht &>(code);
2333 }
2334 
2335 static inline const code_push_catcht &to_code_push_catch(const codet &code)
2336 {
2337  PRECONDITION(code.get_statement() == ID_push_catch);
2338  return static_cast<const code_push_catcht &>(code);
2339 }
2340 
2345 {
2346 public:
2347  code_pop_catcht():codet(ID_pop_catch)
2348  {
2349  }
2350 
2351 protected:
2352  using codet::op0;
2353  using codet::op1;
2354  using codet::op2;
2355  using codet::op3;
2356 };
2357 
2358 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
2359 {
2360  return detail::can_cast_code_impl(base, ID_pop_catch);
2361 }
2362 
2363 // to_code_pop_catch only checks the code statement, so no validate_expr is
2364 // provided for code_pop_catcht
2365 
2367 {
2368  PRECONDITION(code.get_statement() == ID_pop_catch);
2369  return static_cast<code_pop_catcht &>(code);
2370 }
2371 
2372 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
2373 {
2374  PRECONDITION(code.get_statement() == ID_pop_catch);
2375  return static_cast<const code_pop_catcht &>(code);
2376 }
2377 
2382 {
2383  public:
2384  code_landingpadt():codet(ID_exception_landingpad)
2385  {
2386  operands().resize(1);
2387  }
2388 
2390  : codet(ID_exception_landingpad, {std::move(catch_expr)})
2391  {
2392  }
2393 
2394  const exprt &catch_expr() const
2395  {
2396  return op0();
2397  }
2399  {
2400  return op0();
2401  }
2402 
2403 protected:
2404  using codet::op0;
2405  using codet::op1;
2406  using codet::op2;
2407  using codet::op3;
2408 };
2409 
2410 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
2411 {
2412  return detail::can_cast_code_impl(base, ID_exception_landingpad);
2413 }
2414 
2415 // to_code_landingpad only checks the code statement, so no validate_expr is
2416 // provided for code_landingpadt
2417 
2419 {
2420  PRECONDITION(code.get_statement() == ID_exception_landingpad);
2421  return static_cast<code_landingpadt &>(code);
2422 }
2423 
2424 static inline const code_landingpadt &to_code_landingpad(const codet &code)
2425 {
2426  PRECONDITION(code.get_statement() == ID_exception_landingpad);
2427  return static_cast<const code_landingpadt &>(code);
2428 }
2429 
2432 {
2433 public:
2435  explicit code_try_catcht(codet _try_code)
2436  : codet(ID_try_catch, {std::move(_try_code)})
2437  {
2438  }
2439 
2441  {
2442  return static_cast<codet &>(op0());
2443  }
2444 
2445  const codet &try_code() const
2446  {
2447  return static_cast<const codet &>(op0());
2448  }
2449 
2451  {
2452  PRECONDITION((2 * i + 2) < operands().size());
2453  return to_code_decl(to_code(operands()[2*i+1]));
2454  }
2455 
2456  const code_declt &get_catch_decl(unsigned i) const
2457  {
2458  PRECONDITION((2 * i + 2) < operands().size());
2459  return to_code_decl(to_code(operands()[2*i+1]));
2460  }
2461 
2462  codet &get_catch_code(unsigned i)
2463  {
2464  PRECONDITION((2 * i + 2) < operands().size());
2465  return to_code(operands()[2*i+2]);
2466  }
2467 
2468  const codet &get_catch_code(unsigned i) const
2469  {
2470  PRECONDITION((2 * i + 2) < operands().size());
2471  return to_code(operands()[2*i+2]);
2472  }
2473 
2474  void add_catch(const code_declt &to_catch, const codet &code_catch)
2475  {
2476  add_to_operands(to_catch, code_catch);
2477  }
2478 
2479 protected:
2480  using codet::op0;
2481  using codet::op1;
2482  using codet::op2;
2483  using codet::op3;
2484 };
2485 
2486 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
2487 {
2488  return detail::can_cast_code_impl(base, ID_try_catch);
2489 }
2490 
2491 inline void validate_expr(const code_try_catcht &x)
2492 {
2493  validate_operands(x, 3, "try-catch must have three or more operands", true);
2494 }
2495 
2496 inline const code_try_catcht &to_code_try_catch(const codet &code)
2497 {
2498  PRECONDITION(code.get_statement() == ID_try_catch);
2499  const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);
2500  validate_expr(ret);
2501  return ret;
2502 }
2503 
2505 {
2506  PRECONDITION(code.get_statement() == ID_try_catch);
2507  code_try_catcht &ret = static_cast<code_try_catcht &>(code);
2508  validate_expr(ret);
2509  return ret;
2510 }
2511 
2516 {
2517 public:
2519  const std::vector<irep_idt> &parameter_identifiers,
2520  code_blockt _block)
2521  : codet(ID_function_body, {std::move(_block)})
2522  {
2523  set_parameter_identifiers(parameter_identifiers);
2524  }
2525 
2527  {
2528  return to_code_block(to_code(op0()));
2529  }
2530 
2531  const code_blockt &block() const
2532  {
2533  return to_code_block(to_code(op0()));
2534  }
2535 
2536  std::vector<irep_idt> get_parameter_identifiers() const;
2537  void set_parameter_identifiers(const std::vector<irep_idt> &);
2538 
2539 protected:
2540  using codet::op0;
2541  using codet::op1;
2542  using codet::op2;
2543  using codet::op3;
2544 };
2545 
2547 {
2548  PRECONDITION(code.get_statement() == ID_function_body);
2550  code.operands().size() == 1, "code_function_body must have one operand");
2551  return static_cast<const code_function_bodyt &>(code);
2552 }
2553 
2555 {
2556  PRECONDITION(code.get_statement() == ID_function_body);
2558  code.operands().size() == 1, "code_function_body must have one operand");
2559  return static_cast<code_function_bodyt &>(code);
2560 }
2561 
2562 #endif // CPROVER_UTIL_STD_CODE_H
codet representation of an inline assembler statement, for the gcc flavor.
Definition: std_code.h:1743
exprt & outputs()
Definition: std_code.h:1761
const exprt & asm_text() const
Definition: std_code.h:1756
exprt & asm_text()
Definition: std_code.h:1751
const exprt & clobbers() const
Definition: std_code.h:1786
const exprt & inputs() const
Definition: std_code.h:1776
exprt & inputs()
Definition: std_code.h:1771
const exprt & labels() const
Definition: std_code.h:1796
const exprt & outputs() const
Definition: std_code.h:1766
exprt & labels()
Definition: std_code.h:1791
exprt & clobbers()
Definition: std_code.h:1781
codet representation of an inline assembler statement.
Definition: std_code.h:1699
code_asmt(exprt expr)
Definition: std_code.h:1705
const irep_idt & get_flavor() const
Definition: std_code.h:1709
void set_flavor(const irep_idt &f)
Definition: std_code.h:1714
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
code_assertt(exprt expr)
Definition: std_code.h:619
const exprt & assertion() const
Definition: std_code.h:623
exprt & op0()
Definition: expr.h:99
exprt & assertion()
Definition: std_code.h:628
A codet representing an assignment in the program.
Definition: std_code.h:293
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:338
exprt & rhs()
Definition: std_code.h:315
const exprt & rhs() const
Definition: std_code.h:325
exprt & op1()
Definition: expr.h:102
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:330
exprt & lhs()
Definition: std_code.h:310
const exprt & lhs() const
Definition: std_code.h:320
exprt & op0()
Definition: expr.h:99
code_assignt(exprt lhs, exprt rhs, source_locationt loc)
Definition: std_code.h:305
code_assignt(exprt lhs, exprt rhs)
Definition: std_code.h:300
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:351
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
const exprt & assumption() const
Definition: std_code.h:571
code_assumet(exprt expr)
Definition: std_code.h:567
exprt & op0()
Definition: expr.h:99
exprt & assumption()
Definition: std_code.h:576
A codet representing sequential composition of program statements.
Definition: std_code.h:168
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:186
source_locationt end_location() const
Definition: std_code.h:225
void add(codet code, source_locationt loc)
Definition: std_code.h:216
void add(codet &&code)
Definition: std_code.h:211
code_blockt(std::vector< codet > &&_statements)
Definition: std_code.h:201
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
code_blockt(const std::vector< codet > &_statements)
Definition: std_code.h:196
const code_operandst & statements() const
Definition: std_code.h:181
void add(const codet &code)
Definition: std_code.h:206
code_operandst & statements()
Definition: std_code.h:176
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:232
std::vector< codet > code_operandst
Definition: std_code.h:174
codet & find_last_statement()
Definition: std_code.cpp:99
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1664
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:497
symbol_exprt & symbol()
Definition: std_code.h:503
code_deadt(symbol_exprt symbol)
Definition: std_code.h:499
exprt & op0()
Definition: expr.h:99
const irep_idt & get_identifier() const
Definition: std_code.h:513
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:518
const symbol_exprt & symbol() const
Definition: std_code.h:508
A codet representing the declaration of a local variable.
Definition: std_code.h:400
const irep_idt & get_identifier() const
Definition: std_code.h:416
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:436
symbol_exprt & symbol()
Definition: std_code.h:406
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition: std_code.h:425
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:453
code_declt(symbol_exprt symbol)
Definition: std_code.h:402
const symbol_exprt & symbol() const
Definition: std_code.h:411
codet representation of a do while statement.
Definition: std_code.h:988
const exprt & cond() const
Definition: std_code.h:995
code_dowhilet(exprt _cond, codet _body)
Definition: std_code.h:990
exprt & op1()
Definition: expr.h:102
codet & body()
Definition: std_code.h:1010
exprt & cond()
Definition: std_code.h:1000
const codet & body() const
Definition: std_code.h:1005
exprt & op0()
Definition: expr.h:99
codet representation of an expression statement.
Definition: std_code.h:1840
exprt & expression()
Definition: std_code.h:1852
code_expressiont(exprt expr)
Definition: std_code.h:1842
const exprt & expression() const
Definition: std_code.h:1847
exprt & op0()
Definition: expr.h:99
codet representation of a for statement.
Definition: std_code.h:1050
const exprt & init() const
Definition: std_code.h:1065
exprt & iter()
Definition: std_code.h:1090
const exprt & iter() const
Definition: std_code.h:1085
exprt & op3()
Definition: expr.h:108
codet & body()
Definition: std_code.h:1100
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter,...
Definition: std_code.h:1054
static code_fort from_index_bounds(exprt start_index, exprt end_index, symbol_exprt loop_index, codet body, source_locationt location)
Produce a code_fort representing:
Definition: std_code.cpp:214
exprt & op0()
Definition: expr.h:99
const exprt & cond() const
Definition: std_code.h:1075
exprt & cond()
Definition: std_code.h:1080
exprt & init()
Definition: std_code.h:1070
const codet & body() const
Definition: std_code.h:1095
This class is used to interface between a language frontend and goto-convert – it communicates the id...
Definition: std_code.h:2516
const code_blockt & block() const
Definition: std_code.h:2531
code_function_bodyt(const std::vector< irep_idt > &parameter_identifiers, code_blockt _block)
Definition: std_code.h:2518
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:136
code_blockt & block()
Definition: std_code.h:2526
exprt & op0()
Definition: expr.h:99
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:146
codet representation of a function call statement.
Definition: std_code.h:1213
const argumentst & arguments() const
Definition: std_code.h:1263
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1294
argumentst & arguments()
Definition: std_code.h:1258
exprt & op1()
Definition: expr.h:102
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1280
exprt & op2()
Definition: expr.h:105
exprt & op0()
Definition: expr.h:99
code_function_callt(exprt _function)
Definition: std_code.h:1215
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1268
const exprt & lhs() const
Definition: std_code.h:1243
code_function_callt(exprt _function, argumentst _arguments)
Definition: std_code.h:1232
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
Definition: std_code.h:1224
exprt::operandst argumentst
Definition: std_code.h:1222
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1543
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1577
const exprt & lower() const
lower bound of range
Definition: std_code.h:1553
exprt & upper()
upper bound of range
Definition: std_code.h:1571
code_gcc_switch_case_ranget(exprt _lower, exprt _upper, codet _code)
Definition: std_code.h:1545
const codet & code() const
the statement to be executed when the case applies
Definition: std_code.h:1583
const exprt & upper() const
upper bound of range
Definition: std_code.h:1565
exprt & lower()
lower bound of range
Definition: std_code.h:1559
codet representation of a goto statement.
Definition: std_code.h:1157
const irep_idt & get_destination() const
Definition: std_code.h:1169
code_gotot(const irep_idt &label)
Definition: std_code.h:1159
void set_destination(const irep_idt &label)
Definition: std_code.h:1164
codet representation of an if-then-else statement.
Definition: std_code.h:776
const codet & then_case() const
Definition: std_code.h:804
code_ifthenelset(exprt condition, codet then_code)
An if condition then then_code statement (no "else" case).
Definition: std_code.h:787
exprt & op1()
Definition: expr.h:102
exprt & cond()
Definition: std_code.h:799
exprt & op2()
Definition: expr.h:105
codet & then_case()
Definition: std_code.h:819
exprt & op0()
Definition: expr.h:99
const exprt & cond() const
Definition: std_code.h:794
code_ifthenelset(exprt condition, codet then_code, codet else_code)
An if condition then then_code else else_code statement.
Definition: std_code.h:779
codet & else_case()
Definition: std_code.h:824
const codet & else_case() const
Definition: std_code.h:814
bool has_else_case() const
Definition: std_code.h:809
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:675
code_inputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_input in user code.
Definition: std_code.cpp:158
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:180
codet representation of a label for branch targets.
Definition: std_code.h:1405
const irep_idt & get_label() const
Definition: std_code.h:1413
codet & code()
Definition: std_code.h:1423
code_labelt(const irep_idt &_label, codet _code)
Definition: std_code.h:1407
exprt & op0()
Definition: expr.h:99
const codet & code() const
Definition: std_code.h:1428
void set_label(const irep_idt &label)
Definition: std_code.h:1418
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:2382
exprt & catch_expr()
Definition: std_code.h:2398
const exprt & catch_expr() const
Definition: std_code.h:2394
exprt & op0()
Definition: expr.h:99
code_landingpadt(exprt catch_expr)
Definition: std_code.h:2389
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:722
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:208
code_outputt(std::vector< exprt > arguments, optionalt< source_locationt > location={})
This constructor is for support of calls to __CPROVER_output in user code.
Definition: std_code.cpp:186
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:2345
void set_tag(const irep_idt &tag)
Definition: std_code.h:2276
exception_list_entryt(const irep_idt &tag)
Definition: std_code.h:2265
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:2270
void set_label(const irep_idt &label)
Definition: std_code.h:2285
const irep_idt & get_tag() const
Definition: std_code.h:2281
const irep_idt & get_label() const
Definition: std_code.h:2290
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:2251
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2295
code_push_catcht(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:2297
exception_listt & exception_list()
Definition: std_code.h:2306
const exception_listt & exception_list() const
Definition: std_code.h:2310
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1365
code_returnt(exprt _op)
Definition: std_code.h:1346
exprt & return_value()
Definition: std_code.h:1355
const exprt & return_value() const
Definition: std_code.h:1350
exprt & op0()
Definition: expr.h:99
bool has_return_value() const
Definition: std_code.h:1360
A codet representing a skip statement.
Definition: std_code.h:268
code_skipt()
Definition: std_code.h:270
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet & code()
Definition: std_code.h:1496
const exprt & case_op() const
Definition: std_code.h:1486
exprt & case_op()
Definition: std_code.h:1491
exprt & op1()
Definition: expr.h:102
const codet & code() const
Definition: std_code.h:1501
exprt & op0()
Definition: expr.h:99
void set_default()
Definition: std_code.h:1481
code_switch_caset(exprt _case_op, codet _code)
Definition: std_code.h:1471
bool is_default() const
Definition: std_code.h:1476
codet representing a switch statement.
Definition: std_code.h:864
code_switcht(exprt _value, codet _body)
Definition: std_code.h:866
codet & body()
Definition: std_code.h:886
exprt & op1()
Definition: expr.h:102
const exprt & value() const
Definition: std_code.h:871
const codet & body() const
Definition: std_code.h:881
exprt & op0()
Definition: expr.h:99
exprt & value()
Definition: std_code.h:876
codet representation of a try/catch block.
Definition: std_code.h:2432
codet & get_catch_code(unsigned i)
Definition: std_code.h:2462
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:2468
codet & try_code()
Definition: std_code.h:2440
exprt & op0()
Definition: expr.h:99
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
Definition: std_code.h:2435
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:2456
code_declt & get_catch_decl(unsigned i)
Definition: std_code.h:2450
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:2474
const codet & try_code() const
Definition: std_code.h:2445
const typet & return_type() const
Definition: std_types.h:645
codet representing a while statement.
Definition: std_code.h:926
const exprt & cond() const
Definition: std_code.h:933
code_whilet(exprt _cond, codet _body)
Definition: std_code.h:928
const codet & body() const
Definition: std_code.h:943
exprt & op1()
Definition: expr.h:102
codet & body()
Definition: std_code.h:948
exprt & op0()
Definition: expr.h:99
exprt & cond()
Definition: std_code.h:938
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
codet(const irep_idt &statement, source_locationt loc)
Definition: std_code.h:43
exprt & op3()
Definition: expr.h:108
static void validate_full(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed (full check, including checks of all subexpressions)
Definition: std_code.h:116
codet(const irep_idt &statement)
Definition: std_code.h:38
exprt & op1()
Definition: expr.h:102
exprt & op2()
Definition: expr.h:105
codet(const irep_idt &statement, operandst op, source_locationt loc)
Definition: std_code.h:58
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them.
Definition: std_code.cpp:21
exprt & op0()
Definition: expr.h:99
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed, assuming that all its enclosed statements,...
Definition: std_code.h:100
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them.
Definition: std_code.cpp:55
void set_statement(const irep_idt &statement)
Definition: std_code.h:64
const irep_idt & get_statement() const
Definition: std_code.h:69
static void check(const codet &, const validation_modet)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements,...
Definition: std_code.h:87
codet(const irep_idt &statement, operandst _op)
Definition: std_code.h:53
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
exprt & op3()
Definition: expr.h:108
exprt & op1()
Definition: expr.h:102
source_locationt & add_source_location()
Definition: expr.h:235
exprt()
Definition: expr.h:59
exprt & op2()
Definition: expr.h:105
typet & type()
Return the type of the expression.
Definition: expr.h:82
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
irept()=default
subt & get_sub()
Definition: irep.h:467
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:824
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2820
A side_effect_exprt that performs an assignment.
Definition: std_code.h:2011
const exprt & lhs() const
Definition: std_code.h:2042
const exprt & rhs() const
Definition: std_code.h:2052
side_effect_expr_assignt(exprt _lhs, exprt _rhs, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
Definition: std_code.h:2024
side_effect_expr_assignt(const exprt &_lhs, const exprt &_rhs, const source_locationt &loc)
construct an assignment side-effect, given lhs and rhs The type is copied from lhs
Definition: std_code.h:2015
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
side_effect_expr_function_callt(exprt _function, exprt::operandst _arguments, typet _type, source_locationt loc)
Definition: std_code.h:2140
const exprt::operandst & arguments() const
Definition: std_code.h:2169
exprt::operandst & arguments()
Definition: std_code.h:2164
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
void set_nullable(bool nullable)
Definition: std_code.h:1974
bool get_nullable() const
Definition: std_code.h:1979
side_effect_expr_nondett(typet _type, source_locationt loc)
Definition: std_code.h:1968
A side_effect_exprt that contains a statement.
Definition: std_code.h:2081
const codet & statement() const
Definition: std_code.h:2101
side_effect_expr_statement_expressiont(codet _code, typet _type, source_locationt loc)
construct an assignment side-effect, given lhs, rhs and the type
Definition: std_code.h:2084
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2203
side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)
Definition: std_code.h:2205
An expression containing a side effect.
Definition: std_code.h:1896
void set_statement(const irep_idt &statement)
Definition: std_code.h:1923
const irep_idt & get_statement() const
Definition: std_code.h:1918
side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)
Definition: std_code.h:1898
side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)
Definition: std_code.h:1909
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The type of an expression, extends irept.
Definition: type.h:28
Templated functions to cast to specific exprt-derived classes.
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:134
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:1933
nonstd::optional< T > optionalt
Definition: optional.h:35
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &source_location)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition: std_code.cpp:123
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition: std_code.h:2216
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition: std_code.h:836
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:846
bool can_cast_expr< code_switcht >(const exprt &base)
Definition: std_code.h:898
bool can_cast_expr< code_switch_caset >(const exprt &base)
Definition: std_code.h:1513
bool can_cast_expr< code_asmt >(const exprt &base)
Definition: std_code.h:1720
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
bool can_cast_expr< codet >(const exprt &base)
Definition: std_code.h:145
bool can_cast_expr< code_function_callt >(const exprt &base)
Definition: std_code.h:1314
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition: std_code.h:1864
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition: std_code.h:2410
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2418
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition: std_code.h:2366
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:703
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1191
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:970
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:2115
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1685
const code_function_bodyt & to_code_function_body(const codet &code)
Definition: std_code.h:2546
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:598
bool can_cast_expr< code_blockt >(const exprt &base)
Definition: std_code.h:246
bool can_cast_expr< code_breakt >(const exprt &base)
Definition: std_code.h:1641
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1986
bool can_cast_expr< code_dowhilet >(const exprt &base)
Definition: std_code.h:1022
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1523
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition: std_code.h:2486
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:749
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
bool can_cast_expr< code_assignt >(const exprt &base)
Definition: std_code.h:371
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
bool can_cast_expr< code_declt >(const exprt &base)
Definition: std_code.h:470
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
void validate_expr(const code_assignt &x)
Definition: std_code.h:376
bool can_cast_expr< code_assertt >(const exprt &base)
Definition: std_code.h:640
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1032
bool can_cast_expr< code_skipt >(const exprt &base)
Definition: std_code.h:281
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:908
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:480
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2064
bool can_cast_expr< code_returnt >(const exprt &base)
Definition: std_code.h:1379
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
Definition: std_code.h:2059
bool can_cast_expr< code_asm_gcct >(const exprt &base)
Definition: std_code.h:1809
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1874
bool can_cast_expr< code_gotot >(const exprt &base)
Definition: std_code.h:1181
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1649
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
Definition: std_code.h:2109
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2329
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:2176
bool can_cast_expr< code_whilet >(const exprt &base)
Definition: std_code.h:960
bool can_cast_expr< code_continuet >(const exprt &base)
Definition: std_code.h:1677
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:549
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:650
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1944
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition: std_code.h:2321
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1607
bool can_cast_expr< code_fort >(const exprt &base)
Definition: std_code.h:1129
bool can_cast_expr< code_deadt >(const exprt &base)
Definition: std_code.h:539
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
Definition: std_code.h:1596
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1819
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1139
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1994
bool can_cast_expr< code_labelt >(const exprt &base)
Definition: std_code.h:1440
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:2224
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition: std_code.h:2358
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2496
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1728
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
bool can_cast_expr< code_assumet >(const exprt &base)
Definition: std_code.h:588
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements,...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet