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