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 
15 #include "expr.h"
16 
19 class codet:public exprt
20 {
21 public:
22  codet():exprt(ID_code, typet(ID_code))
23  {
24  }
25 
26  explicit codet(const irep_idt &statement):
27  exprt(ID_code, typet(ID_code))
28  {
29  set_statement(statement);
30  }
31 
32  void set_statement(const irep_idt &statement)
33  {
34  set(ID_statement, statement);
35  }
36 
37  const irep_idt &get_statement() const
38  {
39  return get(ID_statement);
40  }
41 
43  const codet &first_statement() const;
45  const codet &last_statement() const;
46  class code_blockt &make_block();
47 };
48 
49 inline const codet &to_code(const exprt &expr)
50 {
51  assert(expr.id()==ID_code);
52  return static_cast<const codet &>(expr);
53 }
54 
55 inline codet &to_code(exprt &expr)
56 {
57  assert(expr.id()==ID_code);
58  return static_cast<codet &>(expr);
59 }
60 
63 class code_blockt:public codet
64 {
65 public:
66  code_blockt():codet(ID_block)
67  {
68  }
69 
70  explicit code_blockt(const std::list<codet> &_list):codet(ID_block)
71  {
72  operandst &o=operands();
73  reserve_operands(_list.size());
74  for(std::list<codet>::const_iterator
75  it=_list.begin();
76  it!=_list.end();
77  it++)
78  o.push_back(*it);
79  }
80 
81  void add(const codet &code)
82  {
83  copy_to_operands(code);
84  }
85 
86  void append(const code_blockt &extra_block);
87 
88  // This is the closing '}' or 'END' at the end of a block
90  {
91  return static_cast<const source_locationt &>(find(ID_C_end_location));
92  }
93 
95  {
96  codet *last=this;
97 
98  while(true)
99  {
100  const irep_idt &statement=last->get_statement();
101 
102  if(statement==ID_block &&
103  !last->operands().empty())
104  {
105  last=&to_code(last->operands().back());
106  }
107  else if(statement==ID_label)
108  {
109  assert(last->operands().size()==1);
110  last=&(to_code(last->op0()));
111  }
112  else
113  break;
114  }
115 
116  return *last;
117  }
118 };
119 
120 inline const code_blockt &to_code_block(const codet &code)
121 {
122  assert(code.get_statement()==ID_block);
123  return static_cast<const code_blockt &>(code);
124 }
125 
127 {
128  assert(code.get_statement()==ID_block);
129  return static_cast<code_blockt &>(code);
130 }
131 
134 class code_skipt:public codet
135 {
136 public:
137  code_skipt():codet(ID_skip)
138  {
139  }
140 };
141 
144 class code_assignt:public codet
145 {
146 public:
147  code_assignt():codet(ID_assign)
148  {
149  operands().resize(2);
150  }
151 
152  code_assignt(const exprt &lhs, const exprt &rhs):codet(ID_assign)
153  {
154  copy_to_operands(lhs, rhs);
155  }
156 
158  {
159  return op0();
160  }
161 
163  {
164  return op1();
165  }
166 
167  const exprt &lhs() const
168  {
169  return op0();
170  }
171 
172  const exprt &rhs() const
173  {
174  return op1();
175  }
176 };
177 
178 inline const code_assignt &to_code_assign(const codet &code)
179 {
180  assert(code.get_statement()==ID_assign && code.operands().size()==2);
181  return static_cast<const code_assignt &>(code);
182 }
183 
185 {
186  assert(code.get_statement()==ID_assign && code.operands().size()==2);
187  return static_cast<code_assignt &>(code);
188 }
189 
192 class code_declt:public codet
193 {
194 public:
195  code_declt():codet(ID_decl)
196  {
197  operands().resize(1);
198  }
199 
200  explicit code_declt(const exprt &symbol):codet(ID_decl)
201  {
202  copy_to_operands(symbol);
203  }
204 
206  {
207  return op0();
208  }
209 
210  const exprt &symbol() const
211  {
212  return op0();
213  }
214 
215  const irep_idt &get_identifier() const;
216 };
217 
218 inline const code_declt &to_code_decl(const codet &code)
219 {
220  // will be size()==1 in the future
221  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
222  return static_cast<const code_declt &>(code);
223 }
224 
226 {
227  // will be size()==1 in the future
228  assert(code.get_statement()==ID_decl && code.operands().size()>=1);
229  return static_cast<code_declt &>(code);
230 }
231 
234 class code_deadt:public codet
235 {
236 public:
237  code_deadt():codet(ID_dead)
238  {
239  operands().resize(1);
240  }
241 
242  explicit code_deadt(const exprt &symbol):codet(ID_dead)
243  {
244  copy_to_operands(symbol);
245  }
246 
248  {
249  return op0();
250  }
251 
252  const exprt &symbol() const
253  {
254  return op0();
255  }
256 
257  const irep_idt &get_identifier() const;
258 };
259 
260 inline const code_deadt &to_code_dead(const codet &code)
261 {
262  assert(code.get_statement()==ID_dead && code.operands().size()==1);
263  return static_cast<const code_deadt &>(code);
264 }
265 
267 {
268  assert(code.get_statement()==ID_dead && code.operands().size()==1);
269  return static_cast<code_deadt &>(code);
270 }
271 
274 class code_assumet:public codet
275 {
276 public:
277  code_assumet():codet(ID_assume)
278  {
279  operands().resize(1);
280  }
281 
282  explicit code_assumet(const exprt &expr):codet(ID_assume)
283  {
284  copy_to_operands(expr);
285  }
286 
287  const exprt &assumption() const
288  {
289  return op0();
290  }
291 
293  {
294  return op0();
295  }
296 };
297 
298 inline const code_assumet &to_code_assume(const codet &code)
299 {
300  assert(code.get_statement()==ID_assume);
301  return static_cast<const code_assumet &>(code);
302 }
303 
305 {
306  assert(code.get_statement()==ID_assume);
307  return static_cast<code_assumet &>(code);
308 }
309 
312 class code_assertt:public codet
313 {
314 public:
315  code_assertt():codet(ID_assert)
316  {
317  operands().resize(1);
318  }
319 
320  explicit code_assertt(const exprt &expr):codet(ID_assert)
321  {
322  copy_to_operands(expr);
323  }
324 
325  const exprt &assertion() const
326  {
327  return op0();
328  }
329 
331  {
332  return op0();
333  }
334 };
335 
336 inline const code_assertt &to_code_assert(const codet &code)
337 {
338  assert(code.get_statement()==ID_assert);
339  return static_cast<const code_assertt &>(code);
340 }
341 
343 {
344  assert(code.get_statement()==ID_assert);
345  return static_cast<code_assertt &>(code);
346 }
347 
351 {
352 public:
353  code_ifthenelset():codet(ID_ifthenelse)
354  {
355  operands().resize(3);
356  op1().make_nil();
357  op2().make_nil();
358  }
359 
360  const exprt &cond() const
361  {
362  return op0();
363  }
364 
366  {
367  return op0();
368  }
369 
370  const codet &then_case() const
371  {
372  return static_cast<const codet &>(op1());
373  }
374 
375  bool has_else_case() const
376  {
377  return op2().is_not_nil();
378  }
379 
380  const codet &else_case() const
381  {
382  return static_cast<const codet &>(op2());
383  }
384 
386  {
387  return static_cast<codet &>(op1());
388  }
389 
391  {
392  return static_cast<codet &>(op2());
393  }
394 };
395 
396 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
397 {
398  assert(code.get_statement()==ID_ifthenelse &&
399  code.operands().size()==3);
400  return static_cast<const code_ifthenelset &>(code);
401 }
402 
404 {
405  assert(code.get_statement()==ID_ifthenelse &&
406  code.operands().size()==3);
407  return static_cast<code_ifthenelset &>(code);
408 }
409 
412 class code_switcht:public codet
413 {
414 public:
415  code_switcht():codet(ID_switch)
416  {
417  operands().resize(2);
418  }
419 
420  const exprt &value() const
421  {
422  return op0();
423  }
424 
426  {
427  return op0();
428  }
429 
430  const codet &body() const
431  {
432  return to_code(op1());
433  }
434 
436  {
437  return static_cast<codet &>(op1());
438  }
439 };
440 
441 inline const code_switcht &to_code_switch(const codet &code)
442 {
443  assert(code.get_statement()==ID_switch &&
444  code.operands().size()==2);
445  return static_cast<const code_switcht &>(code);
446 }
447 
449 {
450  assert(code.get_statement()==ID_switch &&
451  code.operands().size()==2);
452  return static_cast<code_switcht &>(code);
453 }
454 
457 class code_whilet:public codet
458 {
459 public:
460  code_whilet():codet(ID_while)
461  {
462  operands().resize(2);
463  }
464 
465  const exprt &cond() const
466  {
467  return op0();
468  }
469 
471  {
472  return op0();
473  }
474 
475  const codet &body() const
476  {
477  return to_code(op1());
478  }
479 
481  {
482  return static_cast<codet &>(op1());
483  }
484 };
485 
486 inline const code_whilet &to_code_while(const codet &code)
487 {
488  assert(code.get_statement()==ID_while &&
489  code.operands().size()==2);
490  return static_cast<const code_whilet &>(code);
491 }
492 
494 {
495  assert(code.get_statement()==ID_while &&
496  code.operands().size()==2);
497  return static_cast<code_whilet &>(code);
498 }
499 
502 class code_dowhilet:public codet
503 {
504 public:
505  code_dowhilet():codet(ID_dowhile)
506  {
507  operands().resize(2);
508  }
509 
510  const exprt &cond() const
511  {
512  return op0();
513  }
514 
516  {
517  return op0();
518  }
519 
520  const codet &body() const
521  {
522  return to_code(op1());
523  }
524 
526  {
527  return static_cast<codet &>(op1());
528  }
529 };
530 
531 inline const code_dowhilet &to_code_dowhile(const codet &code)
532 {
533  assert(code.get_statement()==ID_dowhile &&
534  code.operands().size()==2);
535  return static_cast<const code_dowhilet &>(code);
536 }
537 
539 {
540  assert(code.get_statement()==ID_dowhile &&
541  code.operands().size()==2);
542  return static_cast<code_dowhilet &>(code);
543 }
544 
547 class code_fort:public codet
548 {
549 public:
550  code_fort():codet(ID_for)
551  {
552  operands().resize(4);
553  }
554 
555  // nil or a statement
556  const exprt &init() const
557  {
558  return op0();
559  }
560 
562  {
563  return op0();
564  }
565 
566  const exprt &cond() const
567  {
568  return op1();
569  }
570 
572  {
573  return op1();
574  }
575 
576  const exprt &iter() const
577  {
578  return op2();
579  }
580 
582  {
583  return op2();
584  }
585 
586  const codet &body() const
587  {
588  return to_code(op3());
589  }
590 
592  {
593  return static_cast<codet &>(op3());
594  }
595 };
596 
597 inline const code_fort &to_code_for(const codet &code)
598 {
599  assert(code.get_statement()==ID_for &&
600  code.operands().size()==4);
601  return static_cast<const code_fort &>(code);
602 }
603 
605 {
606  assert(code.get_statement()==ID_for &&
607  code.operands().size()==4);
608  return static_cast<code_fort &>(code);
609 }
610 
613 class code_gotot:public codet
614 {
615 public:
616  code_gotot():codet(ID_goto)
617  {
618  }
619 
620  explicit code_gotot(const irep_idt &label):codet(ID_goto)
621  {
622  set_destination(label);
623  }
624 
625  void set_destination(const irep_idt &label)
626  {
627  set(ID_destination, label);
628  }
629 
630  const irep_idt &get_destination() const
631  {
632  return get(ID_destination);
633  }
634 };
635 
636 inline const code_gotot &to_code_goto(const codet &code)
637 {
638  assert(code.get_statement()==ID_goto &&
639  code.operands().empty());
640  return static_cast<const code_gotot &>(code);
641 }
642 
644 {
645  assert(code.get_statement()==ID_goto &&
646  code.operands().empty());
647  return static_cast<code_gotot &>(code);
648 }
649 
658 {
659 public:
660  code_function_callt():codet(ID_function_call)
661  {
662  operands().resize(3);
663  lhs().make_nil();
664  op2().id(ID_arguments);
665  }
666 
668  {
669  return op0();
670  }
671 
672  const exprt &lhs() const
673  {
674  return op0();
675  }
676 
677  exprt &function()
678  {
679  return op1();
680  }
681 
682  const exprt &function() const
683  {
684  return op1();
685  }
686 
688 
689  argumentst &arguments()
690  {
691  return op2().operands();
692  }
693 
694  const argumentst &arguments() const
695  {
696  return op2().operands();
697  }
698 };
699 
701 {
702  assert(code.get_statement()==ID_function_call);
703  return static_cast<const code_function_callt &>(code);
704 }
705 
707 {
708  assert(code.get_statement()==ID_function_call);
709  return static_cast<code_function_callt &>(code);
710 }
711 
714 class code_returnt:public codet
715 {
716 public:
717  code_returnt():codet(ID_return)
718  {
719  operands().resize(1);
720  op0().make_nil();
721  }
722 
723  explicit code_returnt(const exprt &_op):codet(ID_return)
724  {
725  copy_to_operands(_op);
726  }
727 
728  const exprt &return_value() const
729  {
730  return op0();
731  }
732 
734  {
735  return op0();
736  }
737 
738  bool has_return_value() const
739  {
740  if(operands().empty())
741  return false; // backwards compatibility
742  return return_value().is_not_nil();
743  }
744 };
745 
746 inline const code_returnt &to_code_return(const codet &code)
747 {
748  assert(code.get_statement()==ID_return);
749  return static_cast<const code_returnt &>(code);
750 }
751 
753 {
754  assert(code.get_statement()==ID_return);
755  return static_cast<code_returnt &>(code);
756 }
757 
760 class code_labelt:public codet
761 {
762 public:
763  code_labelt():codet(ID_label)
764  {
765  operands().resize(1);
766  }
767 
768  explicit code_labelt(const irep_idt &_label):codet(ID_label)
769  {
770  operands().resize(1);
771  set_label(_label);
772  }
773 
775  const irep_idt &_label, const codet &_code):codet(ID_label)
776  {
777  operands().resize(1);
778  set_label(_label);
779  code()=_code;
780  }
781 
782  const irep_idt &get_label() const
783  {
784  return get(ID_label);
785  }
786 
787  void set_label(const irep_idt &label)
788  {
789  set(ID_label, label);
790  }
791 
793  {
794  return static_cast<codet &>(op0());
795  }
796 
797  const codet &code() const
798  {
799  return static_cast<const codet &>(op0());
800  }
801 };
802 
803 inline const code_labelt &to_code_label(const codet &code)
804 {
805  assert(code.get_statement()==ID_label && code.operands().size()==1);
806  return static_cast<const code_labelt &>(code);
807 }
808 
810 {
811  assert(code.get_statement()==ID_label && code.operands().size()==1);
812  return static_cast<code_labelt &>(code);
813 }
814 
818 {
819 public:
820  code_switch_caset():codet(ID_switch_case)
821  {
822  operands().resize(2);
823  }
824 
826  const exprt &_case_op, const codet &_code):codet(ID_switch_case)
827  {
828  copy_to_operands(_case_op, _code);
829  }
830 
831  bool is_default() const
832  {
833  return get_bool(ID_default);
834  }
835 
836  void set_default()
837  {
838  return set(ID_default, true);
839  }
840 
841  const exprt &case_op() const
842  {
843  return op0();
844  }
845 
847  {
848  return op0();
849  }
850 
852  {
853  return static_cast<codet &>(op1());
854  }
855 
856  const codet &code() const
857  {
858  return static_cast<const codet &>(op1());
859  }
860 };
861 
862 inline const code_switch_caset &to_code_switch_case(const codet &code)
863 {
864  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
865  return static_cast<const code_switch_caset &>(code);
866 }
867 
869 {
870  assert(code.get_statement()==ID_switch_case && code.operands().size()==2);
871  return static_cast<code_switch_caset &>(code);
872 }
873 
876 class code_breakt:public codet
877 {
878 public:
879  code_breakt():codet(ID_break)
880  {
881  }
882 };
883 
884 inline const code_breakt &to_code_break(const codet &code)
885 {
886  assert(code.get_statement()==ID_break);
887  return static_cast<const code_breakt &>(code);
888 }
889 
891 {
892  assert(code.get_statement()==ID_break);
893  return static_cast<code_breakt &>(code);
894 }
895 
898 class code_continuet:public codet
899 {
900 public:
901  code_continuet():codet(ID_continue)
902  {
903  }
904 };
905 
906 inline const code_continuet &to_code_continue(const codet &code)
907 {
908  assert(code.get_statement()==ID_continue);
909  return static_cast<const code_continuet &>(code);
910 }
911 
913 {
914  assert(code.get_statement()==ID_continue);
915  return static_cast<code_continuet &>(code);
916 }
917 
920 class code_asmt:public codet
921 {
922 public:
923  code_asmt():codet(ID_asm)
924  {
925  }
926 
927  explicit code_asmt(const exprt &expr):codet(ID_asm)
928  {
929  copy_to_operands(expr);
930  }
931 
932  const irep_idt &get_flavor() const
933  {
934  return get(ID_flavor);
935  }
936 
937  void set_flavor(const irep_idt &f)
938  {
939  set(ID_flavor, f);
940  }
941 };
942 
944 {
945  assert(code.get_statement()==ID_asm);
946  return static_cast<code_asmt &>(code);
947 }
948 
949 inline const code_asmt &to_code_asm(const codet &code)
950 {
951  assert(code.get_statement()==ID_asm);
952  return static_cast<const code_asmt &>(code);
953 }
954 
958 {
959 public:
960  code_expressiont():codet(ID_expression)
961  {
962  operands().resize(1);
963  }
964 
965  explicit code_expressiont(const exprt &expr):codet(ID_expression)
966  {
967  copy_to_operands(expr);
968  }
969 
970  const exprt &expression() const
971  {
972  return op0();
973  }
974 
976  {
977  return op0();
978  }
979 };
980 
982 {
983  assert(code.get_statement()==ID_expression &&
984  code.operands().size()==1);
985  return static_cast<code_expressiont &>(code);
986 }
987 
988 inline const code_expressiont &to_code_expression(const codet &code)
989 {
990  assert(code.get_statement()==ID_expression &&
991  code.operands().size()==1);
992  return static_cast<const code_expressiont &>(code);
993 }
994 
998 {
999 public:
1000  explicit side_effect_exprt(const irep_idt &statement):
1001  exprt(ID_side_effect)
1002  {
1003  set_statement(statement);
1004  }
1005 
1006  side_effect_exprt(const irep_idt &statement, const typet &_type):
1007  exprt(ID_side_effect, _type)
1008  {
1009  set_statement(statement);
1010  }
1011 
1012  const irep_idt &get_statement() const
1013  {
1014  return get(ID_statement);
1015  }
1016 
1017  void set_statement(const irep_idt &statement)
1018  {
1019  return set(ID_statement, statement);
1020  }
1021 };
1022 
1024 {
1025  assert(expr.id()==ID_side_effect);
1026  return static_cast<side_effect_exprt &>(expr);
1027 }
1028 
1029 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1030 {
1031  assert(expr.id()==ID_side_effect);
1032  return static_cast<const side_effect_exprt &>(expr);
1033 }
1034 
1038 {
1039 public:
1041  {
1042  }
1043 
1044  explicit side_effect_expr_nondett(const typet &_type):
1045  side_effect_exprt(ID_nondet, _type)
1046  {
1047  }
1048 };
1049 
1053 {
1054 public:
1056  {
1057  operands().resize(2);
1058  op1().id(ID_arguments);
1059  }
1060 
1061  exprt &function()
1062  {
1063  return op0();
1064  }
1065 
1066  const exprt &function() const
1067  {
1068  return op0();
1069  }
1070 
1072  {
1073  return op1().operands();
1074  }
1075 
1077  {
1078  return op1().operands();
1079  }
1080 };
1081 
1084 {
1085  assert(expr.id()==ID_side_effect);
1086  assert(expr.get(ID_statement)==ID_function_call);
1087  return static_cast<side_effect_expr_function_callt &>(expr);
1088 }
1089 
1092 {
1093  assert(expr.id()==ID_side_effect);
1094  assert(expr.get(ID_statement)==ID_function_call);
1095  return static_cast<const side_effect_expr_function_callt &>(expr);
1096 }
1097 
1101 {
1102 public:
1104  {
1105  }
1106 
1107  explicit side_effect_expr_throwt(const irept &exception_list):
1108  side_effect_exprt(ID_throw)
1109  {
1110  set(ID_exception_list, exception_list);
1111  }
1112 };
1113 
1115 {
1116  assert(expr.id()==ID_side_effect);
1117  assert(expr.get(ID_statement)==ID_throw);
1118  return static_cast<side_effect_expr_throwt &>(expr);
1119 }
1120 
1122  const exprt &expr)
1123 {
1124  assert(expr.id()==ID_side_effect);
1125  assert(expr.get(ID_statement)==ID_throw);
1126  return static_cast<const side_effect_expr_throwt &>(expr);
1127 }
1131 {
1132 public:
1134  {
1135  }
1136  explicit side_effect_expr_catcht(const irept &exception_list):
1137  side_effect_exprt(ID_push_catch)
1138  {
1139  set(ID_exception_list, exception_list);
1140  }
1141 };
1142 
1144 {
1145  assert(expr.id()==ID_side_effect);
1146  assert(expr.get(ID_statement)==ID_push_catch);
1147  return static_cast<side_effect_expr_catcht &>(expr);
1148 }
1149 
1151  const exprt &expr)
1152 {
1153  assert(expr.id()==ID_side_effect);
1154  assert(expr.get(ID_statement)==ID_push_catch);
1155  return static_cast<const side_effect_expr_catcht &>(expr);
1156 }
1157 
1161 {
1162 public:
1163  code_try_catcht():codet(ID_try_catch)
1164  {
1165  operands().resize(1);
1166  }
1167 
1169  {
1170  return static_cast<codet &>(op0());
1171  }
1172 
1173  const codet &try_code() const
1174  {
1175  return static_cast<const codet &>(op0());
1176  }
1177 
1179  {
1180  assert((2*i+2)<operands().size());
1181  return to_code_decl(to_code(operands()[2*i+1]));
1182  }
1183 
1184  const code_declt &get_catch_decl(unsigned i) const
1185  {
1186  assert((2*i+2)<operands().size());
1187  return to_code_decl(to_code(operands()[2*i+1]));
1188  }
1189 
1190  codet &get_catch_code(unsigned i)
1191  {
1192  assert((2*i+2)<operands().size());
1193  return to_code(operands()[2*i+2]);
1194  }
1195 
1196  const codet &get_catch_code(unsigned i) const
1197  {
1198  assert((2*i+2)<operands().size());
1199  return to_code(operands()[2*i+2]);
1200  }
1201 
1202  void add_catch(const code_declt &to_catch, const codet &code_catch)
1203  {
1204  operands().reserve(operands().size()+2);
1205  copy_to_operands(to_catch);
1206  copy_to_operands(code_catch);
1207  }
1208 };
1209 
1210 inline const code_try_catcht &to_code_try_catch(const codet &code)
1211 {
1212  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
1213  return static_cast<const code_try_catcht &>(code);
1214 }
1215 
1217 {
1218  assert(code.get_statement()==ID_try_catch && code.operands().size()>=3);
1219  return static_cast<code_try_catcht &>(code);
1220 }
1221 
1222 #endif // CPROVER_UTIL_STD_CODE_H
const irep_idt & get_statement() const
Definition: std_code.h:37
A side effect that pushes/pops a catch handler.
Definition: std_code.h:1130
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1083
The type of an expression.
Definition: type.h:20
const codet & then_case() const
Definition: std_code.h:370
const exprt & return_value() const
Definition: std_code.h:728
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
A `switch&#39; instruction.
Definition: std_code.h:412
exprt & init()
Definition: std_code.h:561
bool is_not_nil() const
Definition: irep.h:104
const exprt & init() const
Definition: std_code.h:556
code_assignt(const exprt &lhs, const exprt &rhs)
Definition: std_code.h:152
void set_label(const irep_idt &label)
Definition: std_code.h:787
code_gotot(const irep_idt &label)
Definition: std_code.h:620
exprt & cond()
Definition: std_code.h:365
A try/catch block.
Definition: std_code.h:1160
codet & get_catch_code(unsigned i)
Definition: std_code.h:1190
exprt & op0()
Definition: expr.h:84
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:298
const exprt & cond() const
Definition: std_code.h:465
A continue for `for&#39; and `while&#39; loops.
Definition: std_code.h:898
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
const exprt & cond() const
Definition: std_code.h:360
exprt & symbol()
Definition: std_code.h:205
const codet & body() const
Definition: std_code.h:586
codet & code()
Definition: std_code.h:851
const codet & body() const
Definition: std_code.h:520
const argumentst & arguments() const
Definition: std_code.h:694
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
source_locationt end_location() const
Definition: std_code.h:89
code_returnt(const exprt &_op)
Definition: std_code.h:723
code_assertt(const exprt &expr)
Definition: std_code.h:320
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:884
exprt & cond()
Definition: std_code.h:571
const exprt & symbol() const
Definition: std_code.h:210
codet & body()
Definition: std_code.h:480
A `goto&#39; instruction.
Definition: std_code.h:613
exprt::operandst argumentst
Definition: std_code.h:687
codet & first_statement()
Definition: std_code.cpp:39
const irep_idt & get_flavor() const
Definition: std_code.h:932
code_blockt(const std::list< codet > &_list)
Definition: std_code.h:70
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
codet & else_case()
Definition: std_code.h:390
An expression statement.
Definition: std_code.h:957
codet(const irep_idt &statement)
Definition: std_code.h:26
void set_default()
Definition: std_code.h:836
exprt & value()
Definition: std_code.h:425
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:981
A side effect that throws an exception.
Definition: std_code.h:1100
side_effect_exprt(const irep_idt &statement)
Definition: std_code.h:1000
code_assumet(const exprt &expr)
Definition: std_code.h:282
const exprt & case_op() const
Definition: std_code.h:841
exprt & assumption()
Definition: std_code.h:292
void set_flavor(const irep_idt &f)
Definition: std_code.h:937
codet & body()
Definition: std_code.h:435
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
codet & body()
Definition: std_code.h:525
exprt & assertion()
Definition: std_code.h:330
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
void add(const codet &code)
Definition: std_code.h:81
code_expressiont(const exprt &expr)
Definition: std_code.h:965
class code_blockt & make_block()
Definition: std_code.cpp:24
code_deadt()
Definition: std_code.h:237
argumentst & arguments()
Definition: std_code.h:689
codet & body()
Definition: std_code.h:591
A declaration of a local variable.
Definition: std_code.h:192
codet & last_statement()
Definition: std_code.cpp:69
exprt & rhs()
Definition: std_code.h:162
const exprt & cond() const
Definition: std_code.h:566
codet & code()
Definition: std_code.h:792
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:1184
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:531
code_skipt()
Definition: std_code.h:137
code_deadt(const exprt &symbol)
Definition: std_code.h:242
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:486
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:636
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
const codet & try_code() const
Definition: std_code.h:1173
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:1196
side_effect_exprt(const irep_idt &statement, const typet &_type)
Definition: std_code.h:1006
A label for branch targets.
Definition: std_code.h:760
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1114
code_fort()
Definition: std_code.h:550
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
const codet & code() const
Definition: std_code.h:797
const exprt & rhs() const
Definition: std_code.h:172
code_declt()
Definition: std_code.h:195
bool has_else_case() const
Definition: std_code.h:375
static side_effect_expr_catcht & to_side_effect_expr_catch(exprt &expr)
Definition: std_code.h:1143
A `while&#39; instruction.
Definition: std_code.h:457
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:862
codet & find_last_statement()
Definition: std_code.h:94
exprt & symbol()
Definition: std_code.h:247
const codet & body() const
Definition: std_code.h:430
exprt & cond()
Definition: std_code.h:515
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:441
bool has_return_value() const
Definition: std_code.h:738
std::vector< exprt > operandst
Definition: expr.h:49
const exprt & lhs() const
Definition: std_code.h:167
An assertion.
Definition: std_code.h:312
A function call side effect.
Definition: std_code.h:1052
An assumption.
Definition: std_code.h:274
exprt & case_op()
Definition: std_code.h:846
const exprt & symbol() const
Definition: std_code.h:252
side_effect_expr_nondett(const typet &_type)
Definition: std_code.h:1044
const exprt & value() const
Definition: std_code.h:420
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:906
code_gotot()
Definition: std_code.h:616
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
bool is_default() const
Definition: std_code.h:831
codet & try_code()
Definition: std_code.h:1168
Base class for all expressions.
Definition: expr.h:46
A break for `for&#39; and `while&#39; loops.
Definition: std_code.h:876
const exprt & assumption() const
Definition: std_code.h:287
A `do while&#39; instruction.
Definition: std_code.h:502
An inline assembler statement.
Definition: std_code.h:920
const exprt & iter() const
Definition: std_code.h:576
code_labelt(const irep_idt &_label)
Definition: std_code.h:768
exprt & expression()
Definition: std_code.h:975
const codet & code() const
Definition: std_code.h:856
const exprt & expression() const
Definition: std_code.h:970
code_blockt()
Definition: std_code.h:66
codet()
Definition: std_code.h:22
exprt::operandst & arguments()
Definition: std_code.h:1071
A removal of a local variable.
Definition: std_code.h:234
void make_nil()
Definition: irep.h:243
code_declt(const exprt &symbol)
Definition: std_code.h:200
code_declt & get_catch_decl(unsigned i)
Definition: std_code.h:1178
exprt & cond()
Definition: std_code.h:470
Sequential composition.
Definition: std_code.h:63
code_switch_caset(const exprt &_case_op, const codet &_code)
Definition: std_code.h:825
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const irep_idt & get_label() const
Definition: std_code.h:782
code_asmt(const exprt &expr)
Definition: std_code.h:927
Skip.
Definition: std_code.h:134
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:597
An if-then-else.
Definition: std_code.h:350
exprt & op2()
Definition: expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
const exprt::operandst & arguments() const
Definition: std_code.h:1076
const exprt & lhs() const
Definition: std_code.h:672
codet & then_case()
Definition: std_code.h:385
A switch-case.
Definition: std_code.h:817
code_asmt()
Definition: std_code.h:923
const irep_idt & get_destination() const
Definition: std_code.h:630
A statement in a programming language.
Definition: std_code.h:19
side_effect_expr_catcht(const irept &exception_list)
Definition: std_code.h:1136
Return from a function.
Definition: std_code.h:714
void set_destination(const irep_idt &label)
Definition: std_code.h:625
A `for&#39; instruction.
Definition: std_code.h:547
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
An expression containing a side effect.
Definition: std_code.h:997
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:336
operandst & operands()
Definition: expr.h:70
exprt & return_value()
Definition: std_code.h:733
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:1210
const exprt & cond() const
Definition: std_code.h:510
const codet & else_case() const
Definition: std_code.h:380
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
void set_statement(const irep_idt &statement)
Definition: std_code.h:1017
exprt & iter()
Definition: std_code.h:581
const codet & body() const
Definition: std_code.h:475
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:1202
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:943
Assignment.
Definition: std_code.h:144
side_effect_expr_throwt(const irept &exception_list)
Definition: std_code.h:1107
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
const irep_idt & get_statement() const
Definition: std_code.h:1012
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
const exprt & assertion() const
Definition: std_code.h:325
exprt & op3()
Definition: expr.h:93
code_labelt(const irep_idt &_label, const codet &_code)
Definition: std_code.h:774