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 
428  {
429  if(operands().size() < 2)
430  return {};
431  return {op1()};
432  }
433 
439  {
440  if(!initial_value)
441  {
442  operands().resize(1);
443  }
444  else if(operands().size() < 2)
445  {
446  PRECONDITION(operands().size() == 1);
447  add_to_operands(std::move(*initial_value));
448  }
449  else
450  {
451  op1() = std::move(*initial_value);
452  }
453  }
454 
455  static void check(
456  const codet &code,
458  {
459  // will be size()==1 in the future
460  DATA_CHECK(
461  vm,
462  code.operands().size() >= 1,
463  "declaration must have one or more operands");
464  DATA_CHECK(
465  vm,
466  code.op0().id() == ID_symbol,
467  "declaring a non-symbol: " +
469  }
470 };
471 
472 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
473 {
474  return detail::can_cast_code_impl(base, ID_decl);
475 }
476 
477 inline void validate_expr(const code_declt &x)
478 {
480 }
481 
482 inline const code_declt &to_code_decl(const codet &code)
483 {
484  PRECONDITION(code.get_statement() == ID_decl);
485  code_declt::check(code);
486  return static_cast<const code_declt &>(code);
487 }
488 
490 {
491  PRECONDITION(code.get_statement() == ID_decl);
492  code_declt::check(code);
493  return static_cast<code_declt &>(code);
494 }
495 
498 class code_deadt:public codet
499 {
500 public:
501  explicit code_deadt(symbol_exprt symbol) : codet(ID_dead, {std::move(symbol)})
502  {
503  }
504 
506  {
507  return static_cast<symbol_exprt &>(op0());
508  }
509 
510  const symbol_exprt &symbol() const
511  {
512  return static_cast<const symbol_exprt &>(op0());
513  }
514 
515  const irep_idt &get_identifier() const
516  {
517  return symbol().get_identifier();
518  }
519 
520  static void check(
521  const codet &code,
523  {
524  DATA_CHECK(
525  vm,
526  code.operands().size() == 1,
527  "removal (code_deadt) must have one operand");
528  DATA_CHECK(
529  vm,
530  code.op0().id() == ID_symbol,
531  "removing a non-symbol: " + id2string(code.op0().id()) + "from scope");
532  }
533 
534 protected:
535  using codet::op0;
536  using codet::op1;
537  using codet::op2;
538  using codet::op3;
539 };
540 
541 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
542 {
543  return detail::can_cast_code_impl(base, ID_dead);
544 }
545 
546 inline void validate_expr(const code_deadt &x)
547 {
549 }
550 
551 inline const code_deadt &to_code_dead(const codet &code)
552 {
553  PRECONDITION(code.get_statement() == ID_dead);
554  code_deadt::check(code);
555  return static_cast<const code_deadt &>(code);
556 }
557 
559 {
560  PRECONDITION(code.get_statement() == ID_dead);
561  code_deadt::check(code);
562  return static_cast<code_deadt &>(code);
563 }
564 
566 class code_assumet:public codet
567 {
568 public:
569  explicit code_assumet(exprt expr) : codet(ID_assume, {std::move(expr)})
570  {
571  }
572 
573  const exprt &assumption() const
574  {
575  return op0();
576  }
577 
579  {
580  return op0();
581  }
582 
583 protected:
584  using codet::op0;
585  using codet::op1;
586  using codet::op2;
587  using codet::op3;
588 };
589 
590 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
591 {
592  return detail::can_cast_code_impl(base, ID_assume);
593 }
594 
595 inline void validate_expr(const code_assumet &x)
596 {
597  validate_operands(x, 1, "assume must have one operand");
598 }
599 
600 inline const code_assumet &to_code_assume(const codet &code)
601 {
602  PRECONDITION(code.get_statement() == ID_assume);
603  const code_assumet &ret = static_cast<const code_assumet &>(code);
604  validate_expr(ret);
605  return ret;
606 }
607 
609 {
610  PRECONDITION(code.get_statement() == ID_assume);
611  code_assumet &ret = static_cast<code_assumet &>(code);
612  validate_expr(ret);
613  return ret;
614 }
615 
618 class code_assertt:public codet
619 {
620 public:
621  explicit code_assertt(exprt expr) : codet(ID_assert, {std::move(expr)})
622  {
623  }
624 
625  const exprt &assertion() const
626  {
627  return op0();
628  }
629 
631  {
632  return op0();
633  }
634 
635 protected:
636  using codet::op0;
637  using codet::op1;
638  using codet::op2;
639  using codet::op3;
640 };
641 
642 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
643 {
644  return detail::can_cast_code_impl(base, ID_assert);
645 }
646 
647 inline void validate_expr(const code_assertt &x)
648 {
649  validate_operands(x, 1, "assert must have one operand");
650 }
651 
652 inline const code_assertt &to_code_assert(const codet &code)
653 {
654  PRECONDITION(code.get_statement() == ID_assert);
655  const code_assertt &ret = static_cast<const code_assertt &>(code);
656  validate_expr(ret);
657  return ret;
658 }
659 
661 {
662  PRECONDITION(code.get_statement() == ID_assert);
663  code_assertt &ret = static_cast<code_assertt &>(code);
664  validate_expr(ret);
665  return ret;
666 }
667 
676 class code_inputt : public codet
677 {
678 public:
682  explicit code_inputt(
683  std::vector<exprt> arguments,
684  optionalt<source_locationt> location = {});
685 
694  code_inputt(
695  const irep_idt &description,
696  exprt expression,
697  optionalt<source_locationt> location = {});
698 
699  static void check(
700  const codet &code,
702 };
703 
704 template <>
705 inline bool can_cast_expr<code_inputt>(const exprt &base)
706 {
707  return detail::can_cast_code_impl(base, ID_input);
708 }
709 
710 inline void validate_expr(const code_inputt &input)
711 {
712  code_inputt::check(input);
713 }
714 
723 class code_outputt : public codet
724 {
725 public:
729  explicit code_outputt(
730  std::vector<exprt> arguments,
731  optionalt<source_locationt> location = {});
732 
740  code_outputt(
741  const irep_idt &description,
742  exprt expression,
743  optionalt<source_locationt> location = {});
744 
745  static void check(
746  const codet &code,
748 };
749 
750 template <>
751 inline bool can_cast_expr<code_outputt>(const exprt &base)
752 {
753  return detail::can_cast_code_impl(base, ID_output);
754 }
755 
756 inline void validate_expr(const code_outputt &output)
757 {
758  code_outputt::check(output);
759 }
760 
774  const exprt &condition, const source_locationt &source_location);
775 
778 {
779 public:
781  code_ifthenelset(exprt condition, codet then_code, codet else_code)
782  : codet(
783  ID_ifthenelse,
784  {std::move(condition), std::move(then_code), std::move(else_code)})
785  {
786  }
787 
789  code_ifthenelset(exprt condition, codet then_code)
790  : codet(
791  ID_ifthenelse,
792  {std::move(condition), std::move(then_code), nil_exprt()})
793  {
794  }
795 
796  const exprt &cond() const
797  {
798  return op0();
799  }
800 
802  {
803  return op0();
804  }
805 
806  const codet &then_case() const
807  {
808  return static_cast<const codet &>(op1());
809  }
810 
811  bool has_else_case() const
812  {
813  return op2().is_not_nil();
814  }
815 
816  const codet &else_case() const
817  {
818  return static_cast<const codet &>(op2());
819  }
820 
822  {
823  return static_cast<codet &>(op1());
824  }
825 
827  {
828  return static_cast<codet &>(op2());
829  }
830 
831 protected:
832  using codet::op0;
833  using codet::op1;
834  using codet::op2;
835  using codet::op3;
836 };
837 
838 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
839 {
840  return detail::can_cast_code_impl(base, ID_ifthenelse);
841 }
842 
843 inline void validate_expr(const code_ifthenelset &x)
844 {
845  validate_operands(x, 3, "if-then-else must have three operands");
846 }
847 
848 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
849 {
850  PRECONDITION(code.get_statement() == ID_ifthenelse);
851  const code_ifthenelset &ret = static_cast<const code_ifthenelset &>(code);
852  validate_expr(ret);
853  return ret;
854 }
855 
857 {
858  PRECONDITION(code.get_statement() == ID_ifthenelse);
859  code_ifthenelset &ret = static_cast<code_ifthenelset &>(code);
860  validate_expr(ret);
861  return ret;
862 }
863 
865 class code_switcht:public codet
866 {
867 public:
868  code_switcht(exprt _value, codet _body)
869  : codet(ID_switch, {std::move(_value), std::move(_body)})
870  {
871  }
872 
873  const exprt &value() const
874  {
875  return op0();
876  }
877 
879  {
880  return op0();
881  }
882 
883  const codet &body() const
884  {
885  return to_code(op1());
886  }
887 
889  {
890  return static_cast<codet &>(op1());
891  }
892 
893 protected:
894  using codet::op0;
895  using codet::op1;
896  using codet::op2;
897  using codet::op3;
898 };
899 
900 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
901 {
902  return detail::can_cast_code_impl(base, ID_switch);
903 }
904 
905 inline void validate_expr(const code_switcht &x)
906 {
907  validate_operands(x, 2, "switch must have two operands");
908 }
909 
910 inline const code_switcht &to_code_switch(const codet &code)
911 {
912  PRECONDITION(code.get_statement() == ID_switch);
913  const code_switcht &ret = static_cast<const code_switcht &>(code);
914  validate_expr(ret);
915  return ret;
916 }
917 
919 {
920  PRECONDITION(code.get_statement() == ID_switch);
921  code_switcht &ret = static_cast<code_switcht &>(code);
922  validate_expr(ret);
923  return ret;
924 }
925 
927 class code_whilet:public codet
928 {
929 public:
930  code_whilet(exprt _cond, codet _body)
931  : codet(ID_while, {std::move(_cond), std::move(_body)})
932  {
933  }
934 
935  const exprt &cond() const
936  {
937  return op0();
938  }
939 
941  {
942  return op0();
943  }
944 
945  const codet &body() const
946  {
947  return to_code(op1());
948  }
949 
951  {
952  return static_cast<codet &>(op1());
953  }
954 
955 protected:
956  using codet::op0;
957  using codet::op1;
958  using codet::op2;
959  using codet::op3;
960 };
961 
962 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
963 {
964  return detail::can_cast_code_impl(base, ID_while);
965 }
966 
967 inline void validate_expr(const code_whilet &x)
968 {
969  validate_operands(x, 2, "while must have two operands");
970 }
971 
972 inline const code_whilet &to_code_while(const codet &code)
973 {
974  PRECONDITION(code.get_statement() == ID_while);
975  const code_whilet &ret = static_cast<const code_whilet &>(code);
976  validate_expr(ret);
977  return ret;
978 }
979 
981 {
982  PRECONDITION(code.get_statement() == ID_while);
983  code_whilet &ret = static_cast<code_whilet &>(code);
984  validate_expr(ret);
985  return ret;
986 }
987 
989 class code_dowhilet:public codet
990 {
991 public:
992  code_dowhilet(exprt _cond, codet _body)
993  : codet(ID_dowhile, {std::move(_cond), std::move(_body)})
994  {
995  }
996 
997  const exprt &cond() const
998  {
999  return op0();
1000  }
1001 
1003  {
1004  return op0();
1005  }
1006 
1007  const codet &body() const
1008  {
1009  return to_code(op1());
1010  }
1011 
1013  {
1014  return static_cast<codet &>(op1());
1015  }
1016 
1017 protected:
1018  using codet::op0;
1019  using codet::op1;
1020  using codet::op2;
1021  using codet::op3;
1022 };
1023 
1024 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
1025 {
1026  return detail::can_cast_code_impl(base, ID_dowhile);
1027 }
1028 
1029 inline void validate_expr(const code_dowhilet &x)
1030 {
1031  validate_operands(x, 2, "do-while must have two operands");
1032 }
1033 
1034 inline const code_dowhilet &to_code_dowhile(const codet &code)
1035 {
1036  PRECONDITION(code.get_statement() == ID_dowhile);
1037  const code_dowhilet &ret = static_cast<const code_dowhilet &>(code);
1038  validate_expr(ret);
1039  return ret;
1040 }
1041 
1043 {
1044  PRECONDITION(code.get_statement() == ID_dowhile);
1045  code_dowhilet &ret = static_cast<code_dowhilet &>(code);
1046  validate_expr(ret);
1047  return ret;
1048 }
1049 
1051 class code_fort:public codet
1052 {
1053 public:
1056  code_fort(exprt _init, exprt _cond, exprt _iter, codet _body)
1057  : codet(
1058  ID_for,
1059  {std::move(_init),
1060  std::move(_cond),
1061  std::move(_iter),
1062  std::move(_body)})
1063  {
1064  }
1065 
1066  // nil or a statement
1067  const exprt &init() const
1068  {
1069  return op0();
1070  }
1071 
1073  {
1074  return op0();
1075  }
1076 
1077  const exprt &cond() const
1078  {
1079  return op1();
1080  }
1081 
1083  {
1084  return op1();
1085  }
1086 
1087  const exprt &iter() const
1088  {
1089  return op2();
1090  }
1091 
1093  {
1094  return op2();
1095  }
1096 
1097  const codet &body() const
1098  {
1099  return to_code(op3());
1100  }
1101 
1103  {
1104  return static_cast<codet &>(op3());
1105  }
1106 
1118  exprt start_index,
1119  exprt end_index,
1120  symbol_exprt loop_index,
1121  codet body,
1122  source_locationt location);
1123 
1124 protected:
1125  using codet::op0;
1126  using codet::op1;
1127  using codet::op2;
1128  using codet::op3;
1129 };
1130 
1131 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
1132 {
1133  return detail::can_cast_code_impl(base, ID_for);
1134 }
1135 
1136 inline void validate_expr(const code_fort &x)
1137 {
1138  validate_operands(x, 4, "for must have four operands");
1139 }
1140 
1141 inline const code_fort &to_code_for(const codet &code)
1142 {
1143  PRECONDITION(code.get_statement() == ID_for);
1144  const code_fort &ret = static_cast<const code_fort &>(code);
1145  validate_expr(ret);
1146  return ret;
1147 }
1148 
1150 {
1151  PRECONDITION(code.get_statement() == ID_for);
1152  code_fort &ret = static_cast<code_fort &>(code);
1153  validate_expr(ret);
1154  return ret;
1155 }
1156 
1158 class code_gotot:public codet
1159 {
1160 public:
1161  explicit code_gotot(const irep_idt &label):codet(ID_goto)
1162  {
1163  set_destination(label);
1164  }
1165 
1166  void set_destination(const irep_idt &label)
1167  {
1168  set(ID_destination, label);
1169  }
1170 
1171  const irep_idt &get_destination() const
1172  {
1173  return get(ID_destination);
1174  }
1175 
1176 protected:
1177  using codet::op0;
1178  using codet::op1;
1179  using codet::op2;
1180  using codet::op3;
1181 };
1182 
1183 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
1184 {
1185  return detail::can_cast_code_impl(base, ID_goto);
1186 }
1187 
1188 inline void validate_expr(const code_gotot &x)
1189 {
1190  validate_operands(x, 0, "goto must not have operands");
1191 }
1192 
1193 inline const code_gotot &to_code_goto(const codet &code)
1194 {
1195  PRECONDITION(code.get_statement() == ID_goto);
1196  const code_gotot &ret = static_cast<const code_gotot &>(code);
1197  validate_expr(ret);
1198  return ret;
1199 }
1200 
1202 {
1203  PRECONDITION(code.get_statement() == ID_goto);
1204  code_gotot &ret = static_cast<code_gotot &>(code);
1205  validate_expr(ret);
1206  return ret;
1207 }
1208 
1215 {
1216 public:
1217  explicit code_function_callt(exprt _function)
1218  : codet(
1219  ID_function_call,
1220  {nil_exprt(), std::move(_function), exprt(ID_arguments)})
1221  {
1222  }
1223 
1225 
1226  code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
1227  : codet(
1228  ID_function_call,
1229  {std::move(_lhs), std::move(_function), exprt(ID_arguments)})
1230  {
1231  arguments() = std::move(_arguments);
1232  }
1233 
1234  code_function_callt(exprt _function, argumentst _arguments)
1235  : code_function_callt(std::move(_function))
1236  {
1237  arguments() = std::move(_arguments);
1238  }
1239 
1241  {
1242  return op0();
1243  }
1244 
1245  const exprt &lhs() const
1246  {
1247  return op0();
1248  }
1249 
1250  exprt &function()
1251  {
1252  return op1();
1253  }
1254 
1255  const exprt &function() const
1256  {
1257  return op1();
1258  }
1259 
1261  {
1262  return op2().operands();
1263  }
1264 
1265  const argumentst &arguments() const
1266  {
1267  return op2().operands();
1268  }
1269 
1270  static void check(
1271  const codet &code,
1273  {
1274  DATA_CHECK(
1275  vm,
1276  code.operands().size() == 3,
1277  "function calls must have three operands:\n1) expression to store the "
1278  "returned values\n2) the function being called\n3) the vector of "
1279  "arguments");
1280  }
1281 
1282  static void validate(
1283  const codet &code,
1284  const namespacet &,
1286  {
1287  check(code, vm);
1288 
1289  if(code.op0().id() != ID_nil)
1290  DATA_CHECK(
1291  vm,
1292  code.op0().type() == to_code_type(code.op1().type()).return_type(),
1293  "function returns expression of wrong type");
1294  }
1295 
1296  static void validate_full(
1297  const codet &code,
1298  const namespacet &ns,
1300  {
1301  for(const exprt &op : code.operands())
1302  {
1303  validate_full_expr(op, ns, vm);
1304  }
1305 
1306  validate(code, ns, vm);
1307  }
1308 
1309 protected:
1310  using codet::op0;
1311  using codet::op1;
1312  using codet::op2;
1313  using codet::op3;
1314 };
1315 
1316 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
1317 {
1318  return detail::can_cast_code_impl(base, ID_function_call);
1319 }
1320 
1321 inline void validate_expr(const code_function_callt &x)
1322 {
1324 }
1325 
1327 {
1328  PRECONDITION(code.get_statement() == ID_function_call);
1330  return static_cast<const code_function_callt &>(code);
1331 }
1332 
1334 {
1335  PRECONDITION(code.get_statement() == ID_function_call);
1337  return static_cast<code_function_callt &>(code);
1338 }
1339 
1341 class code_returnt:public codet
1342 {
1343 public:
1344  code_returnt() : codet(ID_return, {nil_exprt()})
1345  {
1346  }
1347 
1348  explicit code_returnt(exprt _op) : codet(ID_return, {std::move(_op)})
1349  {
1350  }
1351 
1352  const exprt &return_value() const
1353  {
1354  return op0();
1355  }
1356 
1358  {
1359  return op0();
1360  }
1361 
1362  bool has_return_value() const
1363  {
1364  return return_value().is_not_nil();
1365  }
1366 
1367  static void check(
1368  const codet &code,
1370  {
1371  DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
1372  }
1373 
1374 protected:
1375  using codet::op0;
1376  using codet::op1;
1377  using codet::op2;
1378  using codet::op3;
1379 };
1380 
1381 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
1382 {
1383  return detail::can_cast_code_impl(base, ID_return);
1384 }
1385 
1386 inline void validate_expr(const code_returnt &x)
1387 {
1389 }
1390 
1391 inline const code_returnt &to_code_return(const codet &code)
1392 {
1393  PRECONDITION(code.get_statement() == ID_return);
1394  code_returnt::check(code);
1395  return static_cast<const code_returnt &>(code);
1396 }
1397 
1399 {
1400  PRECONDITION(code.get_statement() == ID_return);
1401  code_returnt::check(code);
1402  return static_cast<code_returnt &>(code);
1403 }
1404 
1406 class code_labelt:public codet
1407 {
1408 public:
1409  code_labelt(const irep_idt &_label, codet _code)
1410  : codet(ID_label, {std::move(_code)})
1411  {
1412  set_label(_label);
1413  }
1414 
1415  const irep_idt &get_label() const
1416  {
1417  return get(ID_label);
1418  }
1419 
1420  void set_label(const irep_idt &label)
1421  {
1422  set(ID_label, label);
1423  }
1424 
1426  {
1427  return static_cast<codet &>(op0());
1428  }
1429 
1430  const codet &code() const
1431  {
1432  return static_cast<const codet &>(op0());
1433  }
1434 
1435 protected:
1436  using codet::op0;
1437  using codet::op1;
1438  using codet::op2;
1439  using codet::op3;
1440 };
1441 
1442 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
1443 {
1444  return detail::can_cast_code_impl(base, ID_label);
1445 }
1446 
1447 inline void validate_expr(const code_labelt &x)
1448 {
1449  validate_operands(x, 1, "label must have one operand");
1450 }
1451 
1452 inline const code_labelt &to_code_label(const codet &code)
1453 {
1454  PRECONDITION(code.get_statement() == ID_label);
1455  const code_labelt &ret = static_cast<const code_labelt &>(code);
1456  validate_expr(ret);
1457  return ret;
1458 }
1459 
1461 {
1462  PRECONDITION(code.get_statement() == ID_label);
1463  code_labelt &ret = static_cast<code_labelt &>(code);
1464  validate_expr(ret);
1465  return ret;
1466 }
1467 
1471 {
1472 public:
1473  code_switch_caset(exprt _case_op, codet _code)
1474  : codet(ID_switch_case, {std::move(_case_op), std::move(_code)})
1475  {
1476  }
1477 
1478  bool is_default() const
1479  {
1480  return get_bool(ID_default);
1481  }
1482 
1484  {
1485  return set(ID_default, true);
1486  }
1487 
1488  const exprt &case_op() const
1489  {
1490  return op0();
1491  }
1492 
1494  {
1495  return op0();
1496  }
1497 
1499  {
1500  return static_cast<codet &>(op1());
1501  }
1502 
1503  const codet &code() const
1504  {
1505  return static_cast<const codet &>(op1());
1506  }
1507 
1508 protected:
1509  using codet::op0;
1510  using codet::op1;
1511  using codet::op2;
1512  using codet::op3;
1513 };
1514 
1515 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1516 {
1517  return detail::can_cast_code_impl(base, ID_switch_case);
1518 }
1519 
1520 inline void validate_expr(const code_switch_caset &x)
1521 {
1522  validate_operands(x, 2, "switch-case must have two operands");
1523 }
1524 
1525 inline const code_switch_caset &to_code_switch_case(const codet &code)
1526 {
1527  PRECONDITION(code.get_statement() == ID_switch_case);
1528  const code_switch_caset &ret = static_cast<const code_switch_caset &>(code);
1529  validate_expr(ret);
1530  return ret;
1531 }
1532 
1534 {
1535  PRECONDITION(code.get_statement() == ID_switch_case);
1536  code_switch_caset &ret = static_cast<code_switch_caset &>(code);
1537  validate_expr(ret);
1538  return ret;
1539 }
1540 
1545 {
1546 public:
1548  : codet(
1549  ID_gcc_switch_case_range,
1550  {std::move(_lower), std::move(_upper), std::move(_code)})
1551  {
1552  }
1553 
1555  const exprt &lower() const
1556  {
1557  return op0();
1558  }
1559 
1562  {
1563  return op0();
1564  }
1565 
1567  const exprt &upper() const
1568  {
1569  return op1();
1570  }
1571 
1574  {
1575  return op1();
1576  }
1577 
1580  {
1581  return static_cast<codet &>(op2());
1582  }
1583 
1585  const codet &code() const
1586  {
1587  return static_cast<const codet &>(op2());
1588  }
1589 
1590 protected:
1591  using codet::op0;
1592  using codet::op1;
1593  using codet::op2;
1594  using codet::op3;
1595 };
1596 
1597 template <>
1599 {
1600  return detail::can_cast_code_impl(base, ID_gcc_switch_case_range);
1601 }
1602 
1604 {
1605  validate_operands(x, 3, "gcc-switch-case-range must have three operands");
1606 }
1607 
1608 inline const code_gcc_switch_case_ranget &
1610 {
1611  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1612  const code_gcc_switch_case_ranget &ret =
1613  static_cast<const code_gcc_switch_case_ranget &>(code);
1614  validate_expr(ret);
1615  return ret;
1616 }
1617 
1619 {
1620  PRECONDITION(code.get_statement() == ID_gcc_switch_case_range);
1622  static_cast<code_gcc_switch_case_ranget &>(code);
1623  validate_expr(ret);
1624  return ret;
1625 }
1626 
1629 class code_breakt:public codet
1630 {
1631 public:
1632  code_breakt():codet(ID_break)
1633  {
1634  }
1635 
1636 protected:
1637  using codet::op0;
1638  using codet::op1;
1639  using codet::op2;
1640  using codet::op3;
1641 };
1642 
1643 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1644 {
1645  return detail::can_cast_code_impl(base, ID_break);
1646 }
1647 
1648 // to_code_break only checks the code statement, so no validate_expr is
1649 // provided for code_breakt
1650 
1651 inline const code_breakt &to_code_break(const codet &code)
1652 {
1653  PRECONDITION(code.get_statement() == ID_break);
1654  return static_cast<const code_breakt &>(code);
1655 }
1656 
1658 {
1659  PRECONDITION(code.get_statement() == ID_break);
1660  return static_cast<code_breakt &>(code);
1661 }
1662 
1665 class code_continuet:public codet
1666 {
1667 public:
1668  code_continuet():codet(ID_continue)
1669  {
1670  }
1671 
1672 protected:
1673  using codet::op0;
1674  using codet::op1;
1675  using codet::op2;
1676  using codet::op3;
1677 };
1678 
1679 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1680 {
1681  return detail::can_cast_code_impl(base, ID_continue);
1682 }
1683 
1684 // to_code_continue only checks the code statement, so no validate_expr is
1685 // provided for code_continuet
1686 
1687 inline const code_continuet &to_code_continue(const codet &code)
1688 {
1689  PRECONDITION(code.get_statement() == ID_continue);
1690  return static_cast<const code_continuet &>(code);
1691 }
1692 
1694 {
1695  PRECONDITION(code.get_statement() == ID_continue);
1696  return static_cast<code_continuet &>(code);
1697 }
1698 
1700 class code_asmt:public codet
1701 {
1702 public:
1703  code_asmt():codet(ID_asm)
1704  {
1705  }
1706 
1707  explicit code_asmt(exprt expr) : codet(ID_asm, {std::move(expr)})
1708  {
1709  }
1710 
1711  const irep_idt &get_flavor() const
1712  {
1713  return get(ID_flavor);
1714  }
1715 
1716  void set_flavor(const irep_idt &f)
1717  {
1718  set(ID_flavor, f);
1719  }
1720 };
1721 
1722 template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1723 {
1724  return detail::can_cast_code_impl(base, ID_asm);
1725 }
1726 
1727 // to_code_asm only checks the code statement, so no validate_expr is
1728 // provided for code_asmt
1729 
1731 {
1732  PRECONDITION(code.get_statement() == ID_asm);
1733  return static_cast<code_asmt &>(code);
1734 }
1735 
1736 inline const code_asmt &to_code_asm(const codet &code)
1737 {
1738  PRECONDITION(code.get_statement() == ID_asm);
1739  return static_cast<const code_asmt &>(code);
1740 }
1741 
1744 class code_asm_gcct : public code_asmt
1745 {
1746 public:
1748  {
1749  set_flavor(ID_gcc);
1750  operands().resize(5);
1751  }
1752 
1754  {
1755  return op0();
1756  }
1757 
1758  const exprt &asm_text() const
1759  {
1760  return op0();
1761  }
1762 
1764  {
1765  return op1();
1766  }
1767 
1768  const exprt &outputs() const
1769  {
1770  return op1();
1771  }
1772 
1774  {
1775  return op2();
1776  }
1777 
1778  const exprt &inputs() const
1779  {
1780  return op2();
1781  }
1782 
1784  {
1785  return op3();
1786  }
1787 
1788  const exprt &clobbers() const
1789  {
1790  return op3();
1791  }
1792 
1794  {
1795  return operands()[4];
1796  }
1797 
1798  const exprt &labels() const
1799  {
1800  return operands()[4];
1801  }
1802 
1803 protected:
1804  using code_asmt::op0;
1805  using code_asmt::op1;
1806  using code_asmt::op2;
1807  using code_asmt::op3;
1808 };
1809 
1810 template <>
1811 inline bool can_cast_expr<code_asm_gcct>(const exprt &base)
1812 {
1813  return detail::can_cast_code_impl(base, ID_asm);
1814 }
1815 
1816 inline void validate_expr(const code_asm_gcct &x)
1817 {
1818  validate_operands(x, 5, "code_asm_gcc must have five operands");
1819 }
1820 
1822 {
1823  PRECONDITION(code.get_statement() == ID_asm);
1824  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1825  code_asm_gcct &ret = static_cast<code_asm_gcct &>(code);
1826  validate_expr(ret);
1827  return ret;
1828 }
1829 
1830 inline const code_asm_gcct &to_code_asm_gcc(const codet &code)
1831 {
1832  PRECONDITION(code.get_statement() == ID_asm);
1833  PRECONDITION(to_code_asm(code).get_flavor() == ID_gcc);
1834  const code_asm_gcct &ret = static_cast<const code_asm_gcct &>(code);
1835  validate_expr(ret);
1836  return ret;
1837 }
1838 
1842 {
1843 public:
1844  explicit code_expressiont(exprt expr)
1845  : codet(ID_expression, {std::move(expr)})
1846  {
1847  }
1848 
1849  const exprt &expression() const
1850  {
1851  return op0();
1852  }
1853 
1855  {
1856  return op0();
1857  }
1858 
1859 protected:
1860  using codet::op0;
1861  using codet::op1;
1862  using codet::op2;
1863  using codet::op3;
1864 };
1865 
1866 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1867 {
1868  return detail::can_cast_code_impl(base, ID_expression);
1869 }
1870 
1871 inline void validate_expr(const code_expressiont &x)
1872 {
1873  validate_operands(x, 1, "expression statement must have one operand");
1874 }
1875 
1877 {
1878  PRECONDITION(code.get_statement() == ID_expression);
1879  code_expressiont &ret = static_cast<code_expressiont &>(code);
1880  validate_expr(ret);
1881  return ret;
1882 }
1883 
1884 inline const code_expressiont &to_code_expression(const codet &code)
1885 {
1886  PRECONDITION(code.get_statement() == ID_expression);
1887  const code_expressiont &ret = static_cast<const code_expressiont &>(code);
1888  validate_expr(ret);
1889  return ret;
1890 }
1891 
1897 class side_effect_exprt : public exprt
1898 {
1899 public:
1901  const irep_idt &statement,
1902  operandst _operands,
1903  typet _type,
1904  source_locationt loc)
1905  : exprt(ID_side_effect, std::move(_type), std::move(loc))
1906  {
1907  set_statement(statement);
1908  operands() = std::move(_operands);
1909  }
1910 
1912  const irep_idt &statement,
1913  typet _type,
1914  source_locationt loc)
1915  : exprt(ID_side_effect, std::move(_type), std::move(loc))
1916  {
1917  set_statement(statement);
1918  }
1919 
1920  const irep_idt &get_statement() const
1921  {
1922  return get(ID_statement);
1923  }
1924 
1925  void set_statement(const irep_idt &statement)
1926  {
1927  return set(ID_statement, statement);
1928  }
1929 };
1930 
1931 namespace detail // NOLINT
1932 {
1933 
1934 template<typename Tag>
1935 inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1936 {
1937  if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1938  {
1939  return ptr->get_statement() == tag;
1940  }
1941  return false;
1942 }
1943 
1944 } // namespace detail
1945 
1946 template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1947 {
1948  return base.id()==ID_side_effect;
1949 }
1950 
1951 // to_side_effect_expr only checks the id, so no validate_expr is provided for
1952 // side_effect_exprt
1953 
1955 {
1956  PRECONDITION(expr.id() == ID_side_effect);
1957  return static_cast<side_effect_exprt &>(expr);
1958 }
1959 
1960 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1961 {
1962  PRECONDITION(expr.id() == ID_side_effect);
1963  return static_cast<const side_effect_exprt &>(expr);
1964 }
1965 
1968 {
1969 public:
1971  : side_effect_exprt(ID_nondet, std::move(_type), std::move(loc))
1972  {
1973  set_nullable(true);
1974  }
1975 
1976  void set_nullable(bool nullable)
1977  {
1978  set(ID_is_nondet_nullable, nullable);
1979  }
1980 
1981  bool get_nullable() const
1982  {
1983  return get_bool(ID_is_nondet_nullable);
1984  }
1985 };
1986 
1987 template<>
1989 {
1990  return detail::can_cast_side_effect_expr_impl(base, ID_nondet);
1991 }
1992 
1993 // to_side_effect_expr_nondet only checks the id, so no validate_expr is
1994 // provided for side_effect_expr_nondett
1995 
1997 {
1998  auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1999  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2000  return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
2001 }
2002 
2004  const exprt &expr)
2005 {
2006  const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
2007  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
2008  return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
2009 }
2010 
2013 {
2014 public:
2018  const exprt &_lhs,
2019  const exprt &_rhs,
2020  const source_locationt &loc)
2021  : side_effect_exprt(ID_assign, {_lhs, _rhs}, _lhs.type(), loc)
2022  {
2023  }
2024 
2027  exprt _lhs,
2028  exprt _rhs,
2029  typet _type,
2030  source_locationt loc)
2032  ID_assign,
2033  {std::move(_lhs), std::move(_rhs)},
2034  std::move(_type),
2035  std::move(loc))
2036  {
2037  }
2038 
2040  {
2041  return op0();
2042  }
2043 
2044  const exprt &lhs() const
2045  {
2046  return op0();
2047  }
2048 
2050  {
2051  return op1();
2052  }
2053 
2054  const exprt &rhs() const
2055  {
2056  return op1();
2057  }
2058 };
2059 
2060 template <>
2062 {
2063  return detail::can_cast_side_effect_expr_impl(base, ID_assign);
2064 }
2065 
2067 {
2068  auto &side_effect_expr_assign = to_side_effect_expr(expr);
2069  PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2070  return static_cast<side_effect_expr_assignt &>(side_effect_expr_assign);
2071 }
2072 
2073 inline const side_effect_expr_assignt &
2075 {
2076  const auto &side_effect_expr_assign = to_side_effect_expr(expr);
2077  PRECONDITION(side_effect_expr_assign.get_statement() == ID_assign);
2078  return static_cast<const side_effect_expr_assignt &>(side_effect_expr_assign);
2079 }
2080 
2083 {
2084 public:
2087  codet _code,
2088  typet _type,
2089  source_locationt loc)
2091  ID_statement_expression,
2092  {std::move(_code)},
2093  std::move(_type),
2094  std::move(loc))
2095  {
2096  }
2097 
2099  {
2100  return to_code(op0());
2101  }
2102 
2103  const codet &statement() const
2104  {
2105  return to_code(op0());
2106  }
2107 };
2108 
2109 template <>
2110 inline bool
2112 {
2113  return detail::can_cast_side_effect_expr_impl(base, ID_statement_expression);
2114 }
2115 
2118 {
2119  auto &side_effect_expr_statement_expression = to_side_effect_expr(expr);
2120  PRECONDITION(
2121  side_effect_expr_statement_expression.get_statement() ==
2122  ID_statement_expression);
2123  return static_cast<side_effect_expr_statement_expressiont &>(
2124  side_effect_expr_statement_expression);
2125 }
2126 
2129 {
2130  const auto &side_effect_expr_statement_expression = to_side_effect_expr(expr);
2131  PRECONDITION(
2132  side_effect_expr_statement_expression.get_statement() ==
2133  ID_statement_expression);
2134  return static_cast<const side_effect_expr_statement_expressiont &>(
2135  side_effect_expr_statement_expression);
2136 }
2137 
2140 {
2141 public:
2143  exprt _function,
2144  exprt::operandst _arguments,
2145  typet _type,
2146  source_locationt loc)
2148  ID_function_call,
2149  {std::move(_function),
2150  multi_ary_exprt{ID_arguments, std::move(_arguments), typet{}}},
2151  std::move(_type),
2152  std::move(loc))
2153  {
2154  }
2155 
2156  exprt &function()
2157  {
2158  return op0();
2159  }
2160 
2161  const exprt &function() const
2162  {
2163  return op0();
2164  }
2165 
2167  {
2168  return op1().operands();
2169  }
2170 
2172  {
2173  return op1().operands();
2174  }
2175 };
2176 
2177 template<>
2179 {
2180  return detail::can_cast_side_effect_expr_impl(base, ID_function_call);
2181 }
2182 
2183 // to_side_effect_expr_function_call only checks the id, so no validate_expr is
2184 // provided for side_effect_expr_function_callt
2185 
2188 {
2189  PRECONDITION(expr.id() == ID_side_effect);
2190  PRECONDITION(expr.get(ID_statement) == ID_function_call);
2191  return static_cast<side_effect_expr_function_callt &>(expr);
2192 }
2193 
2196 {
2197  PRECONDITION(expr.id() == ID_side_effect);
2198  PRECONDITION(expr.get(ID_statement) == ID_function_call);
2199  return static_cast<const side_effect_expr_function_callt &>(expr);
2200 }
2201 
2205 {
2206 public:
2208  irept exception_list,
2209  typet type,
2210  source_locationt loc)
2211  : side_effect_exprt(ID_throw, std::move(type), std::move(loc))
2212  {
2213  set(ID_exception_list, std::move(exception_list));
2214  }
2215 };
2216 
2217 template<>
2219 {
2220  return detail::can_cast_side_effect_expr_impl(base, ID_throw);
2221 }
2222 
2223 // to_side_effect_expr_throw only checks the id, so no validate_expr is
2224 // provided for side_effect_expr_throwt
2225 
2227 {
2228  PRECONDITION(expr.id() == ID_side_effect);
2229  PRECONDITION(expr.get(ID_statement) == ID_throw);
2230  return static_cast<side_effect_expr_throwt &>(expr);
2231 }
2232 
2234  const exprt &expr)
2235 {
2236  PRECONDITION(expr.id() == ID_side_effect);
2237  PRECONDITION(expr.get(ID_statement) == ID_throw);
2238  return static_cast<const side_effect_expr_throwt &>(expr);
2239 }
2240 
2253 {
2254 public:
2255  code_push_catcht():codet(ID_push_catch)
2256  {
2257  set(ID_exception_list, irept(ID_exception_list));
2258  }
2259 
2261  {
2262  public:
2264  {
2265  }
2266 
2267  explicit exception_list_entryt(const irep_idt &tag)
2268  {
2269  set(ID_tag, tag);
2270  }
2271 
2272  exception_list_entryt(const irep_idt &tag, const irep_idt &label)
2273  {
2274  set(ID_tag, tag);
2275  set(ID_label, label);
2276  }
2277 
2278  void set_tag(const irep_idt &tag)
2279  {
2280  set(ID_tag, tag);
2281  }
2282 
2283  const irep_idt &get_tag() const {
2284  return get(ID_tag);
2285  }
2286 
2287  void set_label(const irep_idt &label)
2288  {
2289  set(ID_label, label);
2290  }
2291 
2292  const irep_idt &get_label() const {
2293  return get(ID_label);
2294  }
2295  };
2296 
2297  typedef std::vector<exception_list_entryt> exception_listt;
2298 
2300  const irep_idt &tag,
2301  const irep_idt &label):
2302  codet(ID_push_catch)
2303  {
2304  set(ID_exception_list, irept(ID_exception_list));
2305  exception_list().push_back(exception_list_entryt(tag, label));
2306  }
2307 
2309  return (exception_listt &)find(ID_exception_list).get_sub();
2310  }
2311 
2313  return (const exception_listt &)find(ID_exception_list).get_sub();
2314  }
2315 
2316 protected:
2317  using codet::op0;
2318  using codet::op1;
2319  using codet::op2;
2320  using codet::op3;
2321 };
2322 
2323 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
2324 {
2325  return detail::can_cast_code_impl(base, ID_push_catch);
2326 }
2327 
2328 // to_code_push_catch only checks the code statement, so no validate_expr is
2329 // provided for code_push_catcht
2330 
2332 {
2333  PRECONDITION(code.get_statement() == ID_push_catch);
2334  return static_cast<code_push_catcht &>(code);
2335 }
2336 
2337 static inline const code_push_catcht &to_code_push_catch(const codet &code)
2338 {
2339  PRECONDITION(code.get_statement() == ID_push_catch);
2340  return static_cast<const code_push_catcht &>(code);
2341 }
2342 
2347 {
2348 public:
2349  code_pop_catcht():codet(ID_pop_catch)
2350  {
2351  }
2352 
2353 protected:
2354  using codet::op0;
2355  using codet::op1;
2356  using codet::op2;
2357  using codet::op3;
2358 };
2359 
2360 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
2361 {
2362  return detail::can_cast_code_impl(base, ID_pop_catch);
2363 }
2364 
2365 // to_code_pop_catch only checks the code statement, so no validate_expr is
2366 // provided for code_pop_catcht
2367 
2369 {
2370  PRECONDITION(code.get_statement() == ID_pop_catch);
2371  return static_cast<code_pop_catcht &>(code);
2372 }
2373 
2374 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
2375 {
2376  PRECONDITION(code.get_statement() == ID_pop_catch);
2377  return static_cast<const code_pop_catcht &>(code);
2378 }
2379 
2384 {
2385  public:
2386  code_landingpadt():codet(ID_exception_landingpad)
2387  {
2388  operands().resize(1);
2389  }
2390 
2392  : codet(ID_exception_landingpad, {std::move(catch_expr)})
2393  {
2394  }
2395 
2396  const exprt &catch_expr() const
2397  {
2398  return op0();
2399  }
2401  {
2402  return op0();
2403  }
2404 
2405 protected:
2406  using codet::op0;
2407  using codet::op1;
2408  using codet::op2;
2409  using codet::op3;
2410 };
2411 
2412 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
2413 {
2414  return detail::can_cast_code_impl(base, ID_exception_landingpad);
2415 }
2416 
2417 // to_code_landingpad only checks the code statement, so no validate_expr is
2418 // provided for code_landingpadt
2419 
2421 {
2422  PRECONDITION(code.get_statement() == ID_exception_landingpad);
2423  return static_cast<code_landingpadt &>(code);
2424 }
2425 
2426 static inline const code_landingpadt &to_code_landingpad(const codet &code)
2427 {
2428  PRECONDITION(code.get_statement() == ID_exception_landingpad);
2429  return static_cast<const code_landingpadt &>(code);
2430 }
2431 
2434 {
2435 public:
2437  explicit code_try_catcht(codet _try_code)
2438  : codet(ID_try_catch, {std::move(_try_code)})
2439  {
2440  }
2441 
2443  {
2444  return static_cast<codet &>(op0());
2445  }
2446 
2447  const codet &try_code() const
2448  {
2449  return static_cast<const codet &>(op0());
2450  }
2451 
2453  {
2454  PRECONDITION((2 * i + 2) < operands().size());
2455  return to_code_decl(to_code(operands()[2*i+1]));
2456  }
2457 
2458  const code_declt &get_catch_decl(unsigned i) const
2459  {
2460  PRECONDITION((2 * i + 2) < operands().size());
2461  return to_code_decl(to_code(operands()[2*i+1]));
2462  }
2463 
2464  codet &get_catch_code(unsigned i)
2465  {
2466  PRECONDITION((2 * i + 2) < operands().size());
2467  return to_code(operands()[2*i+2]);
2468  }
2469 
2470  const codet &get_catch_code(unsigned i) const
2471  {
2472  PRECONDITION((2 * i + 2) < operands().size());
2473  return to_code(operands()[2*i+2]);
2474  }
2475 
2476  void add_catch(const code_declt &to_catch, const codet &code_catch)
2477  {
2478  add_to_operands(to_catch, code_catch);
2479  }
2480 
2481 protected:
2482  using codet::op0;
2483  using codet::op1;
2484  using codet::op2;
2485  using codet::op3;
2486 };
2487 
2488 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
2489 {
2490  return detail::can_cast_code_impl(base, ID_try_catch);
2491 }
2492 
2493 inline void validate_expr(const code_try_catcht &x)
2494 {
2495  validate_operands(x, 3, "try-catch must have three or more operands", true);
2496 }
2497 
2498 inline const code_try_catcht &to_code_try_catch(const codet &code)
2499 {
2500  PRECONDITION(code.get_statement() == ID_try_catch);
2501  const code_try_catcht &ret = static_cast<const code_try_catcht &>(code);
2502  validate_expr(ret);
2503  return ret;
2504 }
2505 
2507 {
2508  PRECONDITION(code.get_statement() == ID_try_catch);
2509  code_try_catcht &ret = static_cast<code_try_catcht &>(code);
2510  validate_expr(ret);
2511  return ret;
2512 }
2513 
2518 {
2519 public:
2521  const std::vector<irep_idt> &parameter_identifiers,
2522  code_blockt _block)
2523  : codet(ID_function_body, {std::move(_block)})
2524  {
2525  set_parameter_identifiers(parameter_identifiers);
2526  }
2527 
2529  {
2530  return to_code_block(to_code(op0()));
2531  }
2532 
2533  const code_blockt &block() const
2534  {
2535  return to_code_block(to_code(op0()));
2536  }
2537 
2538  std::vector<irep_idt> get_parameter_identifiers() const;
2539  void set_parameter_identifiers(const std::vector<irep_idt> &);
2540 
2541 protected:
2542  using codet::op0;
2543  using codet::op1;
2544  using codet::op2;
2545  using codet::op3;
2546 };
2547 
2549 {
2550  PRECONDITION(code.get_statement() == ID_function_body);
2552  code.operands().size() == 1, "code_function_body must have one operand");
2553  return static_cast<const code_function_bodyt &>(code);
2554 }
2555 
2557 {
2558  PRECONDITION(code.get_statement() == ID_function_body);
2560  code.operands().size() == 1, "code_function_body must have one operand");
2561  return static_cast<code_function_bodyt &>(code);
2562 }
2563 
2564 #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:122
code_continuet::code_continuet
code_continuet()
Definition: std_code.h:1668
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:109
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:1488
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:2017
side_effect_expr_function_callt::arguments
const exprt::operandst & arguments() const
Definition: std_code.h:2171
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
code_try_catcht::add_catch
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:2476
code_switch_caset::code_switch_caset
code_switch_caset(exprt _case_op, codet _code)
Definition: std_code.h:1473
code_function_bodyt::set_parameter_identifiers
void set_parameter_identifiers(const std::vector< irep_idt > &)
Definition: std_code.cpp:145
code_function_callt::op1
exprt & op1()
Definition: expr.h:106
multi_ary_exprt
A base class for multi-ary expressions Associativity is not specified.
Definition: std_expr.h:741
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:1745
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1876
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
exprt::op3
exprt & op3()
Definition: expr.h:112
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:2187
side_effect_expr_assignt::lhs
const exprt & lhs() const
Definition: std_code.h:2044
can_cast_expr< side_effect_expr_function_callt >
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:2178
code_asm_gcct::clobbers
exprt & clobbers()
Definition: std_code.h:1783
can_cast_expr< code_inputt >
bool can_cast_expr< code_inputt >(const exprt &base)
Definition: std_code.h:705
code_asm_gcct::clobbers
const exprt & clobbers() const
Definition: std_code.h:1788
code_ifthenelset::op1
exprt & op1()
Definition: expr.h:106
code_expressiont::code_expressiont
code_expressiont(exprt expr)
Definition: std_code.h:1844
code_fort::cond
const exprt & cond() const
Definition: std_code.h:1077
code_declt::symbol
const symbol_exprt & symbol() const
Definition: std_code.h:413
code_whilet
codet representing a while statement.
Definition: std_code.h:928
codet::op0
exprt & op0()
Definition: expr.h:103
code_asm_gcct::outputs
exprt & outputs()
Definition: std_code.h:1763
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:482
code_function_callt::code_function_callt
code_function_callt(exprt _function, argumentst _arguments)
Definition: std_code.h:1234
code_breakt::code_breakt
code_breakt()
Definition: std_code.h:1632
can_cast_expr< side_effect_expr_throwt >
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition: std_code.h:2218
code_asmt
codet representation of an inline assembler statement.
Definition: std_code.h:1701
code_try_catcht::code_try_catcht
code_try_catcht(codet _try_code)
A statement representing try _try_code catch ...
Definition: std_code.h:2437
code_gcc_switch_case_ranget::lower
exprt & lower()
lower bound of range
Definition: std_code.h:1561
side_effect_exprt::side_effect_exprt
side_effect_exprt(const irep_idt &statement, operandst _operands, typet _type, source_locationt loc)
Definition: std_code.h:1900
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:157
code_fort
codet representation of a for statement.
Definition: std_code.h:1052
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:22
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:1296
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::op0
exprt & op0()
Definition: expr.h:103
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:806
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:1567
code_assertt::code_assertt
code_assertt(exprt expr)
Definition: std_code.h:621
code_switch_caset::case_op
exprt & case_op()
Definition: std_code.h:1493
code_switch_caset::set_default
void set_default()
Definition: std_code.h:1483
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:2255
code_try_catcht
codet representation of a try/catch block.
Definition: std_code.h:2434
to_code_break
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1651
to_code_function_body
const code_function_bodyt & to_code_function_body(const codet &code)
Definition: std_code.h:2548
code_landingpadt::code_landingpadt
code_landingpadt()
Definition: std_code.h:2386
code_switch_caset::code
const codet & code() const
Definition: std_code.h:1503
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
code_try_catcht::get_catch_code
codet & get_catch_code(unsigned i)
Definition: std_code.h:2464
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:2026
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:2400
code_asm_gcct::labels
exprt & labels()
Definition: std_code.h:1793
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:2142
code_ifthenelset::else_case
codet & else_case()
Definition: std_code.h:826
code_ifthenelset::cond
exprt & cond()
Definition: std_code.h:801
can_cast_expr< side_effect_exprt >
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1946
code_declt::initial_value
optionalt< exprt > initial_value() const
Returns the initial value to which the declared variable is initialized, or empty in the case where n...
Definition: std_code.h:427
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:402
code_assertt
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:619
code_returnt::code_returnt
code_returnt(exprt _op)
Definition: std_code.h:1348
code_gotot::code_gotot
code_gotot(const irep_idt &label)
Definition: std_code.h:1161
can_cast_expr< code_gcc_switch_case_ranget >
bool can_cast_expr< code_gcc_switch_case_ranget >(const exprt &base)
Definition: std_code.h:1598
code_assumet::assumption
const exprt & assumption() const
Definition: std_code.h:573
code_outputt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.cpp:207
exprt::exprt
exprt()
Definition: expr.h:59
side_effect_expr_statement_expressiont::statement
codet & statement()
Definition: std_code.h:2098
code_asm_gcct::inputs
exprt & inputs()
Definition: std_code.h:1773
exprt
Base class for all expressions.
Definition: expr.h:54
code_fort::iter
const exprt & iter() const
Definition: std_code.h:1087
code_function_bodyt
This class is used to interface between a language frontend and goto-convert – it communicates the id...
Definition: std_code.h:2518
code_switcht::code_switcht
code_switcht(exprt _value, codet _body)
Definition: std_code.h:868
code_push_catcht
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:2253
code_push_catcht::exception_list_entryt::exception_list_entryt
exception_list_entryt(const irep_idt &tag)
Definition: std_code.h:2267
detail
Definition: expr_cast.h:52
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:2226
exprt::op0
exprt & op0()
Definition: expr.h:103
side_effect_expr_statement_expressiont::statement
const codet & statement() const
Definition: std_code.h:2103
can_cast_expr< code_function_callt >
bool can_cast_expr< code_function_callt >(const exprt &base)
Definition: std_code.h:1316
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1666
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:972
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:796
code_declt::set_initial_value
void set_initial_value(optionalt< exprt > initial_value)
Sets the value to which this declaration initializes the declared variable.
Definition: std_code.h:438
code_gcc_switch_case_ranget::op0
exprt & op0()
Definition: expr.h:103
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
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:2347
code_gcc_switch_case_ranget::code
const codet & code() const
the statement to be executed when the case applies
Definition: std_code.h:1585
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:541
to_code_for
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1141
to_side_effect_expr_statement_expression
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:2117
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
code_ifthenelset::op2
exprt & op2()
Definition: expr.h:109
irept::irept
irept()=default
can_cast_expr< code_expressiont >
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition: std_code.h:1866
can_cast_expr< code_pop_catcht >
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition: std_code.h:2360
code_labelt::code
codet & code()
Definition: std_code.h:1425
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:1381
code_gcc_switch_case_ranget::lower
const exprt & lower() const
lower bound of range
Definition: std_code.h:1555
code_gcc_switch_case_ranget::op2
exprt & op2()
Definition: expr.h:109
code_try_catcht::get_catch_decl
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:2458
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:2283
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1525
can_cast_expr< code_switcht >
bool can_cast_expr< code_switcht >(const exprt &base)
Definition: std_code.h:900
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:2086
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:781
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:92
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:724
code_deadt::code_deadt
code_deadt(symbol_exprt symbol)
Definition: std_code.h:501
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:1282
code_try_catcht::try_code
const codet & try_code() const
Definition: std_code.h:2447
code_assertt::op0
exprt & op0()
Definition: expr.h:103
code_skipt::code_skipt
code_skipt()
Definition: std_code.h:272
code_switcht::value
exprt & value()
Definition: std_code.h:878
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
to_code_assume
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:600
to_code_assert
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:652
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
side_effect_expr_assignt::rhs
const exprt & rhs() const
Definition: std_code.h:2054
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:391
side_effect_expr_nondett::get_nullable
bool get_nullable() const
Definition: std_code.h:1981
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:185
code_fort::iter
exprt & iter()
Definition: std_code.h:1092
can_cast_expr< code_labelt >
bool can_cast_expr< code_labelt >(const exprt &base)
Definition: std_code.h:1442
can_cast_expr< code_continuet >
bool can_cast_expr< code_continuet >(const exprt &base)
Definition: std_code.h:1679
code_function_bodyt::get_parameter_identifiers
std::vector< irep_idt > get_parameter_identifiers() const
Definition: std_code.cpp:135
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
code_assertt::assertion
const exprt & assertion() const
Definition: std_code.h:625
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:990
code_pop_catcht::code_pop_catcht
code_pop_catcht()
Definition: std_code.h:2349
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:1002
code_returnt::op0
exprt & op0()
Definition: expr.h:103
code_fort::init
const exprt & init() const
Definition: std_code.h:1067
empty_typet
The empty type.
Definition: std_types.h:46
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1478
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:1988
code_switch_caset::op0
exprt & op0()
Definition: expr.h:103
can_cast_expr< code_fort >
bool can_cast_expr< code_fort >(const exprt &base)
Definition: std_code.h:1131
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:1716
code_breakt
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1630
code_whilet::cond
exprt & cond()
Definition: std_code.h:940
code_deadt::op0
exprt & op0()
Definition: expr.h:103
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:179
code_function_callt::op0
exprt & op0()
Definition: expr.h:103
code_gcc_switch_case_ranget::code
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1579
code_assumet::code_assumet
code_assumet(exprt expr)
Definition: std_code.h:569
code_function_bodyt::block
code_blockt & block()
Definition: std_code.h:2528
to_code_goto
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1193
code_labelt::code
const codet & code() const
Definition: std_code.h:1430
can_cast_expr< code_try_catcht >
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition: std_code.h:2488
can_cast_expr< side_effect_expr_assignt >
bool can_cast_expr< side_effect_expr_assignt >(const exprt &base)
Definition: std_code.h:2061
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:848
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
code_whilet::body
codet & body()
Definition: std_code.h:950
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:2299
code_push_catcht::exception_list_entryt::set_tag
void set_tag(const irep_idt &tag)
Definition: std_code.h:2278
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:551
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
code_push_catcht::exception_list_entryt
Definition: std_code.h:2261
code_assignt::op0
exprt & op0()
Definition: expr.h:103
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:567
code_whilet::op0
exprt & op0()
Definition: expr.h:103
code_fort::init
exprt & init()
Definition: std_code.h:1072
side_effect_expr_nondett::set_nullable
void set_nullable(bool nullable)
Definition: std_code.h:1976
code_deadt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:520
std_types.h
Pre-defined types.
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1452
can_cast_expr< code_asmt >
bool can_cast_expr< code_asmt >(const exprt &base)
Definition: std_code.h:1722
side_effect_expr_assignt::lhs
exprt & lhs()
Definition: std_code.h:2039
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:55
can_cast_expr< code_ifthenelset >
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition: std_code.h:838
to_code_pop_catch
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition: std_code.h:2368
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:1747
exprt::op1
exprt & op1()
Definition: expr.h:106
code_returnt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1367
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:2013
can_cast_expr< code_asm_gcct >
bool can_cast_expr< code_asm_gcct >(const exprt &base)
Definition: std_code.h:1811
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:1034
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:2308
code_push_catcht::exception_list_entryt::exception_list_entryt
exception_list_entryt()
Definition: std_code.h:2263
code_function_callt::arguments
const argumentst & arguments() const
Definition: std_code.h:1265
code_fort::op2
exprt & op2()
Definition: expr.h:109
can_cast_expr< side_effect_expr_statement_expressiont >
bool can_cast_expr< side_effect_expr_statement_expressiont >(const exprt &base)
Definition: std_code.h:2111
irept::swap
void swap(irept &irep)
Definition: irep.h:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_fort::body
codet & body()
Definition: std_code.h:1102
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:935
code_asm_gcct::labels
const exprt & labels() const
Definition: std_code.h:1798
side_effect_expr_assignt::rhs
exprt & rhs()
Definition: std_code.h:2049
code_assumet::assumption
exprt & assumption()
Definition: std_code.h:578
validation_modet
validation_modet
Definition: validation_mode.h:13
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:505
code_whilet::body
const codet & body() const
Definition: std_code.h:945
codet::op2
exprt & op2()
Definition: expr.h:109
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_dowhilet::op1
exprt & op1()
Definition: expr.h:106
code_fort::op1
exprt & op1()
Definition: expr.h:106
to_code_asm_gcc
code_asm_gcct & to_code_asm_gcc(codet &code)
Definition: std_code.h:1821
code_push_catcht::exception_list_entryt::set_label
void set_label(const irep_idt &label)
Definition: std_code.h:2287
code_labelt::set_label
void set_label(const irep_idt &label)
Definition: std_code.h:1420
side_effect_exprt::set_statement
void set_statement(const irep_idt &statement)
Definition: std_code.h:1925
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:2272
code_labelt::code_labelt
code_labelt(const irep_idt &_label, codet _code)
Definition: std_code.h:1409
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:499
code_dowhilet::code_dowhilet
code_dowhilet(exprt _cond, codet _body)
Definition: std_code.h:992
code_asmt::code_asmt
code_asmt()
Definition: std_code.h:1703
code_function_callt::code_function_callt
code_function_callt(exprt _lhs, exprt _function, argumentst _arguments)
Definition: std_code.h:1226
side_effect_expr_statement_expressiont
A side_effect_exprt that contains a statement.
Definition: std_code.h:2083
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
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:590
code_push_catcht::exception_list_entryt::get_label
const irep_idt & get_label() const
Definition: std_code.h:2292
side_effect_expr_throwt::side_effect_expr_throwt
side_effect_expr_throwt(irept exception_list, typet type, source_locationt loc)
Definition: std_code.h:2207
code_assignt::op1
exprt & op1()
Definition: expr.h:106
code_try_catcht::get_catch_code
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:2470
code_ifthenelset::has_else_case
bool has_else_case() const
Definition: std_code.h:811
code_declt::symbol
symbol_exprt & symbol()
Definition: std_code.h:408
code_switch_caset::op1
exprt & op1()
Definition: expr.h:106
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:789
code_function_callt::op2
exprt & op2()
Definition: expr.h:109
code_landingpadt::catch_expr
const exprt & catch_expr() const
Definition: std_code.h:2396
to_side_effect_expr_assign
side_effect_expr_assignt & to_side_effect_expr_assign(exprt &expr)
Definition: std_code.h:2066
code_push_catcht::exception_list
const exception_listt & exception_list() const
Definition: std_code.h:2312
to_code_try_catch
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2498
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1920
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:1217
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:1609
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1415
code_asm_gcct::inputs
const exprt & inputs() const
Definition: std_code.h:1778
code_function_callt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1270
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1730
code_switcht::value
const exprt & value() const
Definition: std_code.h:873
can_cast_expr< code_whilet >
bool can_cast_expr< code_whilet >(const exprt &base)
Definition: std_code.h:962
code_returnt::has_return_value
bool has_return_value() const
Definition: std_code.h:1362
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:2420
can_cast_expr< code_outputt >
bool can_cast_expr< code_outputt >(const exprt &base)
Definition: std_code.h:751
code_expressiont::expression
exprt & expression()
Definition: std_code.h:1854
code_labelt::op0
exprt & op0()
Definition: expr.h:103
code_skipt
A codet representing a skip statement.
Definition: std_code.h:270
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:1342
code_landingpadt
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:2384
code_deadt::symbol
const symbol_exprt & symbol() const
Definition: std_code.h:510
code_dowhilet::body
codet & body()
Definition: std_code.h:1012
side_effect_exprt::side_effect_exprt
side_effect_exprt(const irep_idt &statement, typet _type, source_locationt loc)
Definition: std_code.h:1911
can_cast_expr< code_declt >
bool can_cast_expr< code_declt >(const exprt &base)
Definition: std_code.h:472
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:2391
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:677
code_returnt::code_returnt
code_returnt()
Definition: std_code.h:1344
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:2297
code_switcht
codet representing a switch statement.
Definition: std_code.h:866
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
code_dowhilet::body
const codet & body() const
Definition: std_code.h:1007
code_asm_gcct::asm_text
const exprt & asm_text() const
Definition: std_code.h:1758
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2166
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:88
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:1547
code_function_bodyt::op0
exprt & op0()
Definition: expr.h:103
to_side_effect_expr_nondet
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1996
code_fort::body
const codet & body() const
Definition: std_code.h:1097
code_gotot::set_destination
void set_destination(const irep_idt &label)
Definition: std_code.h:1166
code_ifthenelset::then_case
codet & then_case()
Definition: std_code.h:821
code_try_catcht::op0
exprt & op0()
Definition: expr.h:103
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:1056
invariant.h
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:816
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:1515
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:910
code_expressiont::op0
exprt & op0()
Definition: expr.h:103
code_gotot::get_destination
const irep_idt & get_destination() const
Definition: std_code.h:1171
code_dowhilet::op0
exprt & op0()
Definition: expr.h:103
irept::get_sub
subt & get_sub()
Definition: irep.h:466
code_function_bodyt::block
const code_blockt & block() const
Definition: std_code.h:2533
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:1573
can_cast_expr< code_gotot >
bool can_cast_expr< code_gotot >(const exprt &base)
Definition: std_code.h:1183
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:140
codet::op3
exprt & op3()
Definition: expr.h:112
code_whilet::code_whilet
code_whilet(exprt _cond, codet _body)
Definition: std_code.h:930
code_asm_gcct::asm_text
exprt & asm_text()
Definition: std_code.h:1753
validate.h
code_try_catcht::try_code
codet & try_code()
Definition: std_code.h:2442
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:97
code_switch_caset::code
codet & code()
Definition: std_code.h:1498
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:213
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:997
can_cast_expr< code_landingpadt >
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition: std_code.h:2412
side_effect_expr_throwt
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:2205
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
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:383
code_function_bodyt::code_function_bodyt
code_function_bodyt(const std::vector< irep_idt > &parameter_identifiers, code_blockt _block)
Definition: std_code.h:2520
can_cast_expr< code_assertt >
bool can_cast_expr< code_assertt >(const exprt &base)
Definition: std_code.h:642
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1849
code_blockt::find_last_statement
codet & find_last_statement()
Definition: std_code.cpp:98
codet::set_statement
void set_statement(const irep_idt &statement)
Definition: std_code.h:66
code_landingpadt::op0
exprt & op0()
Definition: expr.h:103
exprt::operands
operandst & operands()
Definition: expr.h:96
validate_code.h
codet::op1
exprt & op1()
Definition: expr.h:106
code_deadt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:515
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
code_asmt::get_flavor
const irep_idt & get_flavor() const
Definition: std_code.h:1711
code_whilet::op1
exprt & op1()
Definition: expr.h:106
code_switcht::body
const codet & body() const
Definition: std_code.h:883
code_asm_gcct::outputs
const exprt & outputs() const
Definition: std_code.h:1768
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1352
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
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:1245
code_asmt::code_asmt
code_asmt(exprt expr)
Definition: std_code.h:1707
code_fort::op0
exprt & op0()
Definition: expr.h:103
code_switcht::op0
exprt & op0()
Definition: expr.h:103
code_declt::check
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:455
can_cast_expr< code_breakt >
bool can_cast_expr< code_breakt >(const exprt &base)
Definition: std_code.h:1643
code_assertt::assertion
exprt & assertion()
Definition: std_code.h:630
std_expr.h
API to expression classes.
code_returnt::return_value
exprt & return_value()
Definition: std_code.h:1357
code_fort::op3
exprt & op3()
Definition: expr.h:112
to_code_continue
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1687
code_switcht::op1
exprt & op1()
Definition: expr.h:106
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:2452
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:1082
code_switcht::body
codet & body()
Definition: std_code.h:888
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:1898
code_blockt::end_location
source_locationt end_location() const
Definition: std_code.h:227
code_assumet::op0
exprt & op0()
Definition: expr.h:103
can_cast_expr< code_push_catcht >
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition: std_code.h:2323
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
side_effect_expr_nondett::side_effect_expr_nondett
side_effect_expr_nondett(typet _type, source_locationt loc)
Definition: std_code.h:1970
detail::can_cast_side_effect_expr_impl
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:1935
to_code_push_catch
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2331
code_gcc_switch_case_ranget::op1
exprt & op1()
Definition: expr.h:106
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:1024