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