cprover
std_code.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data structures representing statements in a program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_STD_CODE_H
11 #define CPROVER_UTIL_STD_CODE_H
12 
13 #include <list>
14 
15 #include "base_type.h"
16 #include "expr.h"
17 #include "expr_cast.h"
18 #include "invariant.h"
19 #include "std_expr.h"
20 #include "validate.h"
21 #include "validate_code.h"
22 
34 class codet:public exprt
35 {
36 public:
37  DEPRECATED("use codet(statement) instead")
38  codet():exprt(ID_code, typet(ID_code))
39  {
40  }
41 
45  explicit codet(const irep_idt &statement):
46  exprt(ID_code, typet(ID_code))
47  {
48  set_statement(statement);
49  }
50 
51  void set_statement(const irep_idt &statement)
52  {
53  set(ID_statement, statement);
54  }
55 
56  const irep_idt &get_statement() const
57  {
58  return get(ID_statement);
59  }
60 
62  const codet &first_statement() const;
64  const codet &last_statement() const;
65  class code_blockt &make_block();
66 
75  static void check(
76  const codet &code,
78  {
79  }
80 
90  static void validate(
91  const codet &code,
92  const namespacet &ns,
94  {
95  check_code(code, vm);
96  }
97 
106  static void validate_full(
107  const codet &code,
108  const namespacet &ns,
110  {
111  check_code(code, vm);
112  }
113 };
114 
115 namespace detail // NOLINT
116 {
117 
118 template<typename Tag>
119 inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
120 {
121  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
122  {
123  return ptr->get_statement() == tag;
124  }
125  return false;
126 }
127 
128 } // namespace detail
129 
130 template<> inline bool can_cast_expr<codet>(const exprt &base)
131 {
132  return base.id()==ID_code;
133 }
134 
135 // to_code has no validation other than checking the id(), so no validate_expr
136 // is provided for codet
137 
138 inline const codet &to_code(const exprt &expr)
139 {
140  PRECONDITION(expr.id() == ID_code);
141  return static_cast<const codet &>(expr);
142 }
143 
144 inline codet &to_code(exprt &expr)
145 {
146  PRECONDITION(expr.id() == ID_code);
147  return static_cast<codet &>(expr);
148 }
149 
152 class code_blockt:public codet
153 {
154 public:
155  code_blockt():codet(ID_block)
156  {
157  }
158 
159  typedef std::vector<codet> code_operandst;
160 
162  {
163  return (code_operandst &)get_sub();
164  }
165 
166  const code_operandst &statements() const
167  {
168  return (const code_operandst &)get_sub();
169  }
170 
171  static code_blockt from_list(const std::list<codet> &_list)
172  {
173  code_blockt result;
174  auto &s=result.statements();
175  s.reserve(_list.size());
176  for(const auto &c : _list)
177  s.push_back(c);
178  return result;
179  }
180 
181  explicit code_blockt(const std::vector<codet> &_statements):codet(ID_block)
182  {
183  operands()=(const std::vector<exprt> &)_statements;
184  }
185 
186  explicit code_blockt(std::vector<codet> &&_statements):codet(ID_block)
187  {
188  operands()=std::move((std::vector<exprt> &&)_statements);
189  }
190 
191  void add(const codet &code)
192  {
193  add_to_operands(code);
194  }
195 
196  void add(codet &&code)
197  {
198  add_to_operands(std::move(code));
199  }
200 
201  void add(codet code, const source_locationt &loc)
202  {
203  code.add_source_location() = loc;
204  add(code);
205  }
206 
207  void append(const code_blockt &extra_block);
208 
209  // This is the closing '}' or 'END' at the end of a block
211  {
212  return static_cast<const source_locationt &>(find(ID_C_end_location));
213  }
214 
216 };
217 
218 template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
219 {
220  return detail::can_cast_code_impl(base, ID_block);
221 }
222 
223 // to_code_block has no validation other than checking the statement(), so no
224 // validate_expr is provided for code_blockt
225 
226 inline const code_blockt &to_code_block(const codet &code)
227 {
228  PRECONDITION(code.get_statement() == ID_block);
229  return static_cast<const code_blockt &>(code);
230 }
231 
233 {
234  PRECONDITION(code.get_statement() == ID_block);
235  return static_cast<code_blockt &>(code);
236 }
237 
239 class code_skipt:public codet
240 {
241 public:
242  code_skipt():codet(ID_skip)
243  {
244  }
245 };
246 
247 template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
248 {
249  return detail::can_cast_code_impl(base, ID_skip);
250 }
251 
252 // there is no to_code_skip, so no validate_expr is provided for code_skipt
253 
258 class code_assignt:public codet
259 {
260 public:
261  code_assignt():codet(ID_assign)
262  {
263  operands().resize(2);
264  }
265 
266  code_assignt(const exprt &lhs, const exprt &rhs):codet(ID_assign)
267  {
269  }
270 
272  {
273  return op0();
274  }
275 
277  {
278  return op1();
279  }
280 
281  const exprt &lhs() const
282  {
283  return op0();
284  }
285 
286  const exprt &rhs() const
287  {
288  return op1();
289  }
290 
291  static void check(
292  const codet &code,
294  {
295  DATA_CHECK(
296  code.operands().size() == 2, "assignment must have two operands");
297  }
298 
299  static void validate(
300  const codet &code,
301  const namespacet &ns,
303  {
304  check(code, vm);
305 
306  DATA_CHECK(
307  base_type_eq(code.op0().type(), code.op1().type(), ns),
308  "lhs and rhs of assignment must have same type");
309  }
310 
311  static void validate_full(
312  const codet &code,
313  const namespacet &ns,
315  {
316  for(const exprt &op : code.operands())
317  {
318  validate_full_expr(op, ns, vm);
319  }
320 
321  validate(code, ns, vm);
322  }
323 };
324 
325 template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
326 {
327  return detail::can_cast_code_impl(base, ID_assign);
328 }
329 
330 inline void validate_expr(const code_assignt & x)
331 {
332  validate_operands(x, 2, "assignment must have two operands");
333 }
334 
335 inline const code_assignt &to_code_assign(const codet &code)
336 {
337  PRECONDITION(code.get_statement() == ID_assign);
338  code_assignt::check(code);
339  return static_cast<const code_assignt &>(code);
340 }
341 
343 {
344  PRECONDITION(code.get_statement() == ID_assign);
345  code_assignt::check(code);
346  return static_cast<code_assignt &>(code);
347 }
348 
353 class code_declt:public codet
354 {
355 public:
356  explicit code_declt(const symbol_exprt &symbol) : codet(ID_decl)
357  {
359  }
360 
362  {
363  return static_cast<symbol_exprt &>(op0());
364  }
365 
366  const symbol_exprt &symbol() const
367  {
368  return static_cast<const symbol_exprt &>(op0());
369  }
370 
371  const irep_idt &get_identifier() const
372  {
373  return symbol().get_identifier();
374  }
375 };
376 
377 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
378 {
379  return detail::can_cast_code_impl(base, ID_decl);
380 }
381 
382 inline void validate_expr(const code_declt &x)
383 {
384  validate_operands(x, 1, "decls must have one or more operands", true);
385 }
386 
387 inline const code_declt &to_code_decl(const codet &code)
388 {
389  PRECONDITION(code.get_statement() == ID_decl);
390 
391  // will be size()==1 in the future
393  code.operands().size() >= 1, "decls must have one or more operands");
395  code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\"");
396 
397  return static_cast<const code_declt &>(code);
398 }
399 
401 {
402  PRECONDITION(code.get_statement() == ID_decl);
403 
404  // will be size()==1 in the future
406  code.operands().size() >= 1, "decls must have one or more operands");
407  return static_cast<code_declt &>(code);
408 }
409 
412 class code_deadt:public codet
413 {
414 public:
415  explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead)
416  {
418  }
419 
421  {
422  return static_cast<symbol_exprt &>(op0());
423  }
424 
425  const symbol_exprt &symbol() const
426  {
427  return static_cast<const symbol_exprt &>(op0());
428  }
429 
430  const irep_idt &get_identifier() const
431  {
432  return symbol().get_identifier();
433  }
434 };
435 
436 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
437 {
438  return detail::can_cast_code_impl(base, ID_dead);
439 }
440 
441 inline void validate_expr(const code_deadt &x)
442 {
443  validate_operands(x, 1, "dead statement must have one operand");
444 }
445 
446 inline const code_deadt &to_code_dead(const codet &code)
447 {
448  PRECONDITION(code.get_statement() == ID_dead);
450  code.operands().size() == 1, "dead statement must have one operand");
452  to_unary_expr(code).op().id() == ID_symbol,
453  "dead statement must take symbol operand");
454  return static_cast<const code_deadt &>(code);
455 }
456 
458 {
459  PRECONDITION(code.get_statement() == ID_dead);
461  code.operands().size() == 1, "dead statement must have one operand");
463  to_unary_expr(code).op().id() == ID_symbol,
464  "dead statement must take symbol operand");
465  return static_cast<code_deadt &>(code);
466 }
467 
469 class code_assumet:public codet
470 {
471 public:
472  DEPRECATED("use code_assumet(expr) instead")
473  code_assumet():codet(ID_assume)
474  {
475  operands().resize(1);
476  }
477 
478  explicit code_assumet(const exprt &expr):codet(ID_assume)
479  {
480  add_to_operands(expr);
481  }
482 
483  const exprt &assumption() const
484  {
485  return op0();
486  }
487 
489  {
490  return op0();
491  }
492 };
493 
494 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
495 {
496  return detail::can_cast_code_impl(base, ID_assume);
497 }
498 
499 // to_code_assume only checks the code statement, so no validate_expr is
500 // provided for code_assumet
501 
502 inline const code_assumet &to_code_assume(const codet &code)
503 {
504  PRECONDITION(code.get_statement() == ID_assume);
505  return static_cast<const code_assumet &>(code);
506 }
507 
509 {
510  PRECONDITION(code.get_statement() == ID_assume);
511  return static_cast<code_assumet &>(code);
512 }
513 
516 class code_assertt:public codet
517 {
518 public:
519  DEPRECATED("use code_assertt(expr) instead")
520  code_assertt():codet(ID_assert)
521  {
522  operands().resize(1);
523  }
524 
525  explicit code_assertt(const exprt &expr):codet(ID_assert)
526  {
527  add_to_operands(expr);
528  }
529 
530  const exprt &assertion() const
531  {
532  return op0();
533  }
534 
536  {
537  return op0();
538  }
539 };
540 
541 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
542 {
543  return detail::can_cast_code_impl(base, ID_assert);
544 }
545 
546 // to_code_assert only checks the code statement, so no validate_expr is
547 // provided for code_assertt
548 
549 inline const code_assertt &to_code_assert(const codet &code)
550 {
551  PRECONDITION(code.get_statement() == ID_assert);
552  return static_cast<const code_assertt &>(code);
553 }
554 
556 {
557  PRECONDITION(code.get_statement() == ID_assert);
558  return static_cast<code_assertt &>(code);
559 }
560 
574  const exprt &condition, const source_locationt &source_location);
575 
578 {
579 public:
580  code_ifthenelset():codet(ID_ifthenelse)
581  {
582  operands().resize(3);
583  op1().make_nil();
584  op2().make_nil();
585  }
586 
587  const exprt &cond() const
588  {
589  return op0();
590  }
591 
593  {
594  return op0();
595  }
596 
597  const codet &then_case() const
598  {
599  return static_cast<const codet &>(op1());
600  }
601 
602  bool has_else_case() const
603  {
604  return op2().is_not_nil();
605  }
606 
607  const codet &else_case() const
608  {
609  return static_cast<const codet &>(op2());
610  }
611 
613  {
614  return static_cast<codet &>(op1());
615  }
616 
618  {
619  return static_cast<codet &>(op2());
620  }
621 };
622 
623 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
624 {
625  return detail::can_cast_code_impl(base, ID_ifthenelse);
626 }
627 
628 inline void validate_expr(const code_ifthenelset &x)
629 {
630  validate_operands(x, 3, "if-then-else must have three operands");
631 }
632 
633 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
634 {
635  PRECONDITION(code.get_statement() == ID_ifthenelse);
637  code.operands().size() == 3, "if-then-else must have three operands");
638  return static_cast<const code_ifthenelset &>(code);
639 }
640 
642 {
643  PRECONDITION(code.get_statement() == ID_ifthenelse);
645  code.operands().size() == 3, "if-then-else must have three operands");
646  return static_cast<code_ifthenelset &>(code);
647 }
648 
650 class code_switcht:public codet
651 {
652 public:
653  DEPRECATED("use code_switcht(value, body) instead")
654  code_switcht():codet(ID_switch)
655  {
656  operands().resize(2);
657  }
658 
659  code_switcht(const exprt &_value, const codet &_body) : codet(ID_switch)
660  {
661  operands().resize(2);
662  value() = _value;
663  body() = _body;
664  }
665 
666  const exprt &value() const
667  {
668  return op0();
669  }
670 
672  {
673  return op0();
674  }
675 
676  const codet &body() const
677  {
678  return to_code(op1());
679  }
680 
682  {
683  return static_cast<codet &>(op1());
684  }
685 };
686 
687 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
688 {
689  return detail::can_cast_code_impl(base, ID_switch);
690 }
691 
692 inline void validate_expr(const code_switcht &x)
693 {
694  validate_operands(x, 2, "switch must have two operands");
695 }
696 
697 inline const code_switcht &to_code_switch(const codet &code)
698 {
699  PRECONDITION(code.get_statement() == ID_switch);
700  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
701  return static_cast<const code_switcht &>(code);
702 }
703 
705 {
706  PRECONDITION(code.get_statement() == ID_switch);
707  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
708  return static_cast<code_switcht &>(code);
709 }
710 
712 class code_whilet:public codet
713 {
714 public:
715  DEPRECATED("use code_whilet(cond, body) instead")
716  code_whilet():codet(ID_while)
717  {
718  operands().resize(2);
719  }
720 
721  code_whilet(const exprt &_cond, const codet &_body) : codet(ID_while)
722  {
723  operands().resize(2);
724  cond() = _cond;
725  body() = _body;
726  }
727 
728  const exprt &cond() const
729  {
730  return op0();
731  }
732 
734  {
735  return op0();
736  }
737 
738  const codet &body() const
739  {
740  return to_code(op1());
741  }
742 
744  {
745  return static_cast<codet &>(op1());
746  }
747 };
748 
749 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
750 {
751  return detail::can_cast_code_impl(base, ID_while);
752 }
753 
754 inline void validate_expr(const code_whilet &x)
755 {
756  validate_operands(x, 2, "while must have two operands");
757 }
758 
759 inline const code_whilet &to_code_while(const codet &code)
760 {
761  PRECONDITION(code.get_statement() == ID_while);
762  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
763  return static_cast<const code_whilet &>(code);
764 }
765 
767 {
768  PRECONDITION(code.get_statement() == ID_while);
769  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
770  return static_cast<code_whilet &>(code);
771 }
772 
774 class code_dowhilet:public codet
775 {
776 public:
777  DEPRECATED("use code_dowhilet(cond, body) instead")
778  code_dowhilet():codet(ID_dowhile)
779  {
780  operands().resize(2);
781  }
782 
783  code_dowhilet(const exprt &_cond, const codet &_body) : codet(ID_dowhile)
784  {
785  operands().resize(2);
786  cond() = _cond;
787  body() = _body;
788  }
789 
790  const exprt &cond() const
791  {
792  return op0();
793  }
794 
796  {
797  return op0();
798  }
799 
800  const codet &body() const
801  {
802  return to_code(op1());
803  }
804 
806  {
807  return static_cast<codet &>(op1());
808  }
809 };
810 
811 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
812 {
813  return detail::can_cast_code_impl(base, ID_dowhile);
814 }
815 
816 inline void validate_expr(const code_dowhilet &x)
817 {
818  validate_operands(x, 2, "do-while must have two operands");
819 }
820 
821 inline const code_dowhilet &to_code_dowhile(const codet &code)
822 {
823  PRECONDITION(code.get_statement() == ID_dowhile);
825  code.operands().size() == 2, "do-while must have two operands");
826  return static_cast<const code_dowhilet &>(code);
827 }
828 
830 {
831  PRECONDITION(code.get_statement() == ID_dowhile);
833  code.operands().size() == 2, "do-while must have two operands");
834  return static_cast<code_dowhilet &>(code);
835 }
836 
838 class code_fort:public codet
839 {
840 public:
841  code_fort():codet(ID_for)
842  {
843  operands().resize(4);
844  }
845 
846  // nil or a statement
847  const exprt &init() const
848  {
849  return op0();
850  }
851 
853  {
854  return op0();
855  }
856 
857  const exprt &cond() const
858  {
859  return op1();
860  }
861 
863  {
864  return op1();
865  }
866 
867  const exprt &iter() const
868  {
869  return op2();
870  }
871 
873  {
874  return op2();
875  }
876 
877  const codet &body() const
878  {
879  return to_code(op3());
880  }
881 
883  {
884  return static_cast<codet &>(op3());
885  }
886 };
887 
888 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
889 {
890  return detail::can_cast_code_impl(base, ID_for);
891 }
892 
893 inline void validate_expr(const code_fort &x)
894 {
895  validate_operands(x, 4, "for must have four operands");
896 }
897 
898 inline const code_fort &to_code_for(const codet &code)
899 {
900  PRECONDITION(code.get_statement() == ID_for);
901  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
902  return static_cast<const code_fort &>(code);
903 }
904 
906 {
907  PRECONDITION(code.get_statement() == ID_for);
908  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
909  return static_cast<code_fort &>(code);
910 }
911 
913 class code_gotot:public codet
914 {
915 public:
916  DEPRECATED("use code_gotot(label) instead")
917  code_gotot():codet(ID_goto)
918  {
919  }
920 
921  explicit code_gotot(const irep_idt &label):codet(ID_goto)
922  {
923  set_destination(label);
924  }
925 
926  void set_destination(const irep_idt &label)
927  {
928  set(ID_destination, label);
929  }
930 
931  const irep_idt &get_destination() const
932  {
933  return get(ID_destination);
934  }
935 };
936 
937 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
938 {
939  return detail::can_cast_code_impl(base, ID_goto);
940 }
941 
942 inline void validate_expr(const code_gotot &x)
943 {
944  validate_operands(x, 0, "goto must not have operands");
945 }
946 
947 inline const code_gotot &to_code_goto(const codet &code)
948 {
949  PRECONDITION(code.get_statement() == ID_goto);
950  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
951  return static_cast<const code_gotot &>(code);
952 }
953 
955 {
956  PRECONDITION(code.get_statement() == ID_goto);
957  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
958  return static_cast<code_gotot &>(code);
959 }
960 
967 {
968 public:
969  DEPRECATED("Use code_function_callt(...) instead")
970  code_function_callt():codet(ID_function_call)
971  {
972  operands().resize(3);
973  lhs().make_nil();
974  op2().id(ID_arguments);
975  }
976 
977  explicit code_function_callt(const exprt &_function) : codet(ID_function_call)
978  {
979  operands().resize(3);
980  lhs().make_nil();
981  op2().id(ID_arguments);
982  function() = _function;
983  }
984 
986 
988  const exprt &_lhs,
989  const exprt &_function,
990  argumentst &&_arguments)
991  : code_function_callt(_function)
992  {
993  lhs() = _lhs;
994  arguments() = std::move(_arguments);
995  }
996 
998  const exprt &_lhs,
999  const exprt &_function,
1000  const argumentst &_arguments)
1001  : code_function_callt(_function)
1002  {
1003  lhs() = _lhs;
1004  arguments() = _arguments;
1005  }
1006 
1007  code_function_callt(const exprt &_function, argumentst &&_arguments)
1008  : code_function_callt(_function)
1009  {
1010  arguments() = std::move(_arguments);
1011  }
1012 
1013  code_function_callt(const exprt &_function, const argumentst &_arguments)
1014  : code_function_callt(_function)
1015  {
1016  arguments() = _arguments;
1017  }
1018 
1020  {
1021  return op0();
1022  }
1023 
1024  const exprt &lhs() const
1025  {
1026  return op0();
1027  }
1028 
1029  exprt &function()
1030  {
1031  return op1();
1032  }
1033 
1034  const exprt &function() const
1035  {
1036  return op1();
1037  }
1038 
1040  {
1041  return op2().operands();
1042  }
1043 
1044  const argumentst &arguments() const
1045  {
1046  return op2().operands();
1047  }
1048 };
1049 
1050 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
1051 {
1052  return detail::can_cast_code_impl(base, ID_function_call);
1053 }
1054 
1055 // to_code_function_call only checks the code statement, so no validate_expr is
1056 // provided for code_function_callt
1057 
1059 {
1060  PRECONDITION(code.get_statement() == ID_function_call);
1061  return static_cast<const code_function_callt &>(code);
1062 }
1063 
1065 {
1066  PRECONDITION(code.get_statement() == ID_function_call);
1067  return static_cast<code_function_callt &>(code);
1068 }
1069 
1071 class code_returnt:public codet
1072 {
1073 public:
1074  code_returnt():codet(ID_return)
1075  {
1076  operands().resize(1);
1077  op0().make_nil();
1078  }
1079 
1080  explicit code_returnt(const exprt &_op):codet(ID_return)
1081  {
1082  add_to_operands(_op);
1083  }
1084 
1085  const exprt &return_value() const
1086  {
1087  return op0();
1088  }
1089 
1091  {
1092  return op0();
1093  }
1094 
1095  bool has_return_value() const
1096  {
1097  if(operands().empty())
1098  return false; // backwards compatibility
1099  return return_value().is_not_nil();
1100  }
1101 };
1102 
1103 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
1104 {
1105  return detail::can_cast_code_impl(base, ID_return);
1106 }
1107 
1108 // to_code_return only checks the code statement, so no validate_expr is
1109 // provided for code_returnt
1110 
1111 inline const code_returnt &to_code_return(const codet &code)
1112 {
1113  PRECONDITION(code.get_statement() == ID_return);
1114  return static_cast<const code_returnt &>(code);
1115 }
1116 
1118 {
1119  PRECONDITION(code.get_statement() == ID_return);
1120  return static_cast<code_returnt &>(code);
1121 }
1122 
1124 class code_labelt:public codet
1125 {
1126 public:
1127  DEPRECATED("use code_labelt(label) instead")
1128  code_labelt():codet(ID_label)
1129  {
1130  operands().resize(1);
1131  }
1132 
1133  explicit code_labelt(const irep_idt &_label):codet(ID_label)
1134  {
1135  operands().resize(1);
1136  set_label(_label);
1137  }
1138 
1140  const irep_idt &_label, const codet &_code):codet(ID_label)
1141  {
1142  operands().resize(1);
1143  set_label(_label);
1144  code()=_code;
1145  }
1146 
1147  const irep_idt &get_label() const
1148  {
1149  return get(ID_label);
1150  }
1151 
1152  void set_label(const irep_idt &label)
1153  {
1154  set(ID_label, label);
1155  }
1156 
1158  {
1159  return static_cast<codet &>(op0());
1160  }
1161 
1162  const codet &code() const
1163  {
1164  return static_cast<const codet &>(op0());
1165  }
1166 };
1167 
1168 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
1169 {
1170  return detail::can_cast_code_impl(base, ID_label);
1171 }
1172 
1173 inline void validate_expr(const code_labelt &x)
1174 {
1175  validate_operands(x, 1, "label must have one operand");
1176 }
1177 
1178 inline const code_labelt &to_code_label(const codet &code)
1179 {
1180  PRECONDITION(code.get_statement() == ID_label);
1181  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1182  return static_cast<const code_labelt &>(code);
1183 }
1184 
1186 {
1187  PRECONDITION(code.get_statement() == ID_label);
1188  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1189  return static_cast<code_labelt &>(code);
1190 }
1191 
1195 {
1196 public:
1197  DEPRECATED("use code_switch_caset(case_op, code) instead")
1198  code_switch_caset():codet(ID_switch_case)
1199  {
1200  operands().resize(2);
1201  }
1202 
1204  const exprt &_case_op, const codet &_code):codet(ID_switch_case)
1205  {
1206  add_to_operands(_case_op, _code);
1207  }
1208 
1209  bool is_default() const
1210  {
1211  return get_bool(ID_default);
1212  }
1213 
1215  {
1216  return set(ID_default, true);
1217  }
1218 
1219  const exprt &case_op() const
1220  {
1221  return op0();
1222  }
1223 
1225  {
1226  return op0();
1227  }
1228 
1230  {
1231  return static_cast<codet &>(op1());
1232  }
1233 
1234  const codet &code() const
1235  {
1236  return static_cast<const codet &>(op1());
1237  }
1238 };
1239 
1240 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1241 {
1242  return detail::can_cast_code_impl(base, ID_switch_case);
1243 }
1244 
1245 inline void validate_expr(const code_switch_caset &x)
1246 {
1247  validate_operands(x, 2, "switch-case must have two operands");
1248 }
1249 
1250 inline const code_switch_caset &to_code_switch_case(const codet &code)
1251 {
1252  PRECONDITION(code.get_statement() == ID_switch_case);
1254  code.operands().size() == 2, "switch-case must have two operands");
1255  return static_cast<const code_switch_caset &>(code);
1256 }
1257 
1259 {
1260  PRECONDITION(code.get_statement() == ID_switch_case);
1262  code.operands().size() == 2, "switch-case must have two operands");
1263  return static_cast<code_switch_caset &>(code);
1264 }
1265 
1268 class code_breakt:public codet
1269 {
1270 public:
1271  code_breakt():codet(ID_break)
1272  {
1273  }
1274 };
1275 
1276 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1277 {
1278  return detail::can_cast_code_impl(base, ID_break);
1279 }
1280 
1281 // to_code_break only checks the code statement, so no validate_expr is
1282 // provided for code_breakt
1283 
1284 inline const code_breakt &to_code_break(const codet &code)
1285 {
1286  PRECONDITION(code.get_statement() == ID_break);
1287  return static_cast<const code_breakt &>(code);
1288 }
1289 
1291 {
1292  PRECONDITION(code.get_statement() == ID_break);
1293  return static_cast<code_breakt &>(code);
1294 }
1295 
1298 class code_continuet:public codet
1299 {
1300 public:
1301  code_continuet():codet(ID_continue)
1302  {
1303  }
1304 };
1305 
1306 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1307 {
1308  return detail::can_cast_code_impl(base, ID_continue);
1309 }
1310 
1311 // to_code_continue only checks the code statement, so no validate_expr is
1312 // provided for code_continuet
1313 
1314 inline const code_continuet &to_code_continue(const codet &code)
1315 {
1316  PRECONDITION(code.get_statement() == ID_continue);
1317  return static_cast<const code_continuet &>(code);
1318 }
1319 
1321 {
1322  PRECONDITION(code.get_statement() == ID_continue);
1323  return static_cast<code_continuet &>(code);
1324 }
1325 
1327 class code_asmt:public codet
1328 {
1329 public:
1330  code_asmt():codet(ID_asm)
1331  {
1332  }
1333 
1334  explicit code_asmt(const exprt &expr):codet(ID_asm)
1335  {
1336  add_to_operands(expr);
1337  }
1338 
1339  const irep_idt &get_flavor() const
1340  {
1341  return get(ID_flavor);
1342  }
1343 
1344  void set_flavor(const irep_idt &f)
1345  {
1346  set(ID_flavor, f);
1347  }
1348 };
1349 
1350 template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1351 {
1352  return detail::can_cast_code_impl(base, ID_asm);
1353 }
1354 
1355 // to_code_asm only checks the code statement, so no validate_expr is
1356 // provided for code_asmt
1357 
1359 {
1360  PRECONDITION(code.get_statement() == ID_asm);
1361  return static_cast<code_asmt &>(code);
1362 }
1363 
1364 inline const code_asmt &to_code_asm(const codet &code)
1365 {
1366  PRECONDITION(code.get_statement() == ID_asm);
1367  return static_cast<const code_asmt &>(code);
1368 }
1369 
1373 {
1374 public:
1375  DEPRECATED("use code_expressiont(expr) instead")
1376  code_expressiont():codet(ID_expression)
1377  {
1378  operands().resize(1);
1379  }
1380 
1381  explicit code_expressiont(const exprt &expr):codet(ID_expression)
1382  {
1383  add_to_operands(expr);
1384  }
1385 
1386  const exprt &expression() const
1387  {
1388  return op0();
1389  }
1390 
1392  {
1393  return op0();
1394  }
1395 };
1396 
1397 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1398 {
1399  return detail::can_cast_code_impl(base, ID_expression);
1400 }
1401 
1402 inline void validate_expr(const code_expressiont &x)
1403 {
1404  validate_operands(x, 1, "expression statement must have one operand");
1405 }
1406 
1408 {
1409  PRECONDITION(code.get_statement() == ID_expression);
1411  code.operands().size() == 1, "expression statement must have one operand");
1412  return static_cast<code_expressiont &>(code);
1413 }
1414 
1415 inline const code_expressiont &to_code_expression(const codet &code)
1416 {
1417  PRECONDITION(code.get_statement() == ID_expression);
1419  code.operands().size() == 1, "expression statement must have one operand");
1420  return static_cast<const code_expressiont &>(code);
1421 }
1422 
1429 {
1430 public:
1431  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
1432  explicit side_effect_exprt(const irep_idt &statement) : exprt(ID_side_effect)
1433  {
1434  set_statement(statement);
1435  }
1436 
1437  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
1438  side_effect_exprt(const irep_idt &statement, const typet &_type):
1439  exprt(ID_side_effect, _type)
1440  {
1441  set_statement(statement);
1442  }
1443 
1445  const irep_idt &statement,
1446  const typet &_type,
1447  const source_locationt &loc);
1448 
1449  const irep_idt &get_statement() const
1450  {
1451  return get(ID_statement);
1452  }
1453 
1454  void set_statement(const irep_idt &statement)
1455  {
1456  return set(ID_statement, statement);
1457  }
1458 };
1459 
1460 namespace detail // NOLINT
1461 {
1462 
1463 template<typename Tag>
1464 inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1465 {
1466  if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1467  {
1468  return ptr->get_statement() == tag;
1469  }
1470  return false;
1471 }
1472 
1473 } // namespace detail
1474 
1475 template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1476 {
1477  return base.id()==ID_side_effect;
1478 }
1479 
1480 // to_side_effect_expr only checks the id, so no validate_expr is provided for
1481 // side_effect_exprt
1482 
1484 {
1485  PRECONDITION(expr.id() == ID_side_effect);
1486  return static_cast<side_effect_exprt &>(expr);
1487 }
1488 
1489 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1490 {
1491  PRECONDITION(expr.id() == ID_side_effect);
1492  return static_cast<const side_effect_exprt &>(expr);
1493 }
1494 
1497 {
1498 public:
1499  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
1501  {
1502  set_nullable(true);
1503  }
1504 
1505  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
1506  explicit side_effect_expr_nondett(const typet &_type):
1507  side_effect_exprt(ID_nondet, _type)
1508  {
1509  set_nullable(true);
1510  }
1511 
1512  side_effect_expr_nondett(const typet &_type, const source_locationt &loc);
1513 
1514  void set_nullable(bool nullable)
1515  {
1516  set(ID_is_nondet_nullable, nullable);
1517  }
1518 
1519  bool get_nullable() const
1520  {
1521  return get_bool(ID_is_nondet_nullable);
1522  }
1523 };
1524 
1525 template<>
1527 {
1528  return detail::can_cast_side_effect_expr_impl(base, ID_nondet);
1529 }
1530 
1531 // to_side_effect_expr_nondet only checks the id, so no validate_expr is
1532 // provided for side_effect_expr_nondett
1533 
1535 {
1536  auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1537  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1538  return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
1539 }
1540 
1542  const exprt &expr)
1543 {
1544  const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1545  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1546  return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
1547 }
1548 
1551 {
1552 public:
1553  DEPRECATED(
1554  "use side_effect_expr_function_callt("
1555  "function, arguments, type, loc) instead")
1557  : side_effect_exprt(ID_function_call, typet(), source_locationt())
1558  {
1559  operands().resize(2);
1560  op1().id(ID_arguments);
1561  }
1562 
1563  DEPRECATED(
1564  "use side_effect_expr_function_callt("
1565  "function, arguments, type, loc) instead")
1567  const exprt &_function,
1568  const exprt::operandst &_arguments)
1569  : side_effect_exprt(ID_function_call)
1570  {
1571  operands().resize(2);
1572  op1().id(ID_arguments);
1573  function() = _function;
1574  arguments() = _arguments;
1575  }
1576 
1577  DEPRECATED(
1578  "use side_effect_expr_function_callt("
1579  "function, arguments, type, loc) instead")
1581  const exprt &_function,
1582  const exprt::operandst &_arguments,
1583  const typet &_type)
1584  : side_effect_exprt(ID_function_call, _type)
1585  {
1586  operands().resize(2);
1587  op1().id(ID_arguments);
1588  function() = _function;
1589  arguments() = _arguments;
1590  }
1591 
1593  const exprt &_function,
1594  const exprt::operandst &_arguments,
1595  const typet &_type,
1596  const source_locationt &loc);
1597 
1598  exprt &function()
1599  {
1600  return op0();
1601  }
1602 
1603  const exprt &function() const
1604  {
1605  return op0();
1606  }
1607 
1609  {
1610  return op1().operands();
1611  }
1612 
1614  {
1615  return op1().operands();
1616  }
1617 };
1618 
1619 template<>
1621 {
1622  return detail::can_cast_side_effect_expr_impl(base, ID_function_call);
1623 }
1624 
1625 // to_side_effect_expr_function_call only checks the id, so no validate_expr is
1626 // provided for side_effect_expr_function_callt
1627 
1630 {
1631  PRECONDITION(expr.id() == ID_side_effect);
1632  PRECONDITION(expr.get(ID_statement) == ID_function_call);
1633  return static_cast<side_effect_expr_function_callt &>(expr);
1634 }
1635 
1638 {
1639  PRECONDITION(expr.id() == ID_side_effect);
1640  PRECONDITION(expr.get(ID_statement) == ID_function_call);
1641  return static_cast<const side_effect_expr_function_callt &>(expr);
1642 }
1643 
1647 {
1648 public:
1649  DEPRECATED("use side_effect_expr_throwt(exception_list) instead")
1651  {
1652  }
1653 
1655  const irept &exception_list,
1656  const typet &type,
1657  const source_locationt &loc)
1658  : side_effect_exprt(ID_throw, type, loc)
1659  {
1660  set(ID_exception_list, exception_list);
1661  }
1662 };
1663 
1664 template<>
1666 {
1667  return detail::can_cast_side_effect_expr_impl(base, ID_throw);
1668 }
1669 
1670 // to_side_effect_expr_throw only checks the id, so no validate_expr is
1671 // provided for side_effect_expr_throwt
1672 
1674 {
1675  PRECONDITION(expr.id() == ID_side_effect);
1676  PRECONDITION(expr.get(ID_statement) == ID_throw);
1677  return static_cast<side_effect_expr_throwt &>(expr);
1678 }
1679 
1681  const exprt &expr)
1682 {
1683  PRECONDITION(expr.id() == ID_side_effect);
1684  PRECONDITION(expr.get(ID_statement) == ID_throw);
1685  return static_cast<const side_effect_expr_throwt &>(expr);
1686 }
1687 
1700 {
1701 public:
1702  code_push_catcht():codet(ID_push_catch)
1703  {
1704  set(ID_exception_list, irept(ID_exception_list));
1705  }
1706 
1708  {
1709  public:
1711  {
1712  }
1713 
1714  explicit exception_list_entryt(const irep_idt &tag)
1715  {
1716  set(ID_tag, tag);
1717  }
1718 
1719  exception_list_entryt(const irep_idt &tag, const irep_idt &label)
1720  {
1721  set(ID_tag, tag);
1722  set(ID_label, label);
1723  }
1724 
1725  void set_tag(const irep_idt &tag)
1726  {
1727  set(ID_tag, tag);
1728  }
1729 
1730  const irep_idt &get_tag() const {
1731  return get(ID_tag);
1732  }
1733 
1734  void set_label(const irep_idt &label)
1735  {
1736  set(ID_label, label);
1737  }
1738 
1739  const irep_idt &get_label() const {
1740  return get(ID_label);
1741  }
1742  };
1743 
1744  typedef std::vector<exception_list_entryt> exception_listt;
1745 
1747  const irep_idt &tag,
1748  const irep_idt &label):
1749  codet(ID_push_catch)
1750  {
1751  set(ID_exception_list, irept(ID_exception_list));
1752  exception_list().push_back(exception_list_entryt(tag, label));
1753  }
1754 
1756  return (exception_listt &)find(ID_exception_list).get_sub();
1757  }
1758 
1760  return (const exception_listt &)find(ID_exception_list).get_sub();
1761  }
1762 };
1763 
1764 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
1765 {
1766  return detail::can_cast_code_impl(base, ID_push_catch);
1767 }
1768 
1769 // to_code_push_catch only checks the code statement, so no validate_expr is
1770 // provided for code_push_catcht
1771 
1773 {
1774  PRECONDITION(code.get_statement() == ID_push_catch);
1775  return static_cast<code_push_catcht &>(code);
1776 }
1777 
1778 static inline const code_push_catcht &to_code_push_catch(const codet &code)
1779 {
1780  PRECONDITION(code.get_statement() == ID_push_catch);
1781  return static_cast<const code_push_catcht &>(code);
1782 }
1783 
1788 {
1789 public:
1790  code_pop_catcht():codet(ID_pop_catch)
1791  {
1792  }
1793 };
1794 
1795 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
1796 {
1797  return detail::can_cast_code_impl(base, ID_pop_catch);
1798 }
1799 
1800 // to_code_pop_catch only checks the code statement, so no validate_expr is
1801 // provided for code_pop_catcht
1802 
1804 {
1805  PRECONDITION(code.get_statement() == ID_pop_catch);
1806  return static_cast<code_pop_catcht &>(code);
1807 }
1808 
1809 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
1810 {
1811  PRECONDITION(code.get_statement() == ID_pop_catch);
1812  return static_cast<const code_pop_catcht &>(code);
1813 }
1814 
1819 {
1820  public:
1821  code_landingpadt():codet(ID_exception_landingpad)
1822  {
1823  operands().resize(1);
1824  }
1826  codet(ID_exception_landingpad)
1827  {
1829  }
1830  const exprt &catch_expr() const
1831  {
1832  return op0();
1833  }
1835  {
1836  return op0();
1837  }
1838 };
1839 
1840 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
1841 {
1842  return detail::can_cast_code_impl(base, ID_exception_landingpad);
1843 }
1844 
1845 // to_code_landingpad only checks the code statement, so no validate_expr is
1846 // provided for code_landingpadt
1847 
1849 {
1850  PRECONDITION(code.get_statement() == ID_exception_landingpad);
1851  return static_cast<code_landingpadt &>(code);
1852 }
1853 
1854 static inline const code_landingpadt &to_code_landingpad(const codet &code)
1855 {
1856  PRECONDITION(code.get_statement() == ID_exception_landingpad);
1857  return static_cast<const code_landingpadt &>(code);
1858 }
1859 
1862 {
1863 public:
1864  code_try_catcht():codet(ID_try_catch)
1865  {
1866  operands().resize(1);
1867  }
1868 
1870  {
1871  return static_cast<codet &>(op0());
1872  }
1873 
1874  const codet &try_code() const
1875  {
1876  return static_cast<const codet &>(op0());
1877  }
1878 
1880  {
1881  PRECONDITION((2 * i + 2) < operands().size());
1882  return to_code_decl(to_code(operands()[2*i+1]));
1883  }
1884 
1885  const code_declt &get_catch_decl(unsigned i) const
1886  {
1887  PRECONDITION((2 * i + 2) < operands().size());
1888  return to_code_decl(to_code(operands()[2*i+1]));
1889  }
1890 
1891  codet &get_catch_code(unsigned i)
1892  {
1893  PRECONDITION((2 * i + 2) < operands().size());
1894  return to_code(operands()[2*i+2]);
1895  }
1896 
1897  const codet &get_catch_code(unsigned i) const
1898  {
1899  PRECONDITION((2 * i + 2) < operands().size());
1900  return to_code(operands()[2*i+2]);
1901  }
1902 
1903  void add_catch(const code_declt &to_catch, const codet &code_catch)
1904  {
1905  add_to_operands(to_catch, code_catch);
1906  }
1907 };
1908 
1909 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
1910 {
1911  return detail::can_cast_code_impl(base, ID_try_catch);
1912 }
1913 
1914 inline void validate_expr(const code_try_catcht &x)
1915 {
1916  validate_operands(x, 3, "try-catch must have three or more operands", true);
1917 }
1918 
1919 inline const code_try_catcht &to_code_try_catch(const codet &code)
1920 {
1921  PRECONDITION(code.get_statement() == ID_try_catch);
1923  code.operands().size() >= 3, "try-catch must have three or more operands");
1924  return static_cast<const code_try_catcht &>(code);
1925 }
1926 
1928 {
1929  PRECONDITION(code.get_statement() == ID_try_catch);
1931  code.operands().size() >= 3, "try-catch must have three or more operands");
1932  return static_cast<code_try_catcht &>(code);
1933 }
1934 
1935 #endif // CPROVER_UTIL_STD_CODE_H
side_effect_expr_throwt(const irept &exception_list, const typet &type, const source_locationt &loc)
Definition: std_code.h:1654
bool can_cast_expr< code_asmt >(const exprt &base)
Definition: std_code.h:1350
const irep_idt & get_statement() const
Definition: std_code.h:56
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1629
The type of an expression, extends irept.
Definition: type.h:27
std::vector< codet > code_operandst
Definition: std_code.h:159
const codet & then_case() const
Definition: std_code.h:597
code_dowhilet(const exprt &_cond, const codet &_body)
Definition: std_code.h:783
const exprt & return_value() const
Definition: std_code.h:1085
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:387
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1744
bool can_cast_expr< code_assertt >(const exprt &base)
Definition: std_code.h:541
codet representing a switch statement.
Definition: std_code.h:650
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition: std_code.h:1764
exprt & init()
Definition: std_code.h:852
bool is_not_nil() const
Definition: irep.h:173
const exception_listt & exception_list() const
Definition: std_code.h:1759
const exprt & init() const
Definition: std_code.h:847
code_switcht(const exprt &_value, const codet &_body)
Definition: std_code.h:659
code_assignt(const exprt &lhs, const exprt &rhs)
Definition: std_code.h:266
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed, assuming that all its enclosed statements, subexpressions, etc.
Definition: std_code.h:90
void set_label(const irep_idt &label)
Definition: std_code.h:1152
code_whilet(const exprt &_cond, const codet &_body)
Definition: std_code.h:721
code_gotot(const irep_idt &label)
Definition: std_code.h:921
exprt & cond()
Definition: std_code.h:592
const code_operandst & statements() const
Definition: std_code.h:166
codet representation of a try/catch block.
Definition: std_code.h:1861
codet & get_catch_code(unsigned i)
Definition: std_code.h:1891
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition: std_code.h:1397
exprt & op0()
Definition: expr.h:84
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:502
const exprt & cond() const
Definition: std_code.h:728
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1298
codet & find_last_statement()
Definition: std_code.cpp:112
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:446
bool can_cast_expr< code_whilet >(const exprt &base)
Definition: std_code.h:749
const irep_idt & get_tag() const
Definition: std_code.h:1730
const exprt & cond() const
Definition: std_code.h:587
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
bool get_nullable() const
Definition: std_code.h:1519
bool can_cast_expr< code_blockt >(const exprt &base)
Definition: std_code.h:218
const codet & body() const
Definition: std_code.h:877
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition: std_code.h:1840
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition: std_code.h:623
codet & code()
Definition: std_code.h:1229
const codet & body() const
Definition: std_code.h:800
bool can_cast_expr< code_continuet >(const exprt &base)
Definition: std_code.h:1306
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1534
const argumentst & arguments() const
Definition: std_code.h:1044
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1699
const irep_idt & get_identifier() const
Definition: std_expr.h:176
source_locationt end_location() const
Definition: std_code.h:210
code_returnt(const exprt &_op)
Definition: std_code.h:1080
code_operandst & statements()
Definition: std_code.h:161
code_assertt(const exprt &expr)
Definition: std_code.h:525
const irep_idt & get_identifier() const
Definition: std_code.h:371
void validate_expr(const code_assignt &x)
Definition: std_code.h:330
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1284
code_push_catcht(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1746
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:119
exprt & cond()
Definition: std_code.h:862
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition: std_code.h:1803
code_blockt(std::vector< codet > &&_statements)
Definition: std_code.h:186
codet & body()
Definition: std_code.h:743
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:1464
codet representation of a goto statement.
Definition: std_code.h:913
typet & type()
Return the type of the expression.
Definition: expr.h:68
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1787
exprt::operandst argumentst
Definition: std_code.h:985
codet & first_statement()
In the case of a codet type that represents multiple statements, return the first of them...
Definition: std_code.cpp:36
const irep_idt & get_flavor() const
Definition: std_code.h:1339
exprt & catch_expr()
Definition: std_code.h:1834
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:171
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
void set_label(const irep_idt &label)
Definition: std_code.h:1734
codet & else_case()
Definition: std_code.h:617
codet representation of an expression statement.
Definition: std_code.h:1372
code_blockt create_fatal_assertion(const exprt &condition, const source_locationt &source_location)
Create a fatal assertion, which checks a condition and then halts if it does not hold.
Definition: std_code.cpp:136
codet(const irep_idt &statement)
Definition: std_code.h:45
void set_default()
Definition: std_code.h:1214
exprt & value()
Definition: std_code.h:671
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1407
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1646
side_effect_exprt(const irep_idt &statement)
Definition: std_code.h:1432
code_assumet(const exprt &expr)
Definition: std_code.h:478
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:1219
exprt & assumption()
Definition: std_code.h:488
subt & get_sub()
Definition: irep.h:317
void set_flavor(const irep_idt &f)
Definition: std_code.h:1344
codet & body()
Definition: std_code.h:681
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1483
bool can_cast_expr< code_switch_caset >(const exprt &base)
Definition: std_code.h:1240
codet & body()
Definition: std_code.h:805
void set_nullable(bool nullable)
Definition: std_code.h:1514
Templated functions to cast to specific exprt-derived classes.
exprt & assertion()
Definition: std_code.h:535
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:335
const irep_idt & id() const
Definition: irep.h:259
code_function_callt(const exprt &_function)
Definition: std_code.h:977
exprt & lhs()
Definition: std_code.h:271
void add(const codet &code)
Definition: std_code.h:191
code_expressiont(const exprt &expr)
Definition: std_code.h:1381
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
Definition: std_code.cpp:20
argumentst & arguments()
Definition: std_code.h:1039
void check_code(const codet &code, const validation_modet vm)
Check that the given code statement is well-formed (shallow checks only, i.e., enclosed statements...
codet & body()
Definition: std_code.h:882
bool can_cast_expr< code_labelt >(const exprt &base)
Definition: std_code.h:1168
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1475
A codet representing the declaration of a local variable.
Definition: std_code.h:353
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1772
codet & last_statement()
In the case of a codet type that represents multiple statements, return the last of them...
Definition: std_code.cpp:69
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
code_landingpadt(const exprt &catch_expr)
Definition: std_code.h:1825
exprt & rhs()
Definition: std_code.h:276
const exprt & cond() const
Definition: std_code.h:857
codet & code()
Definition: std_code.h:1157
void add(codet code, const source_locationt &loc)
Definition: std_code.h:201
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:1885
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:821
code_skipt()
Definition: std_code.h:242
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:759
bool can_cast_expr< code_breakt >(const exprt &base)
Definition: std_code.h:1276
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:947
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
const codet & try_code() const
Definition: std_code.h:1874
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:1897
TO_BE_DOCUMENTED.
Definition: namespace.h:79
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:291
void add(codet &&code)
Definition: std_code.h:196
codet representation of a label for branch targets.
Definition: std_code.h:1124
void set_tag(const irep_idt &tag)
Definition: std_code.h:1725
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
#define PRECONDITION(CONDITION)
Definition: invariant.h:427
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements...
Definition: std_code.h:75
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1496
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1111
exception_list_entryt(const irep_idt &tag)
Definition: std_code.h:1714
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1673
code_fort()
Definition: std_code.h:841
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition: std_code.h:1909
bool can_cast_expr< code_declt >(const exprt &base)
Definition: std_code.h:377
Base class for tree-like data structures with sharing.
Definition: irep.h:156
codet representation of a function call statement.
Definition: std_code.h:966
const codet & code() const
Definition: std_code.h:1162
const exprt & rhs() const
Definition: std_code.h:286
bool has_else_case() const
Definition: std_code.h:602
irept()
Definition: irep.h:185
codet representing a while statement.
Definition: std_code.h:712
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1250
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
code_declt(const symbol_exprt &symbol)
Definition: std_code.h:356
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition: std_code.h:1665
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1526
const symbol_exprt & symbol() const
Definition: std_code.h:425
const codet & body() const
Definition: std_code.h:676
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1620
exprt & cond()
Definition: std_code.h:795
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:697
bool has_return_value() const
Definition: std_code.h:1095
bool can_cast_expr< code_switcht >(const exprt &base)
Definition: std_code.h:687
std::vector< exprt > operandst
Definition: expr.h:57
const exprt & lhs() const
Definition: std_code.h:281
bool can_cast_expr< code_gotot >(const exprt &base)
Definition: std_code.h:937
#define DEPRECATED(msg)
Definition: deprecate.h:23
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:516
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1550
An assumption, which must hold in subsequent code.
Definition: std_code.h:469
exprt & case_op()
Definition: std_code.h:1224
const exprt & value() const
Definition: std_code.h:666
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:299
bool can_cast_expr< code_assumet >(const exprt &base)
Definition: std_code.h:494
symbol_exprt & symbol()
Definition: std_code.h:420
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1314
bool can_cast_expr< codet >(const exprt &base)
Definition: std_code.h:130
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1848
bool can_cast_expr< code_dowhilet >(const exprt &base)
Definition: std_code.h:811
symbol_exprt & symbol()
Definition: std_code.h:361
void set_statement(const irep_idt &statement)
Definition: std_code.h:51
bool is_default() const
Definition: std_code.h:1209
codet & try_code()
Definition: std_code.h:1869
Base class for all expressions.
Definition: expr.h:54
code_deadt(const symbol_exprt &symbol)
Definition: std_code.h:415
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1268
#define DATA_CHECK(condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
bool can_cast_expr< code_deadt >(const exprt &base)
Definition: std_code.h:436
const exprt & assumption() const
Definition: std_code.h:483
codet representation of a do while statement.
Definition: std_code.h:774
codet representation of an inline assembler statement.
Definition: std_code.h:1327
const exprt & iter() const
Definition: std_code.h:867
code_labelt(const irep_idt &_label)
Definition: std_code.h:1133
exprt & expression()
Definition: std_code.h:1391
const codet & code() const
Definition: std_code.h:1234
const exprt & expression() const
Definition: std_code.h:1386
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition: std_code.h:1795
exprt::operandst & arguments()
Definition: std_code.h:1608
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:412
void make_nil()
Definition: irep.h:315
code_declt & get_catch_decl(unsigned i)
Definition: std_code.h:1879
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:311
source_locationt & add_source_location()
Definition: expr.h:236
exprt & cond()
Definition: std_code.h:733
A codet representing sequential composition of program statements.
Definition: std_code.h:152
code_switch_caset(const exprt &_case_op, const codet &_code)
Definition: std_code.h:1203
const codet & to_code(const exprt &expr)
Definition: std_code.h:138
const irep_idt & get_label() const
Definition: std_code.h:1147
code_asmt(const exprt &expr)
Definition: std_code.h:1334
A codet representing a skip statement.
Definition: std_code.h:239
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:898
codet representation of an if-then-else statement.
Definition: std_code.h:577
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
const exprt & catch_expr() const
Definition: std_code.h:1830
bool can_cast_expr< code_fort >(const exprt &base)
Definition: std_code.h:888
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:226
const exprt::operandst & arguments() const
Definition: std_code.h:1613
const exprt & lhs() const
Definition: std_code.h:1024
codet & then_case()
Definition: std_code.h:612
bool can_cast_expr< code_skipt >(const exprt &base)
Definition: std_code.h:247
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1194
const irep_idt & get_destination() const
Definition: std_code.h:931
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
codet representation of a "return from a function" statement.
Definition: std_code.h:1071
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed (full check, including checks of all subexpressions) ...
Definition: std_code.h:106
void set_destination(const irep_idt &label)
Definition: std_code.h:926
codet representation of a for statement.
Definition: std_code.h:838
Base Type Computation.
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1178
const irep_idt & get_label() const
Definition: std_code.h:1739
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:474
An expression containing a side effect.
Definition: std_code.h:1428
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:549
bool can_cast_expr< code_assignt >(const exprt &base)
Definition: std_code.h:325
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:394
operandst & operands()
Definition: expr.h:78
exprt & return_value()
Definition: std_code.h:1090
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:1919
code_blockt(const std::vector< codet > &_statements)
Definition: std_code.h:181
code_function_callt(const exprt &_function, const argumentst &_arguments)
Definition: std_code.h:1013
const exprt & cond() const
Definition: std_code.h:790
const codet & else_case() const
Definition: std_code.h:607
exception_listt & exception_list()
Definition: std_code.h:1755
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:633
void set_statement(const irep_idt &statement)
Definition: std_code.h:1454
exprt & iter()
Definition: std_code.h:872
const codet & body() const
Definition: std_code.h:738
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
bool can_cast_expr< code_function_callt >(const exprt &base)
Definition: std_code.h:1050
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:1903
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1358
const symbol_exprt & symbol() const
Definition: std_code.h:366
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt&#39;s operands.
Definition: expr.h:130
const irep_idt & get_identifier() const
Definition: std_code.h:430
A codet representing an assignment in the program.
Definition: std_code.h:258
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1719
const irep_idt & get_statement() const
Definition: std_code.h:1449
code_function_callt(const exprt &_function, argumentst &&_arguments)
Definition: std_code.h:1007
code_function_callt(const exprt &_lhs, const exprt &_function, const argumentst &_arguments)
Definition: std_code.h:997
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1818
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1058
const exprt & assertion() const
Definition: std_code.h:530
code_function_callt(const exprt &_lhs, const exprt &_function, argumentst &&_arguments)
Definition: std_code.h:987
exprt & op3()
Definition: expr.h:93
bool can_cast_expr< code_returnt >(const exprt &base)
Definition: std_code.h:1103
code_labelt(const irep_idt &_label, const codet &_code)
Definition: std_code.h:1139