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(const codet &, const validation_modet)
76  {
77  }
78 
88  static void validate(
89  const codet &code,
90  const namespacet &,
92  {
93  check_code(code, vm);
94  }
95 
104  static void validate_full(
105  const codet &code,
106  const namespacet &,
108  {
109  check_code(code, vm);
110  }
111 };
112 
113 namespace detail // NOLINT
114 {
115 
116 template<typename Tag>
117 inline bool can_cast_code_impl(const exprt &expr, const Tag &tag)
118 {
119  if(const auto ptr = expr_try_dynamic_cast<codet>(expr))
120  {
121  return ptr->get_statement() == tag;
122  }
123  return false;
124 }
125 
126 } // namespace detail
127 
128 template<> inline bool can_cast_expr<codet>(const exprt &base)
129 {
130  return base.id()==ID_code;
131 }
132 
133 // to_code has no validation other than checking the id(), so no validate_expr
134 // is provided for codet
135 
136 inline const codet &to_code(const exprt &expr)
137 {
138  PRECONDITION(expr.id() == ID_code);
139  return static_cast<const codet &>(expr);
140 }
141 
142 inline codet &to_code(exprt &expr)
143 {
144  PRECONDITION(expr.id() == ID_code);
145  return static_cast<codet &>(expr);
146 }
147 
150 class code_blockt:public codet
151 {
152 public:
153  code_blockt():codet(ID_block)
154  {
155  }
156 
157  typedef std::vector<codet> code_operandst;
158 
160  {
161  return (code_operandst &)get_sub();
162  }
163 
164  const code_operandst &statements() const
165  {
166  return (const code_operandst &)get_sub();
167  }
168 
169  static code_blockt from_list(const std::list<codet> &_list)
170  {
171  code_blockt result;
172  auto &s=result.statements();
173  s.reserve(_list.size());
174  for(const auto &c : _list)
175  s.push_back(c);
176  return result;
177  }
178 
179  explicit code_blockt(const std::vector<codet> &_statements):codet(ID_block)
180  {
181  operands()=(const std::vector<exprt> &)_statements;
182  }
183 
184  explicit code_blockt(std::vector<codet> &&_statements):codet(ID_block)
185  {
186  operands()=std::move((std::vector<exprt> &&)_statements);
187  }
188 
189  void add(const codet &code)
190  {
191  add_to_operands(code);
192  }
193 
194  void add(codet &&code)
195  {
196  add_to_operands(std::move(code));
197  }
198 
199  void add(codet code, const source_locationt &loc)
200  {
201  code.add_source_location() = loc;
202  add(code);
203  }
204 
205  void append(const code_blockt &extra_block);
206 
207  // This is the closing '}' or 'END' at the end of a block
209  {
210  return static_cast<const source_locationt &>(find(ID_C_end_location));
211  }
212 
214 };
215 
216 template<> inline bool can_cast_expr<code_blockt>(const exprt &base)
217 {
218  return detail::can_cast_code_impl(base, ID_block);
219 }
220 
221 // to_code_block has no validation other than checking the statement(), so no
222 // validate_expr is provided for code_blockt
223 
224 inline const code_blockt &to_code_block(const codet &code)
225 {
226  PRECONDITION(code.get_statement() == ID_block);
227  return static_cast<const code_blockt &>(code);
228 }
229 
231 {
232  PRECONDITION(code.get_statement() == ID_block);
233  return static_cast<code_blockt &>(code);
234 }
235 
237 class code_skipt:public codet
238 {
239 public:
240  code_skipt():codet(ID_skip)
241  {
242  }
243 };
244 
245 template<> inline bool can_cast_expr<code_skipt>(const exprt &base)
246 {
247  return detail::can_cast_code_impl(base, ID_skip);
248 }
249 
250 // there is no to_code_skip, so no validate_expr is provided for code_skipt
251 
256 class code_assignt:public codet
257 {
258 public:
259  code_assignt():codet(ID_assign)
260  {
261  operands().resize(2);
262  }
263 
264  code_assignt(const exprt &lhs, const exprt &rhs):codet(ID_assign)
265  {
267  }
268 
270  {
271  return op0();
272  }
273 
275  {
276  return op1();
277  }
278 
279  const exprt &lhs() const
280  {
281  return op0();
282  }
283 
284  const exprt &rhs() const
285  {
286  return op1();
287  }
288 
289  static void check(
290  const codet &code,
292  {
293  DATA_CHECK(
294  vm, code.operands().size() == 2, "assignment must have two operands");
295  }
296 
297  static void validate(
298  const codet &code,
299  const namespacet &ns,
301  {
302  check(code, vm);
303 
304  DATA_CHECK(
305  vm,
306  base_type_eq(code.op0().type(), code.op1().type(), ns),
307  "lhs and rhs of assignment must have same type");
308  }
309 
310  static void validate_full(
311  const codet &code,
312  const namespacet &ns,
314  {
315  for(const exprt &op : code.operands())
316  {
317  validate_full_expr(op, ns, vm);
318  }
319 
320  validate(code, ns, vm);
321  }
322 };
323 
324 template<> inline bool can_cast_expr<code_assignt>(const exprt &base)
325 {
326  return detail::can_cast_code_impl(base, ID_assign);
327 }
328 
329 inline void validate_expr(const code_assignt & x)
330 {
331  validate_operands(x, 2, "assignment must have two operands");
332 }
333 
334 inline const code_assignt &to_code_assign(const codet &code)
335 {
336  PRECONDITION(code.get_statement() == ID_assign);
337  code_assignt::check(code);
338  return static_cast<const code_assignt &>(code);
339 }
340 
342 {
343  PRECONDITION(code.get_statement() == ID_assign);
344  code_assignt::check(code);
345  return static_cast<code_assignt &>(code);
346 }
347 
352 class code_declt:public codet
353 {
354 public:
355  explicit code_declt(const symbol_exprt &symbol) : codet(ID_decl)
356  {
358  }
359 
361  {
362  return static_cast<symbol_exprt &>(op0());
363  }
364 
365  const symbol_exprt &symbol() const
366  {
367  return static_cast<const symbol_exprt &>(op0());
368  }
369 
370  const irep_idt &get_identifier() const
371  {
372  return symbol().get_identifier();
373  }
374 
375  static void check(
376  const codet &code,
378  {
379  DATA_CHECK(
380  vm, code.operands().size() == 1, "declaration must have one operand");
381  DATA_CHECK(
382  vm,
383  code.op0().id() == ID_symbol,
384  "declaring a non-symbol: " +
386  }
387 };
388 
389 template<> inline bool can_cast_expr<code_declt>(const exprt &base)
390 {
391  return detail::can_cast_code_impl(base, ID_decl);
392 }
393 
394 inline void validate_expr(const code_declt &x)
395 {
396  validate_operands(x, 1, "decls must have one or more operands", true);
397 }
398 
399 inline const code_declt &to_code_decl(const codet &code)
400 {
401  PRECONDITION(code.get_statement() == ID_decl);
402 
403  // will be size()==1 in the future
405  code.operands().size() >= 1, "decls must have one or more operands");
407  code.op0().id() == ID_symbol, "decls symbols must be a \"symbol\"");
408 
409  return static_cast<const code_declt &>(code);
410 }
411 
413 {
414  PRECONDITION(code.get_statement() == ID_decl);
415 
416  // will be size()==1 in the future
418  code.operands().size() >= 1, "decls must have one or more operands");
419  return static_cast<code_declt &>(code);
420 }
421 
424 class code_deadt:public codet
425 {
426 public:
427  explicit code_deadt(const symbol_exprt &symbol) : codet(ID_dead)
428  {
430  }
431 
433  {
434  return static_cast<symbol_exprt &>(op0());
435  }
436 
437  const symbol_exprt &symbol() const
438  {
439  return static_cast<const symbol_exprt &>(op0());
440  }
441 
442  const irep_idt &get_identifier() const
443  {
444  return symbol().get_identifier();
445  }
446 
447  static void check(
448  const codet &code,
450  {
451  DATA_CHECK(
452  vm,
453  code.operands().size() == 1,
454  "removal (code_deadt) must have one operand");
455  DATA_CHECK(
456  vm,
457  code.op0().id() == ID_symbol,
458  "removing a non-symbol: " +
459  id2string(to_symbol_expr(code.op0()).get_identifier()) + "from scope");
460  }
461 };
462 
463 template<> inline bool can_cast_expr<code_deadt>(const exprt &base)
464 {
465  return detail::can_cast_code_impl(base, ID_dead);
466 }
467 
468 inline void validate_expr(const code_deadt &x)
469 {
470  validate_operands(x, 1, "dead statement must have one operand");
471 }
472 
473 inline const code_deadt &to_code_dead(const codet &code)
474 {
475  PRECONDITION(code.get_statement() == ID_dead);
477  code.operands().size() == 1, "dead statement must have one operand");
479  to_unary_expr(code).op().id() == ID_symbol,
480  "dead statement must take symbol operand");
481  return static_cast<const code_deadt &>(code);
482 }
483 
485 {
486  PRECONDITION(code.get_statement() == ID_dead);
488  code.operands().size() == 1, "dead statement must have one operand");
490  to_unary_expr(code).op().id() == ID_symbol,
491  "dead statement must take symbol operand");
492  return static_cast<code_deadt &>(code);
493 }
494 
496 class code_assumet:public codet
497 {
498 public:
499  DEPRECATED("use code_assumet(expr) instead")
500  code_assumet():codet(ID_assume)
501  {
502  operands().resize(1);
503  }
504 
505  explicit code_assumet(const exprt &expr):codet(ID_assume)
506  {
507  add_to_operands(expr);
508  }
509 
510  const exprt &assumption() const
511  {
512  return op0();
513  }
514 
516  {
517  return op0();
518  }
519 };
520 
521 template<> inline bool can_cast_expr<code_assumet>(const exprt &base)
522 {
523  return detail::can_cast_code_impl(base, ID_assume);
524 }
525 
526 // to_code_assume only checks the code statement, so no validate_expr is
527 // provided for code_assumet
528 
529 inline const code_assumet &to_code_assume(const codet &code)
530 {
531  PRECONDITION(code.get_statement() == ID_assume);
532  return static_cast<const code_assumet &>(code);
533 }
534 
536 {
537  PRECONDITION(code.get_statement() == ID_assume);
538  return static_cast<code_assumet &>(code);
539 }
540 
541 inline void validate_expr(const code_assumet &x)
542 {
543  validate_operands(x, 1, "assume must have one operand");
544 }
545 
548 class code_assertt:public codet
549 {
550 public:
551  DEPRECATED("use code_assertt(expr) instead")
552  code_assertt():codet(ID_assert)
553  {
554  operands().resize(1);
555  }
556 
557  explicit code_assertt(const exprt &expr):codet(ID_assert)
558  {
559  add_to_operands(expr);
560  }
561 
562  const exprt &assertion() const
563  {
564  return op0();
565  }
566 
568  {
569  return op0();
570  }
571 };
572 
573 template<> inline bool can_cast_expr<code_assertt>(const exprt &base)
574 {
575  return detail::can_cast_code_impl(base, ID_assert);
576 }
577 
578 // to_code_assert only checks the code statement, so no validate_expr is
579 // provided for code_assertt
580 
581 inline const code_assertt &to_code_assert(const codet &code)
582 {
583  PRECONDITION(code.get_statement() == ID_assert);
584  return static_cast<const code_assertt &>(code);
585 }
586 
588 {
589  PRECONDITION(code.get_statement() == ID_assert);
590  return static_cast<code_assertt &>(code);
591 }
592 
593 inline void validate_expr(const code_assertt &x)
594 {
595  validate_operands(x, 1, "assert must have one operand");
596 }
597 
611  const exprt &condition, const source_locationt &source_location);
612 
615 {
616 public:
617  DEPRECATED("use code_ifthenelset(condition, then_code[, else_code]) instead")
618  code_ifthenelset():codet(ID_ifthenelse)
619  {
620  operands().resize(3);
621  op1().make_nil();
622  op2().make_nil();
623  }
624 
627  const exprt &condition,
628  const codet &then_code,
629  const codet &else_code)
630  : codet(ID_ifthenelse)
631  {
632  add_to_operands(condition, then_code, else_code);
633  }
634 
636  code_ifthenelset(const exprt &condition, const codet &then_code)
637  : codet(ID_ifthenelse)
638  {
639  add_to_operands(condition, then_code, nil_exprt());
640  }
641 
642  const exprt &cond() const
643  {
644  return op0();
645  }
646 
648  {
649  return op0();
650  }
651 
652  const codet &then_case() const
653  {
654  return static_cast<const codet &>(op1());
655  }
656 
657  bool has_else_case() const
658  {
659  return op2().is_not_nil();
660  }
661 
662  const codet &else_case() const
663  {
664  return static_cast<const codet &>(op2());
665  }
666 
668  {
669  return static_cast<codet &>(op1());
670  }
671 
673  {
674  return static_cast<codet &>(op2());
675  }
676 };
677 
678 template<> inline bool can_cast_expr<code_ifthenelset>(const exprt &base)
679 {
680  return detail::can_cast_code_impl(base, ID_ifthenelse);
681 }
682 
683 inline void validate_expr(const code_ifthenelset &x)
684 {
685  validate_operands(x, 3, "if-then-else must have three operands");
686 }
687 
688 inline const code_ifthenelset &to_code_ifthenelse(const codet &code)
689 {
690  PRECONDITION(code.get_statement() == ID_ifthenelse);
692  code.operands().size() == 3, "if-then-else must have three operands");
693  return static_cast<const code_ifthenelset &>(code);
694 }
695 
697 {
698  PRECONDITION(code.get_statement() == ID_ifthenelse);
700  code.operands().size() == 3, "if-then-else must have three operands");
701  return static_cast<code_ifthenelset &>(code);
702 }
703 
705 class code_switcht:public codet
706 {
707 public:
708  DEPRECATED("use code_switcht(value, body) instead")
709  code_switcht():codet(ID_switch)
710  {
711  operands().resize(2);
712  }
713 
714  code_switcht(const exprt &_value, const codet &_body) : codet(ID_switch)
715  {
716  operands().resize(2);
717  value() = _value;
718  body() = _body;
719  }
720 
721  const exprt &value() const
722  {
723  return op0();
724  }
725 
727  {
728  return op0();
729  }
730 
731  const codet &body() const
732  {
733  return to_code(op1());
734  }
735 
737  {
738  return static_cast<codet &>(op1());
739  }
740 };
741 
742 template<> inline bool can_cast_expr<code_switcht>(const exprt &base)
743 {
744  return detail::can_cast_code_impl(base, ID_switch);
745 }
746 
747 inline void validate_expr(const code_switcht &x)
748 {
749  validate_operands(x, 2, "switch must have two operands");
750 }
751 
752 inline const code_switcht &to_code_switch(const codet &code)
753 {
754  PRECONDITION(code.get_statement() == ID_switch);
755  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
756  return static_cast<const code_switcht &>(code);
757 }
758 
760 {
761  PRECONDITION(code.get_statement() == ID_switch);
762  DATA_INVARIANT(code.operands().size() == 2, "switch must have two operands");
763  return static_cast<code_switcht &>(code);
764 }
765 
767 class code_whilet:public codet
768 {
769 public:
770  DEPRECATED("use code_whilet(cond, body) instead")
771  code_whilet():codet(ID_while)
772  {
773  operands().resize(2);
774  }
775 
776  code_whilet(const exprt &_cond, const codet &_body) : codet(ID_while)
777  {
778  operands().resize(2);
779  cond() = _cond;
780  body() = _body;
781  }
782 
783  const exprt &cond() const
784  {
785  return op0();
786  }
787 
789  {
790  return op0();
791  }
792 
793  const codet &body() const
794  {
795  return to_code(op1());
796  }
797 
799  {
800  return static_cast<codet &>(op1());
801  }
802 };
803 
804 template<> inline bool can_cast_expr<code_whilet>(const exprt &base)
805 {
806  return detail::can_cast_code_impl(base, ID_while);
807 }
808 
809 inline void validate_expr(const code_whilet &x)
810 {
811  validate_operands(x, 2, "while must have two operands");
812 }
813 
814 inline const code_whilet &to_code_while(const codet &code)
815 {
816  PRECONDITION(code.get_statement() == ID_while);
817  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
818  return static_cast<const code_whilet &>(code);
819 }
820 
822 {
823  PRECONDITION(code.get_statement() == ID_while);
824  DATA_INVARIANT(code.operands().size() == 2, "while must have two operands");
825  return static_cast<code_whilet &>(code);
826 }
827 
829 class code_dowhilet:public codet
830 {
831 public:
832  DEPRECATED("use code_dowhilet(cond, body) instead")
833  code_dowhilet():codet(ID_dowhile)
834  {
835  operands().resize(2);
836  }
837 
838  code_dowhilet(const exprt &_cond, const codet &_body) : codet(ID_dowhile)
839  {
840  operands().resize(2);
841  cond() = _cond;
842  body() = _body;
843  }
844 
845  const exprt &cond() const
846  {
847  return op0();
848  }
849 
851  {
852  return op0();
853  }
854 
855  const codet &body() const
856  {
857  return to_code(op1());
858  }
859 
861  {
862  return static_cast<codet &>(op1());
863  }
864 };
865 
866 template<> inline bool can_cast_expr<code_dowhilet>(const exprt &base)
867 {
868  return detail::can_cast_code_impl(base, ID_dowhile);
869 }
870 
871 inline void validate_expr(const code_dowhilet &x)
872 {
873  validate_operands(x, 2, "do-while must have two operands");
874 }
875 
876 inline const code_dowhilet &to_code_dowhile(const codet &code)
877 {
878  PRECONDITION(code.get_statement() == ID_dowhile);
880  code.operands().size() == 2, "do-while must have two operands");
881  return static_cast<const code_dowhilet &>(code);
882 }
883 
885 {
886  PRECONDITION(code.get_statement() == ID_dowhile);
888  code.operands().size() == 2, "do-while must have two operands");
889  return static_cast<code_dowhilet &>(code);
890 }
891 
893 class code_fort:public codet
894 {
895 public:
896  DEPRECATED("use code_fort(init, cond, iter, body) instead")
897  code_fort():codet(ID_for)
898  {
899  operands().resize(4);
900  }
901 
905  const exprt &_init,
906  const exprt &_cond,
907  const exprt &_iter,
908  const codet &_body)
909  : codet(ID_for)
910  {
911  reserve_operands(4);
912  add_to_operands(_init, _cond, _iter);
913  add_to_operands(_body);
914  }
915 
916  // nil or a statement
917  const exprt &init() const
918  {
919  return op0();
920  }
921 
923  {
924  return op0();
925  }
926 
927  const exprt &cond() const
928  {
929  return op1();
930  }
931 
933  {
934  return op1();
935  }
936 
937  const exprt &iter() const
938  {
939  return op2();
940  }
941 
943  {
944  return op2();
945  }
946 
947  const codet &body() const
948  {
949  return to_code(op3());
950  }
951 
953  {
954  return static_cast<codet &>(op3());
955  }
956 };
957 
958 template<> inline bool can_cast_expr<code_fort>(const exprt &base)
959 {
960  return detail::can_cast_code_impl(base, ID_for);
961 }
962 
963 inline void validate_expr(const code_fort &x)
964 {
965  validate_operands(x, 4, "for must have four operands");
966 }
967 
968 inline const code_fort &to_code_for(const codet &code)
969 {
970  PRECONDITION(code.get_statement() == ID_for);
971  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
972  return static_cast<const code_fort &>(code);
973 }
974 
976 {
977  PRECONDITION(code.get_statement() == ID_for);
978  DATA_INVARIANT(code.operands().size() == 4, "for must have four operands");
979  return static_cast<code_fort &>(code);
980 }
981 
983 class code_gotot:public codet
984 {
985 public:
986  DEPRECATED("use code_gotot(label) instead")
987  code_gotot():codet(ID_goto)
988  {
989  }
990 
991  explicit code_gotot(const irep_idt &label):codet(ID_goto)
992  {
993  set_destination(label);
994  }
995 
996  void set_destination(const irep_idt &label)
997  {
998  set(ID_destination, label);
999  }
1000 
1001  const irep_idt &get_destination() const
1002  {
1003  return get(ID_destination);
1004  }
1005 };
1006 
1007 template<> inline bool can_cast_expr<code_gotot>(const exprt &base)
1008 {
1009  return detail::can_cast_code_impl(base, ID_goto);
1010 }
1011 
1012 inline void validate_expr(const code_gotot &x)
1013 {
1014  validate_operands(x, 0, "goto must not have operands");
1015 }
1016 
1017 inline const code_gotot &to_code_goto(const codet &code)
1018 {
1019  PRECONDITION(code.get_statement() == ID_goto);
1020  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
1021  return static_cast<const code_gotot &>(code);
1022 }
1023 
1025 {
1026  PRECONDITION(code.get_statement() == ID_goto);
1027  DATA_INVARIANT(code.operands().empty(), "goto must not have operands");
1028  return static_cast<code_gotot &>(code);
1029 }
1030 
1037 {
1038 public:
1039  DEPRECATED("Use code_function_callt(...) instead")
1040  code_function_callt():codet(ID_function_call)
1041  {
1042  operands().resize(3);
1043  lhs().make_nil();
1044  op2().id(ID_arguments);
1045  }
1046 
1047  explicit code_function_callt(const exprt &_function) : codet(ID_function_call)
1048  {
1049  operands().resize(3);
1050  lhs().make_nil();
1051  op2().id(ID_arguments);
1052  function() = _function;
1053  }
1054 
1056 
1058  const exprt &_lhs,
1059  const exprt &_function,
1060  argumentst &&_arguments)
1061  : code_function_callt(_function)
1062  {
1063  lhs() = _lhs;
1064  arguments() = std::move(_arguments);
1065  }
1066 
1068  const exprt &_lhs,
1069  const exprt &_function,
1070  const argumentst &_arguments)
1071  : code_function_callt(_function)
1072  {
1073  lhs() = _lhs;
1074  arguments() = _arguments;
1075  }
1076 
1077  code_function_callt(const exprt &_function, argumentst &&_arguments)
1078  : code_function_callt(_function)
1079  {
1080  arguments() = std::move(_arguments);
1081  }
1082 
1083  code_function_callt(const exprt &_function, const argumentst &_arguments)
1084  : code_function_callt(_function)
1085  {
1086  arguments() = _arguments;
1087  }
1088 
1090  {
1091  return op0();
1092  }
1093 
1094  const exprt &lhs() const
1095  {
1096  return op0();
1097  }
1098 
1099  exprt &function()
1100  {
1101  return op1();
1102  }
1103 
1104  const exprt &function() const
1105  {
1106  return op1();
1107  }
1108 
1110  {
1111  return op2().operands();
1112  }
1113 
1114  const argumentst &arguments() const
1115  {
1116  return op2().operands();
1117  }
1118 
1119  static void check(
1120  const codet &code,
1122  {
1123  DATA_CHECK(
1124  vm,
1125  code.operands().size() == 3,
1126  "function calls must have three operands:\n1) expression to store the "
1127  "returned values\n2) the function being called\n3) the vector of "
1128  "arguments");
1129  }
1130 
1131  static void validate(
1132  const codet &code,
1133  const namespacet &ns,
1135  {
1136  check(code, vm);
1137 
1138  if(code.op0().id() == ID_nil)
1139  DATA_CHECK(
1140  vm,
1141  to_code_type(code.op1().type()).return_type().id() == ID_empty,
1142  "void function should not return value");
1143  else
1144  DATA_CHECK(
1145  vm,
1146  base_type_eq(
1147  code.op0().type(), to_code_type(code.op1().type()).return_type(), ns),
1148  "function returns expression of wrong type");
1149  }
1150 
1151  static void validate_full(
1152  const codet &code,
1153  const namespacet &ns,
1155  {
1156  for(const exprt &op : code.operands())
1157  {
1158  validate_full_expr(op, ns, vm);
1159  }
1160 
1161  validate(code, ns, vm);
1162  }
1163 };
1164 
1165 template<> inline bool can_cast_expr<code_function_callt>(const exprt &base)
1166 {
1167  return detail::can_cast_code_impl(base, ID_function_call);
1168 }
1169 
1170 // to_code_function_call only checks the code statement, so no validate_expr is
1171 // provided for code_function_callt
1172 
1174 {
1175  PRECONDITION(code.get_statement() == ID_function_call);
1176  return static_cast<const code_function_callt &>(code);
1177 }
1178 
1180 {
1181  PRECONDITION(code.get_statement() == ID_function_call);
1182  return static_cast<code_function_callt &>(code);
1183 }
1184 
1185 inline void validate_expr(const code_function_callt &x)
1186 {
1187  validate_operands(x, 3, "function calls must have three operands");
1188 }
1189 
1191 class code_returnt:public codet
1192 {
1193 public:
1194  code_returnt():codet(ID_return)
1195  {
1196  operands().resize(1);
1197  op0().make_nil();
1198  }
1199 
1200  explicit code_returnt(const exprt &_op):codet(ID_return)
1201  {
1202  add_to_operands(_op);
1203  }
1204 
1205  const exprt &return_value() const
1206  {
1207  return op0();
1208  }
1209 
1211  {
1212  return op0();
1213  }
1214 
1215  bool has_return_value() const
1216  {
1217  if(operands().empty())
1218  return false; // backwards compatibility
1219  return return_value().is_not_nil();
1220  }
1221 
1222  static void check(
1223  const codet &code,
1225  {
1226  DATA_CHECK(vm, code.operands().size() == 1, "return must have one operand");
1227  }
1228 };
1229 
1230 template<> inline bool can_cast_expr<code_returnt>(const exprt &base)
1231 {
1232  return detail::can_cast_code_impl(base, ID_return);
1233 }
1234 
1235 // to_code_return only checks the code statement, so no validate_expr is
1236 // provided for code_returnt
1237 
1238 inline const code_returnt &to_code_return(const codet &code)
1239 {
1240  PRECONDITION(code.get_statement() == ID_return);
1241  return static_cast<const code_returnt &>(code);
1242 }
1243 
1245 {
1246  PRECONDITION(code.get_statement() == ID_return);
1247  return static_cast<code_returnt &>(code);
1248 }
1249 
1250 inline void validate_expr(const code_returnt &x)
1251 {
1252  validate_operands(x, 1, "return must have one operand");
1253 }
1254 
1256 class code_labelt:public codet
1257 {
1258 public:
1259  DEPRECATED("use code_labelt(label) instead")
1260  code_labelt():codet(ID_label)
1261  {
1262  operands().resize(1);
1263  }
1264 
1265  explicit code_labelt(const irep_idt &_label):codet(ID_label)
1266  {
1267  operands().resize(1);
1268  set_label(_label);
1269  }
1270 
1272  const irep_idt &_label, const codet &_code):codet(ID_label)
1273  {
1274  operands().resize(1);
1275  set_label(_label);
1276  code()=_code;
1277  }
1278 
1279  const irep_idt &get_label() const
1280  {
1281  return get(ID_label);
1282  }
1283 
1284  void set_label(const irep_idt &label)
1285  {
1286  set(ID_label, label);
1287  }
1288 
1290  {
1291  return static_cast<codet &>(op0());
1292  }
1293 
1294  const codet &code() const
1295  {
1296  return static_cast<const codet &>(op0());
1297  }
1298 };
1299 
1300 template<> inline bool can_cast_expr<code_labelt>(const exprt &base)
1301 {
1302  return detail::can_cast_code_impl(base, ID_label);
1303 }
1304 
1305 inline void validate_expr(const code_labelt &x)
1306 {
1307  validate_operands(x, 1, "label must have one operand");
1308 }
1309 
1310 inline const code_labelt &to_code_label(const codet &code)
1311 {
1312  PRECONDITION(code.get_statement() == ID_label);
1313  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1314  return static_cast<const code_labelt &>(code);
1315 }
1316 
1318 {
1319  PRECONDITION(code.get_statement() == ID_label);
1320  DATA_INVARIANT(code.operands().size() == 1, "label must have one operand");
1321  return static_cast<code_labelt &>(code);
1322 }
1323 
1327 {
1328 public:
1329  DEPRECATED("use code_switch_caset(case_op, code) instead")
1330  code_switch_caset():codet(ID_switch_case)
1331  {
1332  operands().resize(2);
1333  }
1334 
1336  const exprt &_case_op, const codet &_code):codet(ID_switch_case)
1337  {
1338  add_to_operands(_case_op, _code);
1339  }
1340 
1341  bool is_default() const
1342  {
1343  return get_bool(ID_default);
1344  }
1345 
1347  {
1348  return set(ID_default, true);
1349  }
1350 
1351  const exprt &case_op() const
1352  {
1353  return op0();
1354  }
1355 
1357  {
1358  return op0();
1359  }
1360 
1362  {
1363  return static_cast<codet &>(op1());
1364  }
1365 
1366  const codet &code() const
1367  {
1368  return static_cast<const codet &>(op1());
1369  }
1370 };
1371 
1372 template<> inline bool can_cast_expr<code_switch_caset>(const exprt &base)
1373 {
1374  return detail::can_cast_code_impl(base, ID_switch_case);
1375 }
1376 
1377 inline void validate_expr(const code_switch_caset &x)
1378 {
1379  validate_operands(x, 2, "switch-case must have two operands");
1380 }
1381 
1382 inline const code_switch_caset &to_code_switch_case(const codet &code)
1383 {
1384  PRECONDITION(code.get_statement() == ID_switch_case);
1386  code.operands().size() == 2, "switch-case must have two operands");
1387  return static_cast<const code_switch_caset &>(code);
1388 }
1389 
1391 {
1392  PRECONDITION(code.get_statement() == ID_switch_case);
1394  code.operands().size() == 2, "switch-case must have two operands");
1395  return static_cast<code_switch_caset &>(code);
1396 }
1397 
1400 class code_breakt:public codet
1401 {
1402 public:
1403  code_breakt():codet(ID_break)
1404  {
1405  }
1406 };
1407 
1408 template<> inline bool can_cast_expr<code_breakt>(const exprt &base)
1409 {
1410  return detail::can_cast_code_impl(base, ID_break);
1411 }
1412 
1413 // to_code_break only checks the code statement, so no validate_expr is
1414 // provided for code_breakt
1415 
1416 inline const code_breakt &to_code_break(const codet &code)
1417 {
1418  PRECONDITION(code.get_statement() == ID_break);
1419  return static_cast<const code_breakt &>(code);
1420 }
1421 
1423 {
1424  PRECONDITION(code.get_statement() == ID_break);
1425  return static_cast<code_breakt &>(code);
1426 }
1427 
1430 class code_continuet:public codet
1431 {
1432 public:
1433  code_continuet():codet(ID_continue)
1434  {
1435  }
1436 };
1437 
1438 template<> inline bool can_cast_expr<code_continuet>(const exprt &base)
1439 {
1440  return detail::can_cast_code_impl(base, ID_continue);
1441 }
1442 
1443 // to_code_continue only checks the code statement, so no validate_expr is
1444 // provided for code_continuet
1445 
1446 inline const code_continuet &to_code_continue(const codet &code)
1447 {
1448  PRECONDITION(code.get_statement() == ID_continue);
1449  return static_cast<const code_continuet &>(code);
1450 }
1451 
1453 {
1454  PRECONDITION(code.get_statement() == ID_continue);
1455  return static_cast<code_continuet &>(code);
1456 }
1457 
1459 class code_asmt:public codet
1460 {
1461 public:
1462  code_asmt():codet(ID_asm)
1463  {
1464  }
1465 
1466  explicit code_asmt(const exprt &expr):codet(ID_asm)
1467  {
1468  add_to_operands(expr);
1469  }
1470 
1471  const irep_idt &get_flavor() const
1472  {
1473  return get(ID_flavor);
1474  }
1475 
1476  void set_flavor(const irep_idt &f)
1477  {
1478  set(ID_flavor, f);
1479  }
1480 };
1481 
1482 template<> inline bool can_cast_expr<code_asmt>(const exprt &base)
1483 {
1484  return detail::can_cast_code_impl(base, ID_asm);
1485 }
1486 
1487 // to_code_asm only checks the code statement, so no validate_expr is
1488 // provided for code_asmt
1489 
1491 {
1492  PRECONDITION(code.get_statement() == ID_asm);
1493  return static_cast<code_asmt &>(code);
1494 }
1495 
1496 inline const code_asmt &to_code_asm(const codet &code)
1497 {
1498  PRECONDITION(code.get_statement() == ID_asm);
1499  return static_cast<const code_asmt &>(code);
1500 }
1501 
1505 {
1506 public:
1507  DEPRECATED("use code_expressiont(expr) instead")
1508  code_expressiont():codet(ID_expression)
1509  {
1510  operands().resize(1);
1511  }
1512 
1513  explicit code_expressiont(const exprt &expr):codet(ID_expression)
1514  {
1515  add_to_operands(expr);
1516  }
1517 
1518  const exprt &expression() const
1519  {
1520  return op0();
1521  }
1522 
1524  {
1525  return op0();
1526  }
1527 };
1528 
1529 template<> inline bool can_cast_expr<code_expressiont>(const exprt &base)
1530 {
1531  return detail::can_cast_code_impl(base, ID_expression);
1532 }
1533 
1534 inline void validate_expr(const code_expressiont &x)
1535 {
1536  validate_operands(x, 1, "expression statement must have one operand");
1537 }
1538 
1540 {
1541  PRECONDITION(code.get_statement() == ID_expression);
1543  code.operands().size() == 1, "expression statement must have one operand");
1544  return static_cast<code_expressiont &>(code);
1545 }
1546 
1547 inline const code_expressiont &to_code_expression(const codet &code)
1548 {
1549  PRECONDITION(code.get_statement() == ID_expression);
1551  code.operands().size() == 1, "expression statement must have one operand");
1552  return static_cast<const code_expressiont &>(code);
1553 }
1554 
1561 {
1562 public:
1563  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
1564  explicit side_effect_exprt(const irep_idt &statement) : exprt(ID_side_effect)
1565  {
1566  set_statement(statement);
1567  }
1568 
1569  DEPRECATED("use side_effect_exprt(statement, type, loc) instead")
1570  side_effect_exprt(const irep_idt &statement, const typet &_type):
1571  exprt(ID_side_effect, _type)
1572  {
1573  set_statement(statement);
1574  }
1575 
1577  const irep_idt &statement,
1578  const typet &_type,
1579  const source_locationt &loc)
1580  : exprt(ID_side_effect, _type)
1581  {
1582  set_statement(statement);
1583  add_source_location() = loc;
1584  }
1585 
1586  const irep_idt &get_statement() const
1587  {
1588  return get(ID_statement);
1589  }
1590 
1591  void set_statement(const irep_idt &statement)
1592  {
1593  return set(ID_statement, statement);
1594  }
1595 };
1596 
1597 namespace detail // NOLINT
1598 {
1599 
1600 template<typename Tag>
1601 inline bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
1602 {
1603  if(const auto ptr = expr_try_dynamic_cast<side_effect_exprt>(expr))
1604  {
1605  return ptr->get_statement() == tag;
1606  }
1607  return false;
1608 }
1609 
1610 } // namespace detail
1611 
1612 template<> inline bool can_cast_expr<side_effect_exprt>(const exprt &base)
1613 {
1614  return base.id()==ID_side_effect;
1615 }
1616 
1617 // to_side_effect_expr only checks the id, so no validate_expr is provided for
1618 // side_effect_exprt
1619 
1621 {
1622  PRECONDITION(expr.id() == ID_side_effect);
1623  return static_cast<side_effect_exprt &>(expr);
1624 }
1625 
1626 inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
1627 {
1628  PRECONDITION(expr.id() == ID_side_effect);
1629  return static_cast<const side_effect_exprt &>(expr);
1630 }
1631 
1634 {
1635 public:
1636  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
1638  {
1639  set_nullable(true);
1640  }
1641 
1642  DEPRECATED("use side_effect_expr_nondett(statement, type, loc) instead")
1643  explicit side_effect_expr_nondett(const typet &_type):
1644  side_effect_exprt(ID_nondet, _type)
1645  {
1646  set_nullable(true);
1647  }
1648 
1650  : side_effect_exprt(ID_nondet, _type, loc)
1651  {
1652  set_nullable(true);
1653  }
1654 
1655  void set_nullable(bool nullable)
1656  {
1657  set(ID_is_nondet_nullable, nullable);
1658  }
1659 
1660  bool get_nullable() const
1661  {
1662  return get_bool(ID_is_nondet_nullable);
1663  }
1664 };
1665 
1666 template<>
1668 {
1669  return detail::can_cast_side_effect_expr_impl(base, ID_nondet);
1670 }
1671 
1672 // to_side_effect_expr_nondet only checks the id, so no validate_expr is
1673 // provided for side_effect_expr_nondett
1674 
1676 {
1677  auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1678  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1679  return static_cast<side_effect_expr_nondett &>(side_effect_expr_nondet);
1680 }
1681 
1683  const exprt &expr)
1684 {
1685  const auto &side_effect_expr_nondet=to_side_effect_expr(expr);
1686  PRECONDITION(side_effect_expr_nondet.get_statement() == ID_nondet);
1687  return static_cast<const side_effect_expr_nondett &>(side_effect_expr_nondet);
1688 }
1689 
1692 {
1693 public:
1694  DEPRECATED(
1695  "use side_effect_expr_function_callt("
1696  "function, arguments, type, loc) instead")
1698  : side_effect_exprt(ID_function_call, typet(), source_locationt())
1699  {
1700  operands().resize(2);
1701  op1().id(ID_arguments);
1702  }
1703 
1704  DEPRECATED(
1705  "use side_effect_expr_function_callt("
1706  "function, arguments, type, loc) instead")
1708  const exprt &_function,
1709  const exprt::operandst &_arguments)
1710  : side_effect_exprt(ID_function_call)
1711  {
1712  operands().resize(2);
1713  op1().id(ID_arguments);
1714  function() = _function;
1715  arguments() = _arguments;
1716  }
1717 
1718  DEPRECATED(
1719  "use side_effect_expr_function_callt("
1720  "function, arguments, type, loc) instead")
1722  const exprt &_function,
1723  const exprt::operandst &_arguments,
1724  const typet &_type)
1725  : side_effect_exprt(ID_function_call, _type)
1726  {
1727  operands().resize(2);
1728  op1().id(ID_arguments);
1729  function() = _function;
1730  arguments() = _arguments;
1731  }
1732 
1734  const exprt &_function,
1735  const exprt::operandst &_arguments,
1736  const typet &_type,
1737  const source_locationt &loc)
1738  : side_effect_exprt(ID_function_call, _type, loc)
1739  {
1740  add_to_operands(_function, exprt(ID_arguments));
1741  arguments() = _arguments;
1742  }
1743 
1744  exprt &function()
1745  {
1746  return op0();
1747  }
1748 
1749  const exprt &function() const
1750  {
1751  return op0();
1752  }
1753 
1755  {
1756  return op1().operands();
1757  }
1758 
1760  {
1761  return op1().operands();
1762  }
1763 };
1764 
1765 template<>
1767 {
1768  return detail::can_cast_side_effect_expr_impl(base, ID_function_call);
1769 }
1770 
1771 // to_side_effect_expr_function_call only checks the id, so no validate_expr is
1772 // provided for side_effect_expr_function_callt
1773 
1776 {
1777  PRECONDITION(expr.id() == ID_side_effect);
1778  PRECONDITION(expr.get(ID_statement) == ID_function_call);
1779  return static_cast<side_effect_expr_function_callt &>(expr);
1780 }
1781 
1784 {
1785  PRECONDITION(expr.id() == ID_side_effect);
1786  PRECONDITION(expr.get(ID_statement) == ID_function_call);
1787  return static_cast<const side_effect_expr_function_callt &>(expr);
1788 }
1789 
1793 {
1794 public:
1795  DEPRECATED("use side_effect_expr_throwt(exception_list) instead")
1797  {
1798  }
1799 
1801  const irept &exception_list,
1802  const typet &type,
1803  const source_locationt &loc)
1804  : side_effect_exprt(ID_throw, type, loc)
1805  {
1806  set(ID_exception_list, exception_list);
1807  }
1808 };
1809 
1810 template<>
1812 {
1813  return detail::can_cast_side_effect_expr_impl(base, ID_throw);
1814 }
1815 
1816 // to_side_effect_expr_throw only checks the id, so no validate_expr is
1817 // provided for side_effect_expr_throwt
1818 
1820 {
1821  PRECONDITION(expr.id() == ID_side_effect);
1822  PRECONDITION(expr.get(ID_statement) == ID_throw);
1823  return static_cast<side_effect_expr_throwt &>(expr);
1824 }
1825 
1827  const exprt &expr)
1828 {
1829  PRECONDITION(expr.id() == ID_side_effect);
1830  PRECONDITION(expr.get(ID_statement) == ID_throw);
1831  return static_cast<const side_effect_expr_throwt &>(expr);
1832 }
1833 
1846 {
1847 public:
1848  code_push_catcht():codet(ID_push_catch)
1849  {
1850  set(ID_exception_list, irept(ID_exception_list));
1851  }
1852 
1854  {
1855  public:
1857  {
1858  }
1859 
1860  explicit exception_list_entryt(const irep_idt &tag)
1861  {
1862  set(ID_tag, tag);
1863  }
1864 
1865  exception_list_entryt(const irep_idt &tag, const irep_idt &label)
1866  {
1867  set(ID_tag, tag);
1868  set(ID_label, label);
1869  }
1870 
1871  void set_tag(const irep_idt &tag)
1872  {
1873  set(ID_tag, tag);
1874  }
1875 
1876  const irep_idt &get_tag() const {
1877  return get(ID_tag);
1878  }
1879 
1880  void set_label(const irep_idt &label)
1881  {
1882  set(ID_label, label);
1883  }
1884 
1885  const irep_idt &get_label() const {
1886  return get(ID_label);
1887  }
1888  };
1889 
1890  typedef std::vector<exception_list_entryt> exception_listt;
1891 
1893  const irep_idt &tag,
1894  const irep_idt &label):
1895  codet(ID_push_catch)
1896  {
1897  set(ID_exception_list, irept(ID_exception_list));
1898  exception_list().push_back(exception_list_entryt(tag, label));
1899  }
1900 
1902  return (exception_listt &)find(ID_exception_list).get_sub();
1903  }
1904 
1906  return (const exception_listt &)find(ID_exception_list).get_sub();
1907  }
1908 };
1909 
1910 template<> inline bool can_cast_expr<code_push_catcht>(const exprt &base)
1911 {
1912  return detail::can_cast_code_impl(base, ID_push_catch);
1913 }
1914 
1915 // to_code_push_catch only checks the code statement, so no validate_expr is
1916 // provided for code_push_catcht
1917 
1919 {
1920  PRECONDITION(code.get_statement() == ID_push_catch);
1921  return static_cast<code_push_catcht &>(code);
1922 }
1923 
1924 static inline const code_push_catcht &to_code_push_catch(const codet &code)
1925 {
1926  PRECONDITION(code.get_statement() == ID_push_catch);
1927  return static_cast<const code_push_catcht &>(code);
1928 }
1929 
1934 {
1935 public:
1936  code_pop_catcht():codet(ID_pop_catch)
1937  {
1938  }
1939 };
1940 
1941 template<> inline bool can_cast_expr<code_pop_catcht>(const exprt &base)
1942 {
1943  return detail::can_cast_code_impl(base, ID_pop_catch);
1944 }
1945 
1946 // to_code_pop_catch only checks the code statement, so no validate_expr is
1947 // provided for code_pop_catcht
1948 
1950 {
1951  PRECONDITION(code.get_statement() == ID_pop_catch);
1952  return static_cast<code_pop_catcht &>(code);
1953 }
1954 
1955 static inline const code_pop_catcht &to_code_pop_catch(const codet &code)
1956 {
1957  PRECONDITION(code.get_statement() == ID_pop_catch);
1958  return static_cast<const code_pop_catcht &>(code);
1959 }
1960 
1965 {
1966  public:
1967  code_landingpadt():codet(ID_exception_landingpad)
1968  {
1969  operands().resize(1);
1970  }
1972  codet(ID_exception_landingpad)
1973  {
1975  }
1976  const exprt &catch_expr() const
1977  {
1978  return op0();
1979  }
1981  {
1982  return op0();
1983  }
1984 };
1985 
1986 template<> inline bool can_cast_expr<code_landingpadt>(const exprt &base)
1987 {
1988  return detail::can_cast_code_impl(base, ID_exception_landingpad);
1989 }
1990 
1991 // to_code_landingpad only checks the code statement, so no validate_expr is
1992 // provided for code_landingpadt
1993 
1995 {
1996  PRECONDITION(code.get_statement() == ID_exception_landingpad);
1997  return static_cast<code_landingpadt &>(code);
1998 }
1999 
2000 static inline const code_landingpadt &to_code_landingpad(const codet &code)
2001 {
2002  PRECONDITION(code.get_statement() == ID_exception_landingpad);
2003  return static_cast<const code_landingpadt &>(code);
2004 }
2005 
2008 {
2009 public:
2010  DEPRECATED("use code_try_catcht(try_code) instead")
2011  code_try_catcht():codet(ID_try_catch)
2012  {
2013  operands().resize(1);
2014  }
2015 
2017  explicit code_try_catcht(const codet &_try_code) : codet(ID_try_catch)
2018  {
2019  add_to_operands(_try_code);
2020  }
2021 
2023  {
2024  return static_cast<codet &>(op0());
2025  }
2026 
2027  const codet &try_code() const
2028  {
2029  return static_cast<const codet &>(op0());
2030  }
2031 
2033  {
2034  PRECONDITION((2 * i + 2) < operands().size());
2035  return to_code_decl(to_code(operands()[2*i+1]));
2036  }
2037 
2038  const code_declt &get_catch_decl(unsigned i) const
2039  {
2040  PRECONDITION((2 * i + 2) < operands().size());
2041  return to_code_decl(to_code(operands()[2*i+1]));
2042  }
2043 
2044  codet &get_catch_code(unsigned i)
2045  {
2046  PRECONDITION((2 * i + 2) < operands().size());
2047  return to_code(operands()[2*i+2]);
2048  }
2049 
2050  const codet &get_catch_code(unsigned i) const
2051  {
2052  PRECONDITION((2 * i + 2) < operands().size());
2053  return to_code(operands()[2*i+2]);
2054  }
2055 
2056  void add_catch(const code_declt &to_catch, const codet &code_catch)
2057  {
2058  add_to_operands(to_catch, code_catch);
2059  }
2060 };
2061 
2062 template<> inline bool can_cast_expr<code_try_catcht>(const exprt &base)
2063 {
2064  return detail::can_cast_code_impl(base, ID_try_catch);
2065 }
2066 
2067 inline void validate_expr(const code_try_catcht &x)
2068 {
2069  validate_operands(x, 3, "try-catch must have three or more operands", true);
2070 }
2071 
2072 inline const code_try_catcht &to_code_try_catch(const codet &code)
2073 {
2074  PRECONDITION(code.get_statement() == ID_try_catch);
2076  code.operands().size() >= 3, "try-catch must have three or more operands");
2077  return static_cast<const code_try_catcht &>(code);
2078 }
2079 
2081 {
2082  PRECONDITION(code.get_statement() == ID_try_catch);
2084  code.operands().size() >= 3, "try-catch must have three or more operands");
2085  return static_cast<code_try_catcht &>(code);
2086 }
2087 
2088 #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:1800
bool can_cast_expr< code_asmt >(const exprt &base)
Definition: std_code.h:1482
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:1775
The type of an expression, extends irept.
Definition: type.h:27
std::vector< codet > code_operandst
Definition: std_code.h:157
const codet & then_case() const
Definition: std_code.h:652
code_dowhilet(const exprt &_cond, const codet &_body)
Definition: std_code.h:838
const exprt & return_value() const
Definition: std_code.h:1205
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1890
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:375
bool can_cast_expr< code_assertt >(const exprt &base)
Definition: std_code.h:573
codet representing a switch statement.
Definition: std_code.h:705
bool can_cast_expr< code_push_catcht >(const exprt &base)
Definition: std_code.h:1910
exprt & init()
Definition: std_code.h:922
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:170
const exception_listt & exception_list() const
Definition: std_code.h:1905
const exprt & init() const
Definition: std_code.h:917
code_switcht(const exprt &_value, const codet &_body)
Definition: std_code.h:714
code_assignt(const exprt &lhs, const exprt &rhs)
Definition: std_code.h:264
void set_label(const irep_idt &label)
Definition: std_code.h:1284
code_whilet(const exprt &_cond, const codet &_body)
Definition: std_code.h:776
code_gotot(const irep_idt &label)
Definition: std_code.h:991
exprt & cond()
Definition: std_code.h:647
const code_operandst & statements() const
Definition: std_code.h:164
codet representation of a try/catch block.
Definition: std_code.h:2007
codet & get_catch_code(unsigned i)
Definition: std_code.h:2044
bool can_cast_expr< code_expressiont >(const exprt &base)
Definition: std_code.h:1529
exprt & op0()
Definition: expr.h:84
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:529
const exprt & cond() const
Definition: std_code.h:783
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1430
codet & find_last_statement()
Definition: std_code.cpp:112
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
bool can_cast_expr< code_whilet >(const exprt &base)
Definition: std_code.h:804
const irep_idt & get_tag() const
Definition: std_code.h:1876
const exprt & cond() const
Definition: std_code.h:642
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:318
bool get_nullable() const
Definition: std_code.h:1660
bool can_cast_expr< code_blockt >(const exprt &base)
Definition: std_code.h:216
const codet & body() const
Definition: std_code.h:947
bool can_cast_expr< code_landingpadt >(const exprt &base)
Definition: std_code.h:1986
bool can_cast_expr< code_ifthenelset >(const exprt &base)
Definition: std_code.h:678
codet & code()
Definition: std_code.h:1361
const codet & body() const
Definition: std_code.h:855
bool can_cast_expr< code_continuet >(const exprt &base)
Definition: std_code.h:1438
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:1006
side_effect_expr_nondett & to_side_effect_expr_nondet(exprt &expr)
Definition: std_code.h:1675
const argumentst & arguments() const
Definition: std_code.h:1114
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1845
const irep_idt & get_identifier() const
Definition: std_expr.h:187
source_locationt end_location() const
Definition: std_code.h:208
code_returnt(const exprt &_op)
Definition: std_code.h:1200
code_operandst & statements()
Definition: std_code.h:159
code_assertt(const exprt &expr)
Definition: std_code.h:557
const irep_idt & get_identifier() const
Definition: std_code.h:370
side_effect_exprt(const irep_idt &statement, const typet &_type, const source_locationt &loc)
Definition: std_code.h:1576
exprt()
Definition: expr.h:60
void validate_expr(const code_assignt &x)
Definition: std_code.h:329
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1416
code_push_catcht(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1892
bool can_cast_code_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:117
exprt & cond()
Definition: std_code.h:932
static code_pop_catcht & to_code_pop_catch(codet &code)
Definition: std_code.h:1949
code_blockt(std::vector< codet > &&_statements)
Definition: std_code.h:184
codet & body()
Definition: std_code.h:798
bool can_cast_side_effect_expr_impl(const exprt &expr, const Tag &tag)
Definition: std_code.h:1601
codet representation of a goto statement.
Definition: std_code.h:983
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:1933
exprt::operandst argumentst
Definition: std_code.h:1055
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:1471
exprt & catch_expr()
Definition: std_code.h:1980
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:169
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:228
void set_label(const irep_idt &label)
Definition: std_code.h:1880
codet & else_case()
Definition: std_code.h:672
codet representation of an expression statement.
Definition: std_code.h:1504
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:1346
exprt & value()
Definition: std_code.h:726
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1539
A side_effect_exprt representation of a side effect that throws an exception.
Definition: std_code.h:1792
code_assumet(const exprt &expr)
Definition: std_code.h:505
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:209
const exprt & case_op() const
Definition: std_code.h:1351
exprt & assumption()
Definition: std_code.h:515
subt & get_sub()
Definition: irep.h:314
void set_flavor(const irep_idt &f)
Definition: std_code.h:1476
codet & body()
Definition: std_code.h:736
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
bool can_cast_expr< code_switch_caset >(const exprt &base)
Definition: std_code.h:1372
codet & body()
Definition: std_code.h:860
void set_nullable(bool nullable)
Definition: std_code.h:1655
Templated functions to cast to specific exprt-derived classes.
exprt & assertion()
Definition: std_code.h:567
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:256
code_function_callt(const exprt &_function)
Definition: std_code.h:1047
exprt & lhs()
Definition: std_code.h:269
void add(const codet &code)
Definition: std_code.h:189
code_expressiont(const exprt &expr)
Definition: std_code.h:1513
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
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:447
argumentst & arguments()
Definition: std_code.h:1109
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:952
bool can_cast_expr< code_labelt >(const exprt &base)
Definition: std_code.h:1300
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition: std_code.h:1612
A codet representing the declaration of a local variable.
Definition: std_code.h:352
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1918
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...
The NIL expression.
Definition: std_expr.h:4509
code_landingpadt(const exprt &catch_expr)
Definition: std_code.h:1971
code_fort(const exprt &_init, const exprt &_cond, const exprt &_iter, const codet &_body)
A statement describing a for loop with initializer _init, loop condition _cond, increment _iter...
Definition: std_code.h:904
exprt & rhs()
Definition: std_code.h:274
const exprt & cond() const
Definition: std_code.h:927
static void check(const codet &, const validation_modet)
Check that the code statement is well-formed (shallow checks only, i.e., enclosed statements...
Definition: std_code.h:75
codet & code()
Definition: std_code.h:1289
static void validate_full(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed (full check, including checks of all subexpressions) ...
Definition: std_code.h:104
void add(codet code, const source_locationt &loc)
Definition: std_code.h:199
const code_declt & get_catch_decl(unsigned i) const
Definition: std_code.h:2038
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:876
code_skipt()
Definition: std_code.h:240
code_try_catcht(const codet &_try_code)
A statement representing try _try_code catch ...
Definition: std_code.h:2017
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:814
bool can_cast_expr< code_breakt >(const exprt &base)
Definition: std_code.h:1408
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1017
API to expression classes.
exprt & op1()
Definition: expr.h:87
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1222
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:202
const codet & try_code() const
Definition: std_code.h:2027
const codet & get_catch_code(unsigned i) const
Definition: std_code.h:2050
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:289
code_ifthenelset(const exprt &condition, const codet &then_code, const codet &else_code)
An if condition then then_code else else_code statement.
Definition: std_code.h:626
void add(codet &&code)
Definition: std_code.h:194
codet representation of a label for branch targets.
Definition: std_code.h:1256
void set_tag(const irep_idt &tag)
Definition: std_code.h:1871
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:102
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
exception_list_entryt(const irep_idt &tag)
Definition: std_code.h:1860
side_effect_expr_throwt & to_side_effect_expr_throw(exprt &expr)
Definition: std_code.h:1819
bool can_cast_expr< code_try_catcht >(const exprt &base)
Definition: std_code.h:2062
bool can_cast_expr< code_declt >(const exprt &base)
Definition: std_code.h:389
Base class for tree-like data structures with sharing.
Definition: irep.h:153
codet representation of a function call statement.
Definition: std_code.h:1036
const codet & code() const
Definition: std_code.h:1294
const exprt & rhs() const
Definition: std_code.h:284
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:262
bool has_else_case() const
Definition: std_code.h:657
irept()
Definition: irep.h:182
codet representing a while statement.
Definition: std_code.h:767
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1382
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:355
code_ifthenelset(const exprt &condition, const codet &then_code)
An if condition then then_code statement (no "else" case).
Definition: std_code.h:636
bool can_cast_expr< side_effect_expr_throwt >(const exprt &base)
Definition: std_code.h:1811
bool can_cast_expr< side_effect_expr_nondett >(const exprt &base)
Definition: std_code.h:1667
const symbol_exprt & symbol() const
Definition: std_code.h:437
const codet & body() const
Definition: std_code.h:731
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition: std_code.h:1766
exprt & cond()
Definition: std_code.h:850
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:752
bool has_return_value() const
Definition: std_code.h:1215
bool can_cast_expr< code_switcht >(const exprt &base)
Definition: std_code.h:742
std::vector< exprt > operandst
Definition: expr.h:57
const exprt & lhs() const
Definition: std_code.h:279
bool can_cast_expr< code_gotot >(const exprt &base)
Definition: std_code.h:1007
#define DEPRECATED(msg)
Definition: deprecate.h:23
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:548
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
An assumption, which must hold in subsequent code.
Definition: std_code.h:496
exprt & case_op()
Definition: std_code.h:1356
const exprt & value() const
Definition: std_code.h:721
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:297
bool can_cast_expr< code_assumet >(const exprt &base)
Definition: std_code.h:521
symbol_exprt & symbol()
Definition: std_code.h:432
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1446
bool can_cast_expr< codet >(const exprt &base)
Definition: std_code.h:128
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1994
bool can_cast_expr< code_dowhilet >(const exprt &base)
Definition: std_code.h:866
symbol_exprt & symbol()
Definition: std_code.h:360
void set_statement(const irep_idt &statement)
Definition: std_code.h:51
bool is_default() const
Definition: std_code.h:1341
codet & try_code()
Definition: std_code.h:2022
Base class for all expressions.
Definition: expr.h:54
code_deadt(const symbol_exprt &symbol)
Definition: std_code.h:427
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1400
static void validate(const codet &code, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the code statement is well-formed, assuming that all its enclosed statements, subexpressions, etc.
Definition: std_code.h:88
bool can_cast_expr< code_deadt >(const exprt &base)
Definition: std_code.h:463
const exprt & assumption() const
Definition: std_code.h:510
codet representation of a do while statement.
Definition: std_code.h:829
codet representation of an inline assembler statement.
Definition: std_code.h:1459
const exprt & iter() const
Definition: std_code.h:937
code_labelt(const irep_idt &_label)
Definition: std_code.h:1265
exprt & expression()
Definition: std_code.h:1523
const codet & code() const
Definition: std_code.h:1366
const exprt & expression() const
Definition: std_code.h:1518
bool can_cast_expr< code_pop_catcht >(const exprt &base)
Definition: std_code.h:1941
exprt::operandst & arguments()
Definition: std_code.h:1754
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:424
void make_nil()
Definition: irep.h:312
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
code_declt & get_catch_decl(unsigned i)
Definition: std_code.h:2032
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:310
source_locationt & add_source_location()
Definition: expr.h:233
exprt & cond()
Definition: std_code.h:788
A codet representing sequential composition of program statements.
Definition: std_code.h:150
code_switch_caset(const exprt &_case_op, const codet &_code)
Definition: std_code.h:1335
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
const irep_idt & get_label() const
Definition: std_code.h:1279
code_asmt(const exprt &expr)
Definition: std_code.h:1466
A codet representing a skip statement.
Definition: std_code.h:237
side_effect_expr_nondett(const typet &_type, const source_locationt &loc)
Definition: std_code.h:1649
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:968
codet representation of an if-then-else statement.
Definition: std_code.h:614
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:154
exprt & op2()
Definition: expr.h:90
const exprt & catch_expr() const
Definition: std_code.h:1976
bool can_cast_expr< code_fort >(const exprt &base)
Definition: std_code.h:958
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
const exprt::operandst & arguments() const
Definition: std_code.h:1759
const exprt & lhs() const
Definition: std_code.h:1094
codet & then_case()
Definition: std_code.h:667
bool can_cast_expr< code_skipt >(const exprt &base)
Definition: std_code.h:245
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1326
const irep_idt & get_destination() const
Definition: std_code.h:1001
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:1191
void set_destination(const irep_idt &label)
Definition: std_code.h:996
codet representation of a for statement.
Definition: std_code.h:893
Base Type Computation.
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1310
const irep_idt & get_label() const
Definition: std_code.h:1885
static void validate(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1131
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
An expression containing a side effect.
Definition: std_code.h:1560
static void check(const codet &code, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1119
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:581
bool can_cast_expr< code_assignt >(const exprt &base)
Definition: std_code.h:324
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:406
operandst & operands()
Definition: expr.h:78
exprt & return_value()
Definition: std_code.h:1210
const code_try_catcht & to_code_try_catch(const codet &code)
Definition: std_code.h:2072
code_blockt(const std::vector< codet > &_statements)
Definition: std_code.h:179
code_function_callt(const exprt &_function, const argumentst &_arguments)
Definition: std_code.h:1083
const exprt & cond() const
Definition: std_code.h:845
const codet & else_case() const
Definition: std_code.h:662
exception_listt & exception_list()
Definition: std_code.h:1901
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:688
void set_statement(const irep_idt &statement)
Definition: std_code.h:1591
side_effect_expr_function_callt(const exprt &_function, const exprt::operandst &_arguments, const typet &_type, const source_locationt &loc)
Definition: std_code.h:1733
exprt & iter()
Definition: std_code.h:942
const codet & body() const
Definition: std_code.h:793
const irept & find(const irep_namet &name) const
Definition: irep.cpp:277
bool can_cast_expr< code_function_callt >(const exprt &base)
Definition: std_code.h:1165
void add_catch(const code_declt &to_catch, const codet &code_catch)
Definition: std_code.h:2056
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1490
const symbol_exprt & symbol() const
Definition: std_code.h:365
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:442
A codet representing an assignment in the program.
Definition: std_code.h:256
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
static void validate_full(const codet &code, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: std_code.h:1151
exception_list_entryt(const irep_idt &tag, const irep_idt &label)
Definition: std_code.h:1865
const irep_idt & get_statement() const
Definition: std_code.h:1586
code_function_callt(const exprt &_function, argumentst &&_arguments)
Definition: std_code.h:1077
code_function_callt(const exprt &_lhs, const exprt &_function, const argumentst &_arguments)
Definition: std_code.h:1067
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1964
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
const exprt & assertion() const
Definition: std_code.h:562
code_function_callt(const exprt &_lhs, const exprt &_function, argumentst &&_arguments)
Definition: std_code.h:1057
exprt & op3()
Definition: expr.h:93
bool can_cast_expr< code_returnt >(const exprt &base)
Definition: std_code.h:1230
code_labelt(const irep_idt &_label, const codet &_code)
Definition: std_code.h:1271