cprover
std_code.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
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 <cassert>
14 #include <list>
15 
16 #include "expr.h"
17 #include "expr_cast.h"
18 
21 class codet:public exprt
22 {
23 public:
24  codet():exprt(ID_code, typet(ID_code))
25  {
26  }
27 
28  explicit codet(const irep_idt &statement):
29  exprt(ID_code, typet(ID_code))
30  {
31  set_statement(statement);
32  }
33 
34  void set_statement(const irep_idt &statement)
35  {
36  set(ID_statement, statement);
37  }
38 
39  const irep_idt &get_statement() const
40  {
41  return get(ID_statement);
42  }
43 
45  const codet &first_statement() const;
47  const codet &last_statement() const;
48  class code_blockt &make_block();
49 };
50 
51 namespace detail // NOLINT
52 {
53 
54 template<typename Tag>
55 inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
56 {
57  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
58  {
59  return ptr->get_statement() == tag;
60  }
61  return false;
62 }
63 
64 } // namespace detail
65 
66 template<> inline bool can_cast_expr<codet>(const exprt &base)
67 {
68  return base.id()==ID_code;
69 }
70 
71 // to_code has no validation other than checking the id(), so no validate_expr
72 // is provided for codet
73 
74 inline const codet &to_code(const exprt &expr)
75 {
76  assert(expr.id()==ID_code);
77  return static_cast<const codet &>(expr);
78 }
79 
80 inline codet &to_code(exprt &expr)
81 {
82  assert(expr.id()==ID_code);
83  return static_cast<codet &>(expr);
84 }
85 
88 class code_blockt:public codet
89 {
90 public:
91  code_blockt():codet(ID_block)
92  {
93  }
94 
95  explicit code_blockt(const std::list<codet> &_list):codet(ID_block)
96  {
97  operandst &o=operands();
98  reserve_operands(_list.size());
99  for(std::list<codet>::const_iterator
100  it=_list.begin();
101  it!=_list.end();
102  it++)
103  o.push_back(*it);
104  }
105 
106  void move(codet &code)
107  {
108  move_to_operands(code);
109  }
110 
111  void add(const codet &code)
112  {
113  copy_to_operands(code);
114  }
115 
116  void add(codet code, const source_locationt &loc)
117  {
118  code.add_source_location() = loc;
119  add(code);
120  }
121 
122  void append(const code_blockt &extra_block);
123 
124  // This is the closing '}' or 'END' at the end of a block
126  {
127  return static_cast<const source_locationt &>(find(ID_C_end_location));
128  }
129 
131  {
132  codet *last=this;
133 
134  while(true)
135  {
136  const irep_idt &statement=last->get_statement();
137 
138  if(statement==ID_block &&
139  !last->operands().empty())
140  {
141  last=&to_code(last->operands().back());
142  }
143  else if(statement==ID_label)
144  {
145  assert(last->operands().size()==1);
146  last=&(to_code(last->op0()));
147  }
148  else
149  break;
150  }
151 
152  return *last;
153  }
154 };
155 
156 template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
157 {
158  return detail::can_cast_code_impl(base, ID_block);
159 }
160 
161 // to_code_block has no validation other than checking the statement(), so no
162 // validate_expr is provided for code_blockt
163 
164 inline const code_blockt &to_code_block(const codet &code)
165 {
166  assert(code.get_statement()==ID_block);
167  return static_cast<const code_blockt &>(code);
168 }
169 
171 {
172  assert(code.get_statement()==ID_block);
173  return static_cast<code_blockt &>(code);
174 }
175 
178 class code_skipt:public codet
179 {
180 public:
181  code_skipt():codet(ID_skip)
182  {
183  }
184 };
185 
186 template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
187 {
188  return detail::can_cast_code_impl(base, ID_skip);
189 }
190 
191 // there is no to_code_skip, so no validate_expr is provided for code_skipt
192 
195 class code_assignt:public codet
196 {
197 public:
198  code_assignt():codet(ID_assign)
199  {
200  operands().resize(2);
201  }
202 
203  code_assignt(const exprt &lhs, const exprt &rhs):codet(ID_assign)
204  {
206  }
207 
209  {
210  return op0();
211  }
212 
214  {
215  return op1();
216  }
217 
218  const exprt &lhs() const
219  {
220  return op0();
221  }
222 
223  const exprt &rhs() const
224  {
225  return op1();
226  }
227 };
228 
229 template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
230 {
231  return detail::can_cast_code_impl(base, ID_assign);
232 }
233 
234 inline void validate_expr(const code_assignt & x)
235 {
236  validate_operands(x, 2, "Assignment must have two operands");
237 }
238 
239 inline const code_assignt &to_code_assign(const codet &code)
240 {
241  assert(code.get_statement()==ID_assign && code.operands().size()==2);
242  return static_cast<const code_assignt &>(code);
243 }
244 
246 {
247  assert(code.get_statement()==ID_assign && code.operands().size()==2);
248  return static_cast<code_assignt &>(code);
249 }
250 
253 class code_declt:public codet
254 {
255 public:
256  code_declt():codet(ID_decl)
257  {
258  operands().resize(1);
259  }
260 
261  explicit code_declt(const exprt &symbol):codet(ID_decl)
262  {
264  }
265 
267  {
268  return op0();
269  }
270 
271  const exprt &symbol() const
272  {
273  return op0();
274  }
275 
276  const irep_idt &get_identifier() const;
277 };
278 
279 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
280 {
281  return detail::can_cast_code_impl(base, ID_decl);
282 }
283 
284 inline void validate_expr(const code_declt &x)
285 {
286  validate_operands(x, 1, "Decls must have one or more operands", true);
287 }
288 
289 inline const code_declt &to_code_decl(const codet &code)
290 {
291  // will be size()==1 in the future
292  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
293  return static_cast<const code_declt &>(code);
294 }
295 
297 {
298  // will be size()==1 in the future
299  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
300  return static_cast<code_declt &>(code);
301 }
302 
305 class code_deadt:public codet
306 {
307 public:
308  code_deadt():codet(ID_dead)
309  {
310  operands().resize(1);
311  }
312 
313  explicit code_deadt(const exprt &symbol):codet(ID_dead)
314  {
316  }
317 
319  {
320  return op0();
321  }
322 
323  const exprt &symbol() const
324  {
325  return op0();
326  }
327 
328  const irep_idt &get_identifier() const;
329 };
330 
331 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
332 {
333  return detail::can_cast_code_impl(base, ID_dead);
334 }
335 
336 inline void validate_expr(const code_deadt &x)
337 {
338  validate_operands(x, 1, "Dead code must have one operand");
339 }
340 
341 inline const code_deadt &to_code_dead(const codet &code)
342 {
343  assert(code.get_statement()==ID_dead && code.operands().size()==1);
344  return static_cast<const code_deadt &>(code);
345 }
346 
348 {
349  assert(code.get_statement()==ID_dead && code.operands().size()==1);
350  return static_cast<code_deadt &>(code);
351 }
352 
354 class code_assumet:public codet
355 {
356 public:
357  code_assumet():codet(ID_assume)
358  {
359  operands().resize(1);
360  }
361 
362  explicit code_assumet(const exprt &expr):codet(ID_assume)
363  {
364  copy_to_operands(expr);
365  }
366 
367  const exprt &assumption() const
368  {
369  return op0();
370  }
371 
373  {
374  return op0();
375  }
376 };
377 
378 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
379 {
380  return detail::can_cast_code_impl(base, ID_assume);
381 }
382 
383 // to_code_assume only checks the code statement, so no validate_expr is
384 // provided for code_assumet
385 
386 inline const code_assumet &to_code_assume(const codet &code)
387 {
388  assert(code.get_statement()==ID_assume);
389  return static_cast<const code_assumet &>(code);
390 }
391 
393 {
394  assert(code.get_statement()==ID_assume);
395  return static_cast<code_assumet &>(code);
396 }
397 
400 class code_assertt:public codet
401 {
402 public:
403  code_assertt():codet(ID_assert)
404  {
405  operands().resize(1);
406  }
407 
408  explicit code_assertt(const exprt &expr):codet(ID_assert)
409  {
410  copy_to_operands(expr);
411  }
412 
413  const exprt &assertion() const
414  {
415  return op0();
416  }
417 
419  {
420  return op0();
421  }
422 };
423 
424 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
425 {
426  return detail::can_cast_code_impl(base, ID_assert);
427 }
428 
429 // to_code_assert only checks the code statement, so no validate_expr is
430 // provided for code_assertt
431 
432 inline const code_assertt &to_code_assert(const codet &code)
433 {
434  assert(code.get_statement()==ID_assert);
435  return static_cast<const code_assertt &>(code);
436 }
437 
439 {
440  assert(code.get_statement()==ID_assert);
441  return static_cast<code_assertt &>(code);
442 }
443 
457  const exprt &condition, const source_locationt &source_location);
458 
462 {
463 public:
464  code_ifthenelset():codet(ID_ifthenelse)
465  {
466  operands().resize(3);
467  op1().make_nil();
468  op2().make_nil();
469  }
470 
471  const exprt &cond() const
472  {
473  return op0();
474  }
475 
477  {
478  return op0();
479  }
480 
481  const codet &then_case() const
482  {
483  return static_cast<const codet &>(op1());
484  }
485 
486  bool has_else_case() const
487  {
488  return op2().is_not_nil();
489  }
490 
491  const codet &else_case() const
492  {
493  return static_cast<const codet &>(op2());
494  }
495 
497  {
498  return static_cast<codet &>(op1());
499  }
500 
502  {
503  return static_cast<codet &>(op2());
504  }
505 };
506 
507 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
508 {
509  return detail::can_cast_code_impl(base, ID_ifthenelse);
510 }
511 
512 inline void validate_expr(const code_ifthenelset &x)
513 {
514  validate_operands(x, 3, "If-then-else must have three operands");
515 }
516 
517 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
518 {
519  assert(code.get_statement()==ID_ifthenelse &&
520  code.operands().size()==3);
521  return static_cast<const code_ifthenelset &>(code);
522 }
523 
525 {
526  assert(code.get_statement()==ID_ifthenelse &&
527  code.operands().size()==3);
528  return static_cast<code_ifthenelset &>(code);
529 }
530 
533 class code_switcht:public codet
534 {
535 public:
536  code_switcht():codet(ID_switch)
537  {
538  operands().resize(2);
539  }
540 
541  const exprt &value() const
542  {
543  return op0();
544  }
545 
547  {
548  return op0();
549  }
550 
551  const codet &body() const
552  {
553  return to_code(op1());
554  }
555 
557  {
558  return static_cast<codet &>(op1());
559  }
560 };
561 
562 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
563 {
564  return detail::can_cast_code_impl(base, ID_switch);
565 }
566 
567 inline void validate_expr(const code_switcht &x)
568 {
569  validate_operands(x, 2, "Switch must have two operands");
570 }
571 
572 inline const code_switcht &to_code_switch(const codet &code)
573 {
574  assert(code.get_statement()==ID_switch &&
575  code.operands().size()==2);
576  return static_cast<const code_switcht &>(code);
577 }
578 
580 {
581  assert(code.get_statement()==ID_switch &&
582  code.operands().size()==2);
583  return static_cast<code_switcht &>(code);
584 }
585 
588 class code_whilet:public codet
589 {
590 public:
591  code_whilet():codet(ID_while)
592  {
593  operands().resize(2);
594  }
595 
596  const exprt &cond() const
597  {
598  return op0();
599  }
600 
602  {
603  return op0();
604  }
605 
606  const codet &body() const
607  {
608  return to_code(op1());
609  }
610 
612  {
613  return static_cast<codet &>(op1());
614  }
615 };
616 
617 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
618 {
619  return detail::can_cast_code_impl(base, ID_while);
620 }
621 
622 inline void validate_expr(const code_whilet &x)
623 {
624  validate_operands(x, 2, "While must have two operands");
625 }
626 
627 inline const code_whilet &to_code_while(const codet &code)
628 {
629  assert(code.get_statement()==ID_while &&
630  code.operands().size()==2);
631  return static_cast<const code_whilet &>(code);
632 }
633 
635 {
636  assert(code.get_statement()==ID_while &&
637  code.operands().size()==2);
638  return static_cast<code_whilet &>(code);
639 }
640 
643 class code_dowhilet:public codet
644 {
645 public:
646  code_dowhilet():codet(ID_dowhile)
647  {
648  operands().resize(2);
649  }
650 
651  const exprt &cond() const
652  {
653  return op0();
654  }
655 
657  {
658  return op0();
659  }
660 
661  const codet &body() const
662  {
663  return to_code(op1());
664  }
665 
667  {
668  return static_cast<codet &>(op1());
669  }
670 };
671 
672 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
673 {
674  return detail::can_cast_code_impl(base, ID_dowhile);
675 }
676 
677 inline void validate_expr(const code_dowhilet &x)
678 {
679  validate_operands(x, 2, "Do-while must have two operands");
680 }
681 
682 inline const code_dowhilet &to_code_dowhile(const codet &code)
683 {
684  assert(code.get_statement()==ID_dowhile &&
685  code.operands().size()==2);
686  return static_cast<const code_dowhilet &>(code);
687 }
688 
690 {
691  assert(code.get_statement()==ID_dowhile &&
692  code.operands().size()==2);
693  return static_cast<code_dowhilet &>(code);
694 }
695 
698 class code_fort:public codet
699 {
700 public:
701  code_fort():codet(ID_for)
702  {
703  operands().resize(4);
704  }
705 
706  // nil or a statement
707  const exprt &init() const
708  {
709  return op0();
710  }
711 
713  {
714  return op0();
715  }
716 
717  const exprt &cond() const
718  {
719  return op1();
720  }
721 
723  {
724  return op1();
725  }
726 
727  const exprt &iter() const
728  {
729  return op2();
730  }
731 
733  {
734  return op2();
735  }
736 
737  const codet &body() const
738  {
739  return to_code(op3());
740  }
741 
743  {
744  return static_cast<codet &>(op3());
745  }
746 };
747 
748 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
749 {
750  return detail::can_cast_code_impl(base, ID_for);
751 }
752 
753 inline void validate_expr(const code_fort &x)
754 {
755  validate_operands(x, 4, "For must have four operands");
756 }
757 
758 inline const code_fort &to_code_for(const codet &code)
759 {
760  assert(code.get_statement()==ID_for &&
761  code.operands().size()==4);
762  return static_cast<const code_fort &>(code);
763 }
764 
766 {
767  assert(code.get_statement()==ID_for &&
768  code.operands().size()==4);
769  return static_cast<code_fort &>(code);
770 }
771 
774 class code_gotot:public codet
775 {
776 public:
777  code_gotot():codet(ID_goto)
778  {
779  }
780 
781  explicit code_gotot(const irep_idt &label):codet(ID_goto)
782  {
783  set_destination(label);
784  }
785 
786  void set_destination(const irep_idt &label)
787  {
788  set(ID_destination, label);
789  }
790 
791  const irep_idt &get_destination() const
792  {
793  return get(ID_destination);
794  }
795 };
796 
797 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
798 {
799  return detail::can_cast_code_impl(base, ID_goto);
800 }
801 
802 inline void validate_expr(const code_gotot &x)
803 {
804  validate_operands(x, 0, "Goto must not have operands");
805 }
806 
807 inline const code_gotot &to_code_goto(const codet &code)
808 {
809  assert(code.get_statement()==ID_goto &&
810  code.operands().empty());
811  return static_cast<const code_gotot &>(code);
812 }
813 
815 {
816  assert(code.get_statement()==ID_goto &&
817  code.operands().empty());
818  return static_cast<code_gotot &>(code);
819 }
820 
829 {
830 public:
831  code_function_callt():codet(ID_function_call)
832  {
833  operands().resize(3);
834  lhs().make_nil();
835  op2().id(ID_arguments);
836  }
837 
839  {
840  return op0();
841  }
842 
843  const exprt &lhs() const
844  {
845  return op0();
846  }
847 
848  exprt &function()
849  {
850  return op1();
851  }
852 
853  const exprt &function() const
854  {
855  return op1();
856  }
857 
859 
861  {
862  return op2().operands();
863  }
864 
865  const argumentst &arguments() const
866  {
867  return op2().operands();
868  }
869 };
870 
871 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
872 {
873  return detail::can_cast_code_impl(base, ID_function_call);
874 }
875 
876 // to_code_function_call only checks the code statement, so no validate_expr is
877 // provided for code_function_callt
878 
880 {
881  assert(code.get_statement()==ID_function_call);
882  return static_cast<const code_function_callt &>(code);
883 }
884 
886 {
887  assert(code.get_statement()==ID_function_call);
888  return static_cast<code_function_callt &>(code);
889 }
890 
893 class code_returnt:public codet
894 {
895 public:
896  code_returnt():codet(ID_return)
897  {
898  operands().resize(1);
899  op0().make_nil();
900  }
901 
902  explicit code_returnt(const exprt &_op):codet(ID_return)
903  {
904  copy_to_operands(_op);
905  }
906 
907  const exprt &return_value() const
908  {
909  return op0();
910  }
911 
913  {
914  return op0();
915  }
916 
917  bool has_return_value() const
918  {
919  if(operands().empty())
920  return false; // backwards compatibility
921  return return_value().is_not_nil();
922  }
923 };
924 
925 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
926 {
927  return detail::can_cast_code_impl(base, ID_return);
928 }
929 
930 // to_code_return only checks the code statement, so no validate_expr is
931 // provided for code_returnt
932 
933 inline const code_returnt &to_code_return(const codet &code)
934 {
935  assert(code.get_statement()==ID_return);
936  return static_cast<const code_returnt &>(code);
937 }
938 
940 {
941  assert(code.get_statement()==ID_return);
942  return static_cast<code_returnt &>(code);
943 }
944 
947 class code_labelt:public codet
948 {
949 public:
950  code_labelt():codet(ID_label)
951  {
952  operands().resize(1);
953  }
954 
955  explicit code_labelt(const irep_idt &_label):codet(ID_label)
956  {
957  operands().resize(1);
958  set_label(_label);
959  }
960 
962  const irep_idt &_label, const codet &_code):codet(ID_label)
963  {
964  operands().resize(1);
965  set_label(_label);
966  code()=_code;
967  }
968 
969  const irep_idt &get_label() const
970  {
971  return get(ID_label);
972  }
973 
974  void set_label(const irep_idt &label)
975  {
976  set(ID_label, label);
977  }
978 
980  {
981  return static_cast<codet &>(op0());
982  }
983 
984  const codet &code() const
985  {
986  return static_cast<const codet &>(op0());
987  }
988 };
989 
990 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
991 {
992  return detail::can_cast_code_impl(base, ID_label);
993 }
994 
995 inline void validate_expr(const code_labelt &x)
996 {
997  validate_operands(x, 1, "Label must have one operand");
998 }
999 
1000 inline const code_labelt &to_code_label(const codet &code)
1001 {
1002  assert(code.get_statement()==ID_label && code.operands().size()==1);
1003  return static_cast<const code_labelt &>(code);
1004 }
1005 
1007 {
1008  assert(code.get_statement()==ID_label && code.operands().size()==1);
1009  return static_cast<code_labelt &>(code);
1010 }
1011 
1015 {
1016 public:
1017  code_switch_caset():codet(ID_switch_case)
1018  {
1019  operands().resize(2);
1020  }
1021 
1023  const exprt &_case_op, const codet &_code):codet(ID_switch_case)
1024  {
1025  copy_to_operands(_case_op, _code);
1026  }
1027 
1028  bool is_default() const
1029  {
1030  return get_bool(ID_default);
1031  }
1032 
1034  {
1035  return set(ID_default, true);
1036  }
1037 
1038  const exprt &case_op() const
1039  {
1040  return op0();
1041  }
1042 
1044  {
1045  return op0();
1046  }
1047 
1049  {
1050  return static_cast<codet &>(op1());
1051  }
1052 
1053  const codet &code() const
1054  {
1055  return static_cast<const codet &>(op1());
1056  }
1057 };
1058 
1059 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1060 {
1061  return detail::can_cast_code_impl(base, ID_switch_case);
1062 }
1063 
1064 inline void validate_expr(const code_switch_caset &x)
1065 {
1066  validate_operands(x, 2, "Switch-case must have two operands");
1067 }
1068 
1069 inline const code_switch_caset &to_code_switch_case(const codet &code)
1070 {
1071  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
1072  return static_cast<const code_switch_caset &>(code);
1073 }
1074 
1076 {
1077  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
1078  return static_cast<code_switch_caset &>(code);
1079 }
1080 
1083 class code_breakt:public codet
1084 {
1085 public:
1086  code_breakt():codet(ID_break)
1087  {
1088  }
1089 };
1090 
1091 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1092 {
1093  return detail::can_cast_code_impl(base, ID_break);
1094 }
1095 
1096 // to_code_break only checks the code statement, so no validate_expr is
1097 // provided for code_breakt
1098 
1099 inline const code_breakt &to_code_break(const codet &code)
1100 {
1101  assert(code.get_statement()==ID_break);
1102  return static_cast<const code_breakt &>(code);
1103 }
1104 
1106 {
1107  assert(code.get_statement()==ID_break);
1108  return static_cast<code_breakt &>(code);
1109 }
1110 
1113 class code_continuet:public codet
1114 {
1115 public:
1116  code_continuet():codet(ID_continue)
1117  {
1118  }
1119 };
1120 
1121 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1122 {
1123  return detail::can_cast_code_impl(base, ID_continue);
1124 }
1125 
1126 // to_code_continue only checks the code statement, so no validate_expr is
1127 // provided for code_continuet
1128 
1129 inline const code_continuet &to_code_continue(const codet &code)
1130 {
1131  assert(code.get_statement()==ID_continue);
1132  return static_cast<const code_continuet &>(code);
1133 }
1134 
1136 {
1137  assert(code.get_statement()==ID_continue);
1138  return static_cast<code_continuet &>(code);
1139 }
1140 
1143 class code_asmt:public codet
1144 {
1145 public:
1146  code_asmt():codet(ID_asm)
1147  {
1148  }
1149 
1150  explicit code_asmt(const exprt &expr):codet(ID_asm)
1151  {
1152  copy_to_operands(expr);
1153  }
1154 
1155  const irep_idt &get_flavor() const
1156  {
1157  return get(ID_flavor);
1158  }
1159 
1160  void set_flavor(const irep_idt &f)
1161  {
1162  set(ID_flavor, f);
1163  }
1164 };
1165 
1166 template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1167 {
1168  return detail::can_cast_code_impl(base, ID_asm);
1169 }
1170 
1171 // to_code_asm only checks the code statement, so no validate_expr is
1172 // provided for code_asmt
1173 
1175 {
1176  assert(code.get_statement()==ID_asm);
1177  return static_cast<code_asmt &>(code);
1178 }
1179 
1180 inline const code_asmt &to_code_asm(const codet &code)
1181 {
1182  assert(code.get_statement()==ID_asm);
1183  return static_cast<const code_asmt &>(code);
1184 }
1185 
1189 {
1190 public:
1191  code_expressiont():codet(ID_expression)
1192  {
1193  operands().resize(1);
1194  }
1195 
1196  explicit code_expressiont(const exprt &expr):codet(ID_expression)
1197  {
1198  copy_to_operands(expr);
1199  }
1200 
1201  const exprt &expression() const
1202  {
1203  return op0();
1204  }
1205 
1207  {
1208  return op0();
1209  }
1210 };
1211 
1212 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1213 {
1214  return detail::can_cast_code_impl(base, ID_expression);
1215 }
1216 
1217 inline void validate_expr(const code_expressiont &x)
1218 {
1219  validate_operands(x, 1, "Expression must have one operand");
1220 }
1221 
1223 {
1224  assert(code.get_statement()==ID_expression &&
1225  code.operands().size()==1);
1226  return static_cast<code_expressiont &>(code);
1227 }
1228 
1229 inline const code_expressiont &to_code_expression(const codet &code)
1230 {
1231  assert(code.get_statement()==ID_expression &&
1232  code.operands().size()==1);
1233  return static_cast<const code_expressiont &>(code);
1234 }
1235 
1239 {
1240 public:
1241  explicit side_effect_exprt(const irep_idt &statement):
1242  exprt(ID_side_effect)
1243  {
1244  set_statement(statement);
1245  }
1246 
1247  side_effect_exprt(const irep_idt &statement, const typet &_type):
1248  exprt(ID_side_effect, _type)
1249  {
1250  set_statement(statement);
1251  }
1252 
1253  const irep_idt &get_statement() const
1254  {
1255  return get(ID_statement);
1256  }
1257 
1258  void set_statement(const irep_idt &statement)
1259  {
1260  return set(ID_statement, statement);
1261  }
1262 };
1263 
1264 namespace detail // NOLINT
1265 {
1266 
1267 template<typename Tag>
1268 inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1269 {
1270  if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1271  {
1272  return ptr->get_statement() == tag;
1273  }
1274  return false;
1275 }
1276 
1277 } // namespace detail
1278 
1279 template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1280 {
1281  return base.id()==ID_side_effect;
1282 }
1283 
1284 // to_side_effect_expr only checks the id, so no validate_expr is provided for
1285 // side_effect_exprt
1286 
1288 {
1289  assert(expr.id()==ID_side_effect);
1290  return static_cast<side_effect_exprt &>(expr);
1291 }
1292 
1293 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1294 {
1295  assert(expr.id()==ID_side_effect);
1296  return static_cast<const side_effect_exprt &>(expr);
1297 }
1298 
1302 {
1303 public:
1305  {
1306  set_nullable(true);
1307  }
1308 
1309  explicit side_effect_expr_nondett(const typet &_type):
1310  side_effect_exprt(ID_nondet, _type)
1311  {
1312  set_nullable(true);
1313  }
1314 
1315  void set_nullable(bool nullable)
1316  {
1317  set(ID_is_nondet_nullable, nullable);
1318  }
1319 
1320  bool get_nullable() const
1321  {
1322  return get_bool(ID_is_nondet_nullable);
1323  }
1324 };
1325 
1326 template<>
1328 {
1329  return detail::can_cast_side_effect_expr_impl(base, ID_nondet);
1330 }
1331 
1332 // to_side_effect_expr_nondet only checks the id, so no validate_expr is
1333 // provided for side_effect_expr_nondett
1334 
1336 {
1337  auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1338  assert(side_effect_expr_nondet.get_statement()==ID_nondet);
1339  return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
1340 }
1341 
1343  const exprt &expr)
1344 {
1345  const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1346  assert(side_effect_expr_nondet.get_statement()==ID_nondet);
1347  return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
1348 }
1349 
1353 {
1354 public:
1356  {
1357  operands().resize(2);
1358  op1().id(ID_arguments);
1359  }
1360 
1361  exprt &function()
1362  {
1363  return op0();
1364  }
1365 
1366  const exprt &function() const
1367  {
1368  return op0();
1369  }
1370 
1372  {
1373  return op1().operands();
1374  }
1375 
1377  {
1378  return op1().operands();
1379  }
1380 };
1381 
1382 template<>
1384 {
1385  return detail::can_cast_side_effect_expr_impl(base, ID_function_call);
1386 }
1387 
1388 // to_side_effect_expr_function_call only checks the id, so no validate_expr is
1389 // provided for side_effect_expr_function_callt
1390 
1393 {
1394  assert(expr.id()==ID_side_effect);
1395  assert(expr.get(ID_statement)==ID_function_call);
1396  return static_cast<side_effect_expr_function_callt &>(expr);
1397 }
1398 
1401 {
1402  assert(expr.id()==ID_side_effect);
1403  assert(expr.get(ID_statement)==ID_function_call);
1404  return static_cast<const side_effect_expr_function_callt &>(expr);
1405 }
1406 
1410 {
1411 public:
1413  {
1414  }
1415 
1416  explicit side_effect_expr_throwt(const irept &exception_list):
1417  side_effect_exprt(ID_throw)
1418  {
1419  set(ID_exception_list, exception_list);
1420  }
1421 };
1422 
1423 template<>
1425 {
1426  return detail::can_cast_side_effect_expr_impl(base, ID_throw);
1427 }
1428 
1429 // to_side_effect_expr_throw only checks the id, so no validate_expr is
1430 // provided for side_effect_expr_throwt
1431 
1433 {
1434  assert(expr.id()==ID_side_effect);
1435  assert(expr.get(ID_statement)==ID_throw);
1436  return static_cast<side_effect_expr_throwt &>(expr);
1437 }
1438 
1440  const exprt &expr)
1441 {
1442  assert(expr.id()==ID_side_effect);
1443  assert(expr.get(ID_statement)==ID_throw);
1444  return static_cast<const side_effect_expr_throwt &>(expr);
1445 }
1446 
1459 {
1460 public:
1461  code_push_catcht():codet(ID_push_catch)
1462  {
1463  set(ID_exception_list, irept(ID_exception_list));
1464  }
1465 
1467  {
1468  public:
1470  {
1471  }
1472 
1473  explicit exception_list_entryt(const irep_idt &tag)
1474  {
1475  set(ID_tag, tag);
1476  }
1477 
1478  exception_list_entryt(const irep_idt &tag, const irep_idt &label)
1479  {
1480  set(ID_tag, tag);
1481  set(ID_label, label);
1482  }
1483 
1484  void set_tag(const irep_idt &tag)
1485  {
1486  set(ID_tag, tag);
1487  }
1488 
1489  const irep_idt &get_tag() const {
1490  return get(ID_tag);
1491  }
1492 
1493  void set_label(const irep_idt &label)
1494  {
1495  set(ID_label, label);
1496  }
1497 
1498  const irep_idt &get_label() const {
1499  return get(ID_label);
1500  }
1501  };
1502 
1503  typedef std::vector<exception_list_entryt> exception_listt;
1504 
1506  const irep_idt &tag,
1507  const irep_idt &label):
1508  codet(ID_push_catch)
1509  {
1510  set(ID_exception_list, irept(ID_exception_list));
1511  exception_list().push_back(exception_list_entryt(tag, label));
1512  }
1513 
1515  return (exception_listt &)find(ID_exception_list).get_sub();
1516  }
1517 
1519  return (const exception_listt &)find(ID_exception_list).get_sub();
1520  }
1521 };
1522 
1523 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
1524 {
1525  return detail::can_cast_code_impl(base, ID_push_catch);
1526 }
1527 
1528 // to_code_push_catch only checks the code statement, so no validate_expr is
1529 // provided for code_push_catcht
1530 
1532 {
1533  assert(code.get_statement()==ID_push_catch);
1534  return static_cast<code_push_catcht &>(code);
1535 }
1536 
1537 static inline const code_push_catcht &to_code_push_catch(const codet &code)
1538 {
1539  assert(code.get_statement()==ID_push_catch);
1540  return static_cast<const code_push_catcht &>(code);
1541 }
1542 
1547 {
1548 public:
1549  code_pop_catcht():codet(ID_pop_catch)
1550  {
1551  }
1552 };
1553 
1554 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
1555 {
1556  return detail::can_cast_code_impl(base, ID_pop_catch);
1557 }
1558 
1559 // to_code_pop_catch only checks the code statement, so no validate_expr is
1560 // provided for code_pop_catcht
1561 
1563 {
1564  assert(code.get_statement()==ID_pop_catch);
1565  return static_cast<code_pop_catcht &>(code);
1566 }
1567 
1568 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
1569 {
1570  assert(code.get_statement()==ID_pop_catch);
1571  return static_cast<const code_pop_catcht &>(code);
1572 }
1573 
1578 {
1579  public:
1580  code_landingpadt():codet(ID_exception_landingpad)
1581  {
1582  operands().resize(1);
1583  }
1585  codet(ID_exception_landingpad)
1586  {
1588  }
1589  const exprt &catch_expr() const
1590  {
1591  return op0();
1592  }
1594  {
1595  return op0();
1596  }
1597 };
1598 
1599 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
1600 {
1601  return detail::can_cast_code_impl(base, ID_exception_landingpad);
1602 }
1603 
1604 // to_code_landingpad only checks the code statement, so no validate_expr is
1605 // provided for code_landingpadt
1606 
1608 {
1609  assert(code.get_statement()==ID_exception_landingpad);
1610  return static_cast<code_landingpadt &>(code);
1611 }
1612 
1613 static inline const code_landingpadt &to_code_landingpad(const codet &code)
1614 {
1615  assert(code.get_statement()==ID_exception_landingpad);
1616  return static_cast<const code_landingpadt &>(code);
1617 }
1618 
1622 {
1623 public:
1624  code_try_catcht():codet(ID_try_catch)
1625  {
1626  operands().resize(1);
1627  }
1628 
1630  {
1631  return static_cast<codet &>(op0());
1632  }
1633 
1634  const codet &try_code() const
1635  {
1636  return static_cast<const codet &>(op0());
1637  }
1638 
1640  {
1641  assert((2*i+2)<operands().size());
1642  return to_code_decl(to_code(operands()[2*i+1]));
1643  }
1644 
1645  const code_declt &get_catch_decl(unsigned i) const
1646  {
1647  assert((2*i+2)<operands().size());
1648  return to_code_decl(to_code(operands()[2*i+1]));
1649  }
1650 
1651  codet &get_catch_code(unsigned i)
1652  {
1653  assert((2*i+2)<operands().size());
1654  return to_code(operands()[2*i+2]);
1655  }
1656 
1657  const codet &get_catch_code(unsigned i) const
1658  {
1659  assert((2*i+2)<operands().size());
1660  return to_code(operands()[2*i+2]);
1661  }
1662 
1663  void add_catch(const code_declt &to_catch, const codet &code_catch)
1664  {
1665  operands().reserve(operands().size()+2);
1666  copy_to_operands(to_catch);
1667  copy_to_operands(code_catch);
1668  }
1669 };
1670 
1671 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
1672 {
1673  return detail::can_cast_code_impl(base, ID_try_catch);
1674 }
1675 
1676 inline void validate_expr(const code_try_catcht &x)
1677 {
1678  validate_operands(x, 3, "Try-catch must have three or more operands", true);
1679 }
1680 
1681 inline const code_try_catcht &to_code_try_catch(const codet &code)
1682 {
1683  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
1684  return static_cast<const code_try_catcht &>(code);
1685 }
1686 
1688 {
1689  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
1690  return static_cast<code_try_catcht &>(code);
1691 }
1692 
1693 #endif // CPROVER_UTIL_STD_CODE_H
#define loc()
bool can_cast_expr< code_asmt >(const exprt &base)
Definition: std_code.h:1166
const irep_idt & get_statement() const
Definition: std_code.h:39
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1392
The type of an expression.
Definition: type.h:22
const codet & then_case() const
Definition: std_code.h:481
const exprt & return_value() const
Definition: std_code.h:907
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1503
bool can_cast_expr< code_assertt >(const exprt &base)
Definition: std_code.h:424
A ‘switch’ instruction.
Definition: std_code.h:533
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition: std_code.h:1523
exprt & init()
Definition: std_code.h:712
bool is_not_nil() const
Definition: irep.h:103
const exception_listt & exception_list() const
Definition: std_code.h:1518
const irep_idt & get_identifier() const
Definition: std_code.cpp:19
const exprt & init() const
Definition: std_code.h:707
code_assignt(const exprt &lhs, const exprt &rhs)
Definition: std_code.h:203
void set_label(const irep_idt &label)
Definition: std_code.h:974
code_gotot(const irep_idt &label)
Definition: std_code.h:781
exprt & cond()
Definition: std_code.h:476
A try/catch block.
Definition: std_code.h:1621
codet & get_catch_code(unsigned i)
Definition: std_code.h:1651
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition: std_code.h:1212
exprt & op0()
Definition: expr.h:72
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:386
const exprt & cond() const
Definition: std_code.h:596
A continue for ‘for’ and ‘while’ loops.
Definition: std_code.h:1113
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:341
bool can_cast_expr< code_whilet >(const exprt &base)
Definition: std_code.h:617
const irep_idt & get_tag() const
Definition: std_code.h:1489
const exprt & cond() const
Definition: std_code.h:471
exprt & symbol()
Definition: std_code.h:266
bool get_nullable() const
Definition: std_code.h:1320
bool can_cast_expr< code_blockt >(const exprt &base)
Definition: std_code.h:156
const codet & body() const
Definition: std_code.h:737
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition: std_code.h:1599
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition: std_code.h:507
codet & code()
Definition: std_code.h:1048
const codet & body() const
Definition: std_code.h:661
bool can_cast_expr< code_continuet >(const exprt &base)
Definition: std_code.h:1121
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1335
const argumentst & arguments() const
Definition: std_code.h:865
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1458
source_locationt end_location() const
Definition: std_code.h:125
code_returnt(const exprt &_op)
Definition: std_code.h:902
code_assertt(const exprt &expr)
Definition: std_code.h:408
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
void validate_expr(const code_assignt &x)
Definition: std_code.h:234
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1099
code_push_catcht(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1505
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:55
exprt & cond()
Definition: std_code.h:722
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition: std_code.h:1562
const exprt & symbol() const
Definition: std_code.h:271
codet & body()
Definition: std_code.h:611
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:1268
A ‘goto’ instruction.
Definition: std_code.h:774
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1546
exprt::operandst argumentst
Definition: std_code.h:858
codet & first_statement()
Definition: std_code.cpp:39
const irep_idt & get_flavor() const
Definition: std_code.h:1155
exprt & catch_expr()
Definition: std_code.h:1593
code_blockt(const std::list< codet > &_list)
Definition: std_code.h:95
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
void set_label(const irep_idt &label)
Definition: std_code.h:1493
codet & else_case()
Definition: std_code.h:501
An expression statement.
Definition: std_code.h:1188
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:111
codet(const irep_idt &statement)
Definition: std_code.h:28
void set_default()
Definition: std_code.h:1033
exprt & value()
Definition: std_code.h:546
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1222
A side effect that throws an exception.
Definition: std_code.h:1409
side_effect_exprt(const irep_idt &statement)
Definition: std_code.h:1241
code_assumet(const exprt &expr)
Definition: std_code.h:362
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:206
const exprt & case_op() const
Definition: std_code.h:1038
exprt & assumption()
Definition: std_code.h:372
subt & get_sub()
Definition: irep.h:245
void set_flavor(const irep_idt &f)
Definition: std_code.h:1160
codet & body()
Definition: std_code.h:556
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1287
bool can_cast_expr< code_switch_caset >(const exprt &base)
Definition: std_code.h:1059
codet & body()
Definition: std_code.h:666
void set_nullable(bool nullable)
Definition: std_code.h:1315
Templated functions to cast to specific exprt-derived classes.
exprt & assertion()
Definition: std_code.h:418
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
void add(const codet &code)
Definition: std_code.h:111
code_expressiont(const exprt &expr)
Definition: std_code.h:1196
class code_blockt & make_block()
Definition: std_code.cpp:24
code_deadt()
Definition: std_code.h:308
argumentst & arguments()
Definition: std_code.h:860
codet & body()
Definition: std_code.h:742
bool can_cast_expr< code_labelt >(const exprt &base)
Definition: std_code.h:990
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1279
A declaration of a local variable.
Definition: std_code.h:253
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1531
codet & last_statement()
Definition: std_code.cpp:69
code_landingpadt(const exprt &catch_expr)
Definition: std_code.h:1584
exprt & rhs()
Definition: std_code.h:213
const exprt & cond() const
Definition: std_code.h:717
codet & code()
Definition: std_code.h:979
void add(codet code, const source_locationt &loc)
Definition: std_code.h:116
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:1645
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:682
code_skipt()
Definition: std_code.h:181
code_deadt(const exprt &symbol)
Definition: std_code.h:313
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:627
bool can_cast_expr< code_breakt >(const exprt &base)
Definition: std_code.h:1091
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:807
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const codet & try_code() const
Definition: std_code.h:1634
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:1657
side_effect_exprt(const irep_idt &statement, const typet &_type)
Definition: std_code.h:1247
A label for branch targets.
Definition: std_code.h:947
void set_tag(const irep_idt &tag)
Definition: std_code.h:1484
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:101
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:933
exception_list_entryt(const irep_idt &tag)
Definition: std_code.h:1473
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1432
code_fort()
Definition: std_code.h:701
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition: std_code.h:1671
bool can_cast_expr< code_declt >(const exprt &base)
Definition: std_code.h:279
Base class for tree-like data structures with sharing.
Definition: irep.h:86
A function call.
Definition: std_code.h:828
const codet & code() const
Definition: std_code.h:984
const exprt & rhs() const
Definition: std_code.h:223
code_declt()
Definition: std_code.h:256
bool has_else_case() const
Definition: std_code.h:486
irept()
Definition: irep.h:115
A ‘while’ instruction.
Definition: std_code.h:588
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1069
codet & find_last_statement()
Definition: std_code.h:130
exprt & symbol()
Definition: std_code.h:318
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition: std_code.h:1424
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1327
const codet & body() const
Definition: std_code.h:551
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1383
exprt & cond()
Definition: std_code.h:656
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:572
bool has_return_value() const
Definition: std_code.h:917
bool can_cast_expr< code_switcht >(const exprt &base)
Definition: std_code.h:562
std::vector< exprt > operandst
Definition: expr.h:45
const exprt & lhs() const
Definition: std_code.h:218
bool can_cast_expr< code_gotot >(const exprt &base)
Definition: std_code.h:797
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:400
A function call side effect.
Definition: std_code.h:1352
An assumption, which must hold in subsequent code.
Definition: std_code.h:354
exprt & case_op()
Definition: std_code.h:1043
const exprt & symbol() const
Definition: std_code.h:323
side_effect_expr_nondett(const typet &_type)
Definition: std_code.h:1309
const exprt & value() const
Definition: std_code.h:541
bool can_cast_expr< code_assumet >(const exprt &base)
Definition: std_code.h:378
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1129
code_gotot()
Definition: std_code.h:777
bool can_cast_expr< codet >(const exprt &base)
Definition: std_code.h:66
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1607
bool can_cast_expr< code_dowhilet >(const exprt &base)
Definition: std_code.h:672
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
bool is_default() const
Definition: std_code.h:1028
codet & try_code()
Definition: std_code.h:1629
Base class for all expressions.
Definition: expr.h:42
A break for ‘for’ and ‘while’ loops.
Definition: std_code.h:1083
void move(codet &code)
Definition: std_code.h:106
bool can_cast_expr< code_deadt >(const exprt &base)
Definition: std_code.h:331
const exprt & assumption() const
Definition: std_code.h:367
A ‘do while’ instruction.
Definition: std_code.h:643
An inline assembler statement.
Definition: std_code.h:1143
const exprt & iter() const
Definition: std_code.h:727
code_labelt(const irep_idt &_label)
Definition: std_code.h:955
exprt & expression()
Definition: std_code.h:1206
const codet & code() const
Definition: std_code.h:1053
const exprt & expression() const
Definition: std_code.h:1201
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition: std_code.h:1554
code_blockt()
Definition: std_code.h:91
codet()
Definition: std_code.h:24
exprt::operandst & arguments()
Definition: std_code.h:1371
A removal of a local variable.
Definition: std_code.h:305
void make_nil()
Definition: irep.h:243
code_declt(const exprt &symbol)
Definition: std_code.h:261
code_declt & get_catch_decl(unsigned i)
Definition: std_code.h:1639
source_locationt & add_source_location()
Definition: expr.h:130
exprt & cond()
Definition: std_code.h:601
Sequential composition.
Definition: std_code.h:88
code_switch_caset(const exprt &_case_op, const codet &_code)
Definition: std_code.h:1022
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
const irep_idt & get_label() const
Definition: std_code.h:969
code_asmt(const exprt &expr)
Definition: std_code.h:1150
Skip.
Definition: std_code.h:178
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:758
An if-then-else.
Definition: std_code.h:461
exprt & op2()
Definition: expr.h:78
const exprt & catch_expr() const
Definition: std_code.h:1589
bool can_cast_expr< code_fort >(const exprt &base)
Definition: std_code.h:748
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
const exprt::operandst & arguments() const
Definition: std_code.h:1376
const exprt & lhs() const
Definition: std_code.h:843
codet & then_case()
Definition: std_code.h:496
bool can_cast_expr< code_skipt >(const exprt &base)
Definition: std_code.h:186
A switch-case.
Definition: std_code.h:1014
const irep_idt & get_destination() const
Definition: std_code.h:791
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:893
void set_destination(const irep_idt &label)
Definition: std_code.h:786
A ‘for’ instruction.
Definition: std_code.h:698
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1000
const irep_idt & get_label() const
Definition: std_code.h:1498
An expression containing a side effect.
Definition: std_code.h:1238
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:432
bool can_cast_expr< code_assignt >(const exprt &base)
Definition: std_code.h:229
operandst & operands()
Definition: expr.h:66
exprt & return_value()
Definition: std_code.h:912
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:1681
const exprt & cond() const
Definition: std_code.h:651
const codet & else_case() const
Definition: std_code.h:491
exception_listt & exception_list()
Definition: std_code.h:1514
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:517
void set_statement(const irep_idt &statement)
Definition: std_code.h:1258
exprt & iter()
Definition: std_code.h:732
const codet & body() const
Definition: std_code.h:606
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool can_cast_expr< code_function_callt >(const exprt &base)
Definition: std_code.h:871
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:1663
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1174
Assignment.
Definition: std_code.h:195
side_effect_expr_throwt(const irept &exception_list)
Definition: std_code.h:1416
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1478
const irep_idt & get_statement() const
Definition: std_code.h:1253
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1577
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
const exprt & assertion() const
Definition: std_code.h:413
exprt & op3()
Definition: expr.h:81
bool can_cast_expr< code_returnt >(const exprt &base)
Definition: std_code.h:925
code_labelt(const irep_idt &_label, const codet &_code)
Definition: std_code.h:961