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