CBMC
state.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: State Encoding
4 
5 Author: Daniel Kroening, dkr@amazon.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_CPROVER_STATE_H
10 #define CPROVER_CPROVER_STATE_H
11 
13 #include <util/pointer_expr.h>
14 
15 class state_typet : public typet
16 {
17 public:
18  state_typet() : typet(ID_state)
19  {
20  }
21 };
22 
24 {
26 }
27 
28 static inline symbol_exprt state_expr()
29 {
30  return symbol_exprt(u8"\u03c2", state_typet());
31 }
32 
34 {
35 public:
37  : unary_predicate_exprt(ID_initial_state, std::move(state))
38  {
39  PRECONDITION(this->state().type().id() == ID_state);
40  }
41 
42  const exprt &state() const
43  {
44  return op();
45  }
46 
48  {
49  return op();
50  }
51 };
52 
60 {
61  PRECONDITION(expr.id() == ID_initial_state);
62  const initial_state_exprt &ret =
63  static_cast<const initial_state_exprt &>(expr);
64  validate_expr(ret);
65  return ret;
66 }
67 
70 {
71  PRECONDITION(expr.id() == ID_initial_state);
72  initial_state_exprt &ret = static_cast<initial_state_exprt &>(expr);
73  validate_expr(ret);
74  return ret;
75 }
76 
78 {
79 public:
81  : binary_exprt(
82  std::move(state),
83  ID_evaluate,
84  std::move(address),
85  std::move(type))
86  {
87  PRECONDITION(this->state().type().id() == ID_state);
88  PRECONDITION(this->address().type().id() == ID_pointer);
89  }
90 
91  // convenience constructor
94  std::move(state),
95  address,
96  to_pointer_type(address.type()).base_type())
97  {
98  }
99 
100  const exprt &state() const
101  {
102  return op0();
103  }
104 
106  {
107  return op0();
108  }
109 
110  const exprt &address() const
111  {
112  return op1();
113  }
114 
115  // helper
117  {
118  auto result = *this; // copy
119  result.state() = std::move(state);
120  return result;
121  }
122 };
123 
130 inline const evaluate_exprt &to_evaluate_expr(const exprt &expr)
131 {
132  PRECONDITION(expr.id() == ID_evaluate);
133  const evaluate_exprt &ret = static_cast<const evaluate_exprt &>(expr);
134  validate_expr(ret);
135  return ret;
136 }
137 
140 {
141  PRECONDITION(expr.id() == ID_evaluate);
142  evaluate_exprt &ret = static_cast<evaluate_exprt &>(expr);
143  validate_expr(ret);
144  return ret;
145 }
146 
148 {
149 public:
151  : ternary_exprt(
152  ID_update_state,
153  std::move(state),
154  std::move(address),
155  std::move(new_value),
156  state_typet())
157  {
158  PRECONDITION(this->state().type().id() == ID_state);
159  PRECONDITION(this->address().type().id() == ID_pointer);
160  PRECONDITION(
161  to_pointer_type(this->address().type()).base_type() ==
162  this->new_value().type());
163  }
164 
165  const exprt &state() const
166  {
167  return op0();
168  }
169 
171  {
172  return op0();
173  }
174 
175  const exprt &address() const
176  {
177  return op1();
178  }
179 
180  const exprt &new_value() const
181  {
182  return op2();
183  }
184 
185  // helper
187  {
188  auto result = *this; // copy
189  result.state() = std::move(state);
190  return result;
191  }
192 };
193 
201 {
202  PRECONDITION(expr.id() == ID_update_state);
203  const update_state_exprt &ret = static_cast<const update_state_exprt &>(expr);
204  validate_expr(ret);
205  return ret;
206 }
207 
210 {
211  PRECONDITION(expr.id() == ID_update_state);
212  update_state_exprt &ret = static_cast<update_state_exprt &>(expr);
213  validate_expr(ret);
214  return ret;
215 }
216 
218 {
219 public:
221  : binary_exprt(
222  std::move(state),
223  ID_allocate,
224  std::move(size),
225  std::move(type))
226  {
227  PRECONDITION(this->state().type().id() == ID_state);
228  }
229 
230  const exprt &state() const
231  {
232  return op0();
233  }
234 
236  {
237  return op0();
238  }
239 
240  const exprt &size() const
241  {
242  return op1();
243  }
244 
245  // helper
247  {
248  auto result = *this; // copy
249  result.state() = std::move(state);
250  return result;
251  }
252 };
253 
260 inline const allocate_exprt &to_allocate_expr(const exprt &expr)
261 {
262  PRECONDITION(expr.id() == ID_allocate);
263  const allocate_exprt &ret = static_cast<const allocate_exprt &>(expr);
264  validate_expr(ret);
265  return ret;
266 }
267 
269 {
270 public:
272  : binary_exprt(
273  std::move(state),
274  ID_allocate_state,
275  std::move(size),
276  state_typet())
277  {
278  PRECONDITION(this->state().type().id() == ID_state);
279  }
280 
281  const exprt &state() const
282  {
283  return op0();
284  }
285 
287  {
288  return op0();
289  }
290 
291  const exprt &size() const
292  {
293  return op1();
294  }
295 };
296 
304 {
305  PRECONDITION(expr.id() == ID_allocate_state);
306  const allocate_state_exprt &ret =
307  static_cast<const allocate_state_exprt &>(expr);
308  validate_expr(ret);
309  return ret;
310 }
311 
313 {
314 public:
316  : ternary_exprt(
317  ID_reallocate,
318  std::move(state),
319  std::move(address),
320  std::move(size),
321  std::move(type))
322  {
323  PRECONDITION(this->state().type().id() == ID_state);
324  }
325 
326  const exprt &state() const
327  {
328  return op0();
329  }
330 
332  {
333  return op0();
334  }
335 
336  const exprt &address() const
337  {
338  return op1();
339  }
340 
341  const exprt &size() const
342  {
343  return op2();
344  }
345 };
346 
353 inline const reallocate_exprt &to_reallocate_expr(const exprt &expr)
354 {
355  PRECONDITION(expr.id() == ID_reallocate);
356  const reallocate_exprt &ret = static_cast<const reallocate_exprt &>(expr);
357  validate_expr(ret);
358  return ret;
359 }
360 
362 {
363 public:
365  : ternary_exprt(
366  ID_allocate_state,
367  std::move(state),
368  std::move(address),
369  std::move(size),
370  state_typet())
371  {
372  PRECONDITION(this->state().type().id() == ID_state);
373  }
374 
375  const exprt &state() const
376  {
377  return op0();
378  }
379 
381  {
382  return op0();
383  }
384 
385  const exprt &address() const
386  {
387  return op1();
388  }
389 
390  const exprt &size() const
391  {
392  return op1();
393  }
394 };
395 
403 {
404  PRECONDITION(expr.id() == ID_reallocate_state);
405  const reallocate_state_exprt &ret =
406  static_cast<const reallocate_state_exprt &>(expr);
407  validate_expr(ret);
408  return ret;
409 }
410 
412 {
413 public:
415  : binary_exprt(
416  std::move(state),
417  ID_deallocate_state,
418  std::move(address),
419  state_typet())
420  {
421  PRECONDITION(this->state().type().id() == ID_state);
422  }
423 
424  const exprt &state() const
425  {
426  return op0();
427  }
428 
430  {
431  return op0();
432  }
433 
434  const exprt &address() const
435  {
436  return op1();
437  }
438 };
439 
447 {
448  PRECONDITION(expr.id() == ID_deallocate_state);
449  const deallocate_state_exprt &ret =
450  static_cast<const deallocate_state_exprt &>(expr);
451  validate_expr(ret);
452  return ret;
453 }
454 
456 {
457 public:
460  std::move(state),
461  ID_state_live_object,
462  std::move(address))
463  {
464  PRECONDITION(this->state().type().id() == ID_state);
465  PRECONDITION(this->address().type().id() == ID_pointer);
466  }
467 
468  const exprt &state() const
469  {
470  return op0();
471  }
472 
474  {
475  return op0();
476  }
477 
478  const exprt &address() const
479  {
480  return op1();
481  }
482 
483  // helper
485  {
486  auto result = *this; // copy
487  result.state() = std::move(state);
488  return result;
489  }
490 };
491 
498 inline const state_live_object_exprt &
500 {
501  PRECONDITION(expr.id() == ID_state_live_object);
502  const state_live_object_exprt &ret =
503  static_cast<const state_live_object_exprt &>(expr);
504  validate_expr(ret);
505  return ret;
506 }
507 
510 {
511  PRECONDITION(expr.id() == ID_state_live_object);
512  state_live_object_exprt &ret = static_cast<state_live_object_exprt &>(expr);
513  validate_expr(ret);
514  return ret;
515 }
516 
518 {
519 public:
522  std::move(state),
523  ID_state_writeable_object,
524  std::move(address))
525  {
526  PRECONDITION(this->state().type().id() == ID_state);
527  PRECONDITION(this->address().type().id() == ID_pointer);
528  }
529 
530  const exprt &state() const
531  {
532  return op0();
533  }
534 
536  {
537  return op0();
538  }
539 
540  const exprt &address() const
541  {
542  return op1();
543  }
544 };
545 
552 inline const state_writeable_object_exprt &
554 {
555  PRECONDITION(expr.id() == ID_state_writeable_object);
556  const state_writeable_object_exprt &ret =
557  static_cast<const state_writeable_object_exprt &>(expr);
558  validate_expr(ret);
559  return ret;
560 }
561 
564 {
565  PRECONDITION(expr.id() == ID_state_writeable_object);
567  static_cast<state_writeable_object_exprt &>(expr);
568  validate_expr(ret);
569  return ret;
570 }
571 
573 {
574 public:
577  std::move(state),
578  ID_state_is_cstring,
579  std::move(address))
580  {
581  PRECONDITION(this->state().type().id() == ID_state);
582  PRECONDITION(this->address().type().id() == ID_pointer);
583  }
584 
585  const exprt &state() const
586  {
587  return op0();
588  }
589 
591  {
592  return op0();
593  }
594 
595  const exprt &address() const
596  {
597  return op1();
598  }
599 
600  // helper
602  {
603  auto result = *this; // copy
604  result.state() = std::move(state);
605  return result;
606  }
607 };
608 
616 {
617  PRECONDITION(expr.id() == ID_state_is_cstring);
618  const state_is_cstring_exprt &ret =
619  static_cast<const state_is_cstring_exprt &>(expr);
620  validate_expr(ret);
621  return ret;
622 }
623 
626 {
627  PRECONDITION(expr.id() == ID_state_is_cstring);
628  state_is_cstring_exprt &ret = static_cast<state_is_cstring_exprt &>(expr);
629  validate_expr(ret);
630  return ret;
631 }
632 
634 {
635 public:
637  : binary_exprt(
638  std::move(state),
639  ID_state_cstrlen,
640  std::move(address),
641  std::move(type))
642  {
643  PRECONDITION(this->state().type().id() == ID_state);
644  PRECONDITION(this->address().type().id() == ID_pointer);
645  }
646 
647  const exprt &state() const
648  {
649  return op0();
650  }
651 
653  {
654  return op0();
655  }
656 
657  const exprt &address() const
658  {
659  return op1();
660  }
661 
662  // helper
664  {
665  auto result = *this; // copy
666  result.state() = std::move(state);
667  return result;
668  }
669 };
670 
678 {
679  PRECONDITION(expr.id() == ID_state_cstrlen);
680  const state_cstrlen_exprt &ret =
681  static_cast<const state_cstrlen_exprt &>(expr);
682  validate_expr(ret);
683  return ret;
684 }
685 
688 {
689  PRECONDITION(expr.id() == ID_state_cstrlen);
690  state_cstrlen_exprt &ret = static_cast<state_cstrlen_exprt &>(expr);
691  validate_expr(ret);
692  return ret;
693 }
694 
696 {
697 public:
700  std::move(state),
701  ID_state_is_dynamic_object,
702  std::move(address))
703  {
704  PRECONDITION(this->state().type().id() == ID_state);
705  PRECONDITION(this->address().type().id() == ID_pointer);
706  }
707 
708  const exprt &state() const
709  {
710  return op0();
711  }
712 
714  {
715  return op0();
716  }
717 
718  const exprt &address() const
719  {
720  return op1();
721  }
722 
723  // helper
725  {
726  auto result = *this; // copy
727  result.state() = std::move(state);
728  return result;
729  }
730 };
731 
738 inline const state_is_dynamic_object_exprt &
740 {
741  PRECONDITION(expr.id() == ID_state_is_dynamic_object);
742  const state_is_dynamic_object_exprt &ret =
743  static_cast<const state_is_dynamic_object_exprt &>(expr);
744  validate_expr(ret);
745  return ret;
746 }
747 
751 {
752  PRECONDITION(expr.id() == ID_state_is_dynamic_object);
754  static_cast<state_is_dynamic_object_exprt &>(expr);
755  validate_expr(ret);
756  return ret;
757 }
758 
760 {
761 public:
763  : binary_exprt(
764  std::move(state),
765  ID_state_object_size,
766  std::move(address),
767  std::move(type))
768  {
769  PRECONDITION(this->state().type().id() == ID_state);
770  PRECONDITION(this->address().type().id() == ID_pointer);
771  }
772 
773  const exprt &state() const
774  {
775  return op0();
776  }
777 
779  {
780  return op0();
781  }
782 
783  const exprt &address() const
784  {
785  return op1();
786  }
787 
788  // helper
790  {
791  auto result = *this; // copy
792  result.state() = std::move(state);
793  return result;
794  }
795 };
796 
803 inline const state_object_size_exprt &
805 {
806  PRECONDITION(expr.id() == ID_state_object_size);
807  const state_object_size_exprt &ret =
808  static_cast<const state_object_size_exprt &>(expr);
809  validate_expr(ret);
810  return ret;
811 }
812 
815 {
816  PRECONDITION(expr.id() == ID_state_object_size);
817  state_object_size_exprt &ret = static_cast<state_object_size_exprt &>(expr);
818  validate_expr(ret);
819  return ret;
820 }
821 
823 {
824 public:
826  : ternary_exprt(
827  id,
828  std::move(state),
829  std::move(address),
830  std::move(size),
831  bool_typet())
832  {
833  PRECONDITION(this->state().type().id() == ID_state);
834  PRECONDITION(this->address().type().id() == ID_pointer);
835  }
836 
837  const exprt &state() const
838  {
839  return op0();
840  }
841 
843  {
844  return op0();
845  }
846 
847  const exprt &address() const
848  {
849  return op1();
850  }
851 
853  {
854  return op1();
855  }
856 
857  const exprt &size() const
858  {
859  return op2();
860  }
861 
863  {
864  return op2();
865  }
866 
867  // helper
869  {
870  auto result = *this; // copy
871  result.state() = std::move(state);
872  return result;
873  }
874 };
875 
882 inline const state_ok_exprt &to_state_ok_expr(const exprt &expr)
883 {
884  PRECONDITION(
885  expr.id() == ID_state_r_ok || expr.id() == ID_state_w_ok ||
886  expr.id() == ID_state_rw_ok);
887  const state_ok_exprt &ret = static_cast<const state_ok_exprt &>(expr);
888  validate_expr(ret);
889  return ret;
890 }
891 
894 {
895  PRECONDITION(
896  expr.id() == ID_state_r_ok || expr.id() == ID_state_w_ok ||
897  expr.id() == ID_state_rw_ok);
898  state_ok_exprt &ret = static_cast<state_ok_exprt &>(expr);
899  validate_expr(ret);
900  return ret;
901 }
902 
904 {
905 public:
907  : binary_exprt(
908  std::move(state),
909  ID_state_type_compatible,
910  std::move(address),
911  bool_typet())
912  {
913  PRECONDITION(this->state().type().id() == ID_state);
914  PRECONDITION(this->address().type().id() == ID_pointer);
915  }
916 
917  const exprt &state() const
918  {
919  return op0();
920  }
921 
923  {
924  return op0();
925  }
926 
927  const exprt &address() const
928  {
929  return op1();
930  }
931 
933  {
934  return op1();
935  }
936 
937  const typet &access_type() const
938  {
939  return to_pointer_type(address().type()).base_type();
940  }
941 
942  // helper
944  {
945  auto result = *this; // copy
946  result.state() = std::move(state);
947  return result;
948  }
949 };
950 
957 inline const state_type_compatible_exprt &
959 {
960  PRECONDITION(expr.id() == ID_state_type_compatible);
961  const state_type_compatible_exprt &ret =
962  static_cast<const state_type_compatible_exprt &>(expr);
963  validate_expr(ret);
964  return ret;
965 }
966 
969 {
970  PRECONDITION(expr.id() == ID_state_type_compatible);
972  static_cast<state_type_compatible_exprt &>(expr);
973  validate_expr(ret);
974  return ret;
975 }
976 
978 {
979 public:
981  : binary_exprt(
982  std::move(state),
983  ID_enter_scope_state,
984  std::move(address),
985  state_typet())
986  {
987  PRECONDITION(this->state().type().id() == ID_state);
988  PRECONDITION(this->address().type().id() == ID_pointer);
989  }
990 
991  const exprt &state() const
992  {
993  return op0();
994  }
995 
997  {
998  return op0();
999  }
1000 
1001  const exprt &address() const
1002  {
1003  return op1();
1004  }
1005 
1007  {
1008  return op1();
1009  }
1010 
1012  {
1013  return to_pointer_type(address().type()).base_type();
1014  }
1015 
1017  {
1018  PRECONDITION(address().id() == ID_object_address);
1020  }
1021 
1022 #if 0
1023  const exprt &size() const
1024  {
1025  return op2();
1026  }
1027 
1028  exprt &size()
1029  {
1030  return op2();
1031  }
1032 #endif
1033 };
1034 
1041 inline const enter_scope_state_exprt &
1043 {
1044  PRECONDITION(expr.id() == ID_enter_scope_state);
1045  const enter_scope_state_exprt &ret =
1046  static_cast<const enter_scope_state_exprt &>(expr);
1047  validate_expr(ret);
1048  return ret;
1049 }
1050 
1053 {
1054  PRECONDITION(expr.id() == ID_enter_scope_state);
1055  enter_scope_state_exprt &ret = static_cast<enter_scope_state_exprt &>(expr);
1056  validate_expr(ret);
1057  return ret;
1058 }
1059 
1061 {
1062 public:
1064  : binary_exprt(
1065  std::move(state),
1066  ID_exit_scope_state,
1067  std::move(address),
1068  state_typet())
1069  {
1070  PRECONDITION(this->state().type().id() == ID_state);
1071  PRECONDITION(this->address().type().id() == ID_pointer);
1072  }
1073 
1074  const exprt &state() const
1075  {
1076  return op0();
1077  }
1078 
1080  {
1081  return op0();
1082  }
1083 
1084  const exprt &address() const
1085  {
1086  return op1();
1087  }
1088 
1090  {
1091  return op1();
1092  }
1093 
1095  {
1096  PRECONDITION(address().id() == ID_object_address);
1098  }
1099 
1100 #if 0
1101  const exprt &size() const
1102  {
1103  return op2();
1104  }
1105 
1106  exprt &size()
1107  {
1108  return op2();
1109  }
1110 #endif
1111 };
1112 
1120 {
1121  PRECONDITION(expr.id() == ID_exit_scope_state);
1122  const exit_scope_state_exprt &ret =
1123  static_cast<const exit_scope_state_exprt &>(expr);
1124  validate_expr(ret);
1125  return ret;
1126 }
1127 
1130 {
1131  PRECONDITION(expr.id() == ID_exit_scope_state);
1132  exit_scope_state_exprt &ret = static_cast<exit_scope_state_exprt &>(expr);
1133  validate_expr(ret);
1134  return ret;
1135 }
1136 
1137 #endif // CPROVER_CPROVER_STATE_H
uint64_t u8
Definition: bytecode_info.h:58
void validate_expr(const shuffle_vector_exprt &value)
Definition: c_expr.h:82
allocate_exprt(exprt state, exprt size, pointer_typet type)
Definition: state.h:220
allocate_exprt with_state(exprt state) const
Definition: state.h:246
const exprt & state() const
Definition: state.h:230
const exprt & size() const
Definition: state.h:240
exprt & state()
Definition: state.h:235
exprt & state()
Definition: state.h:286
allocate_state_exprt(exprt state, exprt size)
Definition: state.h:271
const exprt & state() const
Definition: state.h:281
const exprt & size() const
Definition: state.h:291
A base class for binary expressions.
Definition: std_expr.h:638
exprt & op1()
Definition: expr.h:136
const exprt & op2() const =delete
exprt & op0()
Definition: expr.h:133
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:731
The Boolean type.
Definition: std_types.h:36
const exprt & address() const
Definition: state.h:434
exprt & state()
Definition: state.h:429
deallocate_state_exprt(exprt state, exprt address)
Definition: state.h:414
const exprt & state() const
Definition: state.h:424
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const exprt & address() const
Definition: state.h:1001
typet object_type() const
Definition: state.h:1011
const exprt & state() const
Definition: state.h:991
symbol_exprt symbol() const
Definition: state.h:1016
enter_scope_state_exprt(exprt state, exprt address)
Definition: state.h:980
const exprt & state() const
Definition: state.h:100
exprt & state()
Definition: state.h:105
evaluate_exprt(exprt state, exprt address)
Definition: state.h:92
evaluate_exprt with_state(exprt state) const
Definition: state.h:116
const exprt & address() const
Definition: state.h:110
evaluate_exprt(exprt state, exprt address, typet type)
Definition: state.h:80
exit_scope_state_exprt(exprt state, exprt address)
Definition: state.h:1063
const exprt & state() const
Definition: state.h:1074
exprt & address()
Definition: state.h:1089
symbol_exprt symbol() const
Definition: state.h:1094
const exprt & address() const
Definition: state.h:1084
Base class for all expressions.
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:84
exprt & state()
Definition: state.h:47
initial_state_exprt(exprt state)
Definition: state.h:36
const exprt & state() const
Definition: state.h:42
const irep_idt & id() const
Definition: irep.h:388
A type for mathematical functions (do not confuse with functions/methods in code)
symbol_exprt object_expr() const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
const exprt & address() const
Definition: state.h:336
const exprt & state() const
Definition: state.h:326
const exprt & size() const
Definition: state.h:341
exprt & state()
Definition: state.h:331
reallocate_exprt(exprt state, exprt address, exprt size, pointer_typet type)
Definition: state.h:315
const exprt & size() const
Definition: state.h:390
const exprt & address() const
Definition: state.h:385
reallocate_state_exprt(exprt state, exprt address, exprt size)
Definition: state.h:364
exprt & state()
Definition: state.h:380
const exprt & state() const
Definition: state.h:375
const exprt & address() const
Definition: state.h:657
const exprt & state() const
Definition: state.h:647
state_cstrlen_exprt(exprt state, exprt address, typet type)
Definition: state.h:636
exprt & state()
Definition: state.h:652
state_cstrlen_exprt with_state(exprt state) const
Definition: state.h:663
const exprt & address() const
Definition: state.h:595
const exprt & state() const
Definition: state.h:585
state_is_cstring_exprt(exprt state, exprt address)
Definition: state.h:575
exprt & state()
Definition: state.h:590
state_is_cstring_exprt with_state(exprt state) const
Definition: state.h:601
const exprt & address() const
Definition: state.h:718
state_is_dynamic_object_exprt(exprt state, exprt address)
Definition: state.h:698
state_is_dynamic_object_exprt with_state(exprt state) const
Definition: state.h:724
const exprt & state() const
Definition: state.h:708
state_live_object_exprt(exprt state, exprt address)
Definition: state.h:458
const exprt & state() const
Definition: state.h:468
const exprt & address() const
Definition: state.h:478
state_live_object_exprt with_state(exprt state) const
Definition: state.h:484
const exprt & address() const
Definition: state.h:783
state_object_size_exprt with_state(exprt state) const
Definition: state.h:789
state_object_size_exprt(exprt state, exprt address, typet type)
Definition: state.h:762
const exprt & state() const
Definition: state.h:773
exprt & state()
Definition: state.h:842
const exprt & address() const
Definition: state.h:847
state_ok_exprt with_state(exprt state) const
Definition: state.h:868
const exprt & state() const
Definition: state.h:837
const exprt & size() const
Definition: state.h:857
exprt & address()
Definition: state.h:852
exprt & size()
Definition: state.h:862
state_ok_exprt(irep_idt id, exprt state, exprt address, exprt size)
Definition: state.h:825
const exprt & address() const
Definition: state.h:927
state_type_compatible_exprt with_state(exprt state) const
Definition: state.h:943
const exprt & state() const
Definition: state.h:917
state_type_compatible_exprt(exprt state, exprt address)
Definition: state.h:906
const typet & access_type() const
Definition: state.h:937
state_typet()
Definition: state.h:18
const exprt & state() const
Definition: state.h:530
const exprt & address() const
Definition: state.h:540
state_writeable_object_exprt(exprt state, exprt address)
Definition: state.h:520
Expression to hold a symbol (variable)
Definition: std_expr.h:131
An expression with three operands.
Definition: std_expr.h:67
exprt & op1()
Definition: expr.h:136
exprt & op2()
Definition: expr.h:139
exprt & op0()
Definition: expr.h:133
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:585
update_state_exprt with_state(exprt state) const
Definition: state.h:186
const exprt & state() const
Definition: state.h:165
exprt & state()
Definition: state.h:170
update_state_exprt(exprt state, exprt address, exprt new_value)
Definition: state.h:150
const exprt & new_value() const
Definition: state.h:180
const exprt & address() const
Definition: state.h:175
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:643
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const state_type_compatible_exprt & to_state_type_compatible_expr(const exprt &expr)
Cast an exprt to a state_type_compatible_exprt.
Definition: state.h:958
const deallocate_state_exprt & to_deallocate_state_expr(const exprt &expr)
Cast an exprt to a deallocate_state_exprt.
Definition: state.h:446
const state_cstrlen_exprt & to_state_cstrlen_expr(const exprt &expr)
Cast an exprt to a state_cstrlen_exprt.
Definition: state.h:677
const reallocate_exprt & to_reallocate_expr(const exprt &expr)
Cast an exprt to a reallocate_exprt.
Definition: state.h:353
const update_state_exprt & to_update_state_expr(const exprt &expr)
Cast an exprt to a update_state_exprt.
Definition: state.h:200
static symbol_exprt state_expr()
Definition: state.h:28
const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr(const exprt &expr)
Cast an exprt to a state_is_dynamic_object_exprt.
Definition: state.h:739
const evaluate_exprt & to_evaluate_expr(const exprt &expr)
Cast an exprt to a evaluate_exprt.
Definition: state.h:130
const state_object_size_exprt & to_state_object_size_expr(const exprt &expr)
Cast an exprt to a state_object_size_exprt.
Definition: state.h:804
const initial_state_exprt & to_initial_state_expr(const exprt &expr)
Cast an exprt to a initial_state_exprt.
Definition: state.h:59
const allocate_exprt & to_allocate_expr(const exprt &expr)
Cast an exprt to a allocate_exprt.
Definition: state.h:260
const state_live_object_exprt & to_state_live_object_expr(const exprt &expr)
Cast an exprt to a state_live_object_exprt.
Definition: state.h:499
const reallocate_state_exprt & to_reallocate_state_expr(const exprt &expr)
Cast an exprt to a reallocate_state_exprt.
Definition: state.h:402
const state_writeable_object_exprt & to_state_writeable_object_expr(const exprt &expr)
Cast an exprt to a state_writeable_object_exprt.
Definition: state.h:553
const state_is_cstring_exprt & to_state_is_cstring_expr(const exprt &expr)
Cast an exprt to a state_is_cstring_exprt.
Definition: state.h:615
const exit_scope_state_exprt & to_exit_scope_state_expr(const exprt &expr)
Cast an exprt to a exit_scope_state_exprt.
Definition: state.h:1119
const enter_scope_state_exprt & to_enter_scope_state_expr(const exprt &expr)
Cast an exprt to a enter_scope_state_exprt.
Definition: state.h:1042
const state_ok_exprt & to_state_ok_expr(const exprt &expr)
Cast an exprt to a state_ok_exprt.
Definition: state.h:882
const allocate_state_exprt & to_allocate_state_expr(const exprt &expr)
Cast an exprt to a allocate_state_exprt.
Definition: state.h:303
static mathematical_function_typet state_predicate_type()
Definition: state.h:23