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