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