cprover
pointer_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: API to expression classes for Pointers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_UTIL_POINTER_EXPR_H
10 #define CPROVER_UTIL_POINTER_EXPR_H
11 
14 
15 #include "bitvector_types.h"
16 #include "std_expr.h"
17 
18 class namespacet;
19 
24 {
25 public:
26  pointer_typet(typet _base_type, std::size_t width)
27  : bitvector_typet(ID_pointer, width)
28  {
29  subtype().swap(_base_type);
30  }
31 
35  const typet &base_type() const
36  {
37  return subtype();
38  }
39 
44  {
45  return subtype();
46  }
47 
49  {
50  return signedbv_typet(get_width());
51  }
52 
53  static void check(
54  const typet &type,
56  {
58  DATA_CHECK(vm, !type.get(ID_width).empty(), "pointer must have width");
59  }
60 };
61 
65 template <>
66 inline bool can_cast_type<pointer_typet>(const typet &type)
67 {
68  return type.id() == ID_pointer;
69 }
70 
79 inline const pointer_typet &to_pointer_type(const typet &type)
80 {
83  return static_cast<const pointer_typet &>(type);
84 }
85 
88 {
91  return static_cast<pointer_typet &>(type);
92 }
93 
96 inline bool is_void_pointer(const typet &type)
97 {
98  return type.id() == ID_pointer &&
99  to_pointer_type(type).base_type().id() == ID_empty;
100 }
101 
107 {
108 public:
109  reference_typet(typet _subtype, std::size_t _width)
110  : pointer_typet(std::move(_subtype), _width)
111  {
112  set(ID_C_reference, true);
113  }
114 
115  static void check(
116  const typet &type,
118  {
119  PRECONDITION(type.id() == ID_pointer);
120  DATA_CHECK(
121  vm, type.get_sub().size() == 1, "reference must have one type parameter");
123  static_cast<const reference_typet &>(type);
124  DATA_CHECK(
125  vm, !reference_type.get(ID_width).empty(), "reference must have width");
126  DATA_CHECK(
127  vm, reference_type.get_width() > 0, "reference must have non-zero width");
128  }
129 };
130 
134 template <>
135 inline bool can_cast_type<reference_typet>(const typet &type)
136 {
137  return can_cast_type<pointer_typet>(type) && type.get_bool(ID_C_reference);
138 }
139 
148 inline const reference_typet &to_reference_type(const typet &type)
149 {
151  return static_cast<const reference_typet &>(type);
152 }
153 
156 {
158  return static_cast<reference_typet &>(type);
159 }
160 
161 bool is_reference(const typet &type);
162 
163 bool is_rvalue_reference(const typet &type);
164 
167 {
168 public:
170  : binary_exprt(
171  exprt(ID_unknown),
172  ID_object_descriptor,
173  exprt(ID_unknown),
174  typet())
175  {
176  }
177 
178  explicit object_descriptor_exprt(exprt _object)
179  : binary_exprt(
180  std::move(_object),
181  ID_object_descriptor,
182  exprt(ID_unknown),
183  typet())
184  {
185  }
186 
191  void build(const exprt &expr, const namespacet &ns);
192 
194  {
195  return op0();
196  }
197 
198  const exprt &object() const
199  {
200  return op0();
201  }
202 
203  static const exprt &root_object(const exprt &expr);
204  const exprt &root_object() const
205  {
206  return root_object(object());
207  }
208 
210  {
211  return op1();
212  }
213 
214  const exprt &offset() const
215  {
216  return op1();
217  }
218 };
219 
220 template <>
222 {
223  return base.id() == ID_object_descriptor;
224 }
225 
226 inline void validate_expr(const object_descriptor_exprt &value)
227 {
228  validate_operands(value, 2, "Object descriptor must have two operands");
229 }
230 
237 inline const object_descriptor_exprt &
239 {
240  PRECONDITION(expr.id() == ID_object_descriptor);
241  const object_descriptor_exprt &ret =
242  static_cast<const object_descriptor_exprt &>(expr);
243  validate_expr(ret);
244  return ret;
245 }
246 
249 {
250  PRECONDITION(expr.id() == ID_object_descriptor);
251  object_descriptor_exprt &ret = static_cast<object_descriptor_exprt &>(expr);
252  validate_expr(ret);
253  return ret;
254 }
255 
258 {
259 public:
261  : binary_exprt(
262  exprt(ID_unknown),
263  ID_dynamic_object,
264  exprt(ID_unknown),
265  std::move(type))
266  {
267  }
268 
269  void set_instance(unsigned int instance);
270 
271  unsigned int get_instance() const;
272 
274  {
275  return op1();
276  }
277 
278  const exprt &valid() const
279  {
280  return op1();
281  }
282 };
283 
284 template <>
286 {
287  return base.id() == ID_dynamic_object;
288 }
289 
290 inline void validate_expr(const dynamic_object_exprt &value)
291 {
292  validate_operands(value, 2, "Dynamic object must have two operands");
293 }
294 
302 {
303  PRECONDITION(expr.id() == ID_dynamic_object);
304  const dynamic_object_exprt &ret =
305  static_cast<const dynamic_object_exprt &>(expr);
306  validate_expr(ret);
307  return ret;
308 }
309 
312 {
313  PRECONDITION(expr.id() == ID_dynamic_object);
314  dynamic_object_exprt &ret = static_cast<dynamic_object_exprt &>(expr);
315  validate_expr(ret);
316  return ret;
317 }
318 
321 {
322 public:
324  : unary_predicate_exprt(ID_is_dynamic_object, op)
325  {
326  }
327 };
328 
329 template <>
331 {
332  return base.id() == ID_is_invalid_pointer;
333 }
334 
335 inline void validate_expr(const is_dynamic_object_exprt &value)
336 {
337  validate_operands(value, 1, "is_dynamic_object must have one operand");
338 }
339 
340 inline const is_dynamic_object_exprt &
342 {
343  PRECONDITION(expr.id() == ID_is_dynamic_object);
345  expr.operands().size() == 1, "is_dynamic_object must have one operand");
346  return static_cast<const is_dynamic_object_exprt &>(expr);
347 }
348 
352 {
353  PRECONDITION(expr.id() == ID_is_dynamic_object);
355  expr.operands().size() == 1, "is_dynamic_object must have one operand");
356  return static_cast<is_dynamic_object_exprt &>(expr);
357 }
358 
361 {
362 public:
363  explicit address_of_exprt(const exprt &op);
364 
366  : unary_exprt(ID_address_of, std::move(op), std::move(_type))
367  {
368  }
369 
371  {
372  return op0();
373  }
374 
375  const exprt &object() const
376  {
377  return op0();
378  }
379 };
380 
381 template <>
382 inline bool can_cast_expr<address_of_exprt>(const exprt &base)
383 {
384  return base.id() == ID_address_of;
385 }
386 
387 inline void validate_expr(const address_of_exprt &value)
388 {
389  validate_operands(value, 1, "Address of must have one operand");
390 }
391 
398 inline const address_of_exprt &to_address_of_expr(const exprt &expr)
399 {
400  PRECONDITION(expr.id() == ID_address_of);
401  const address_of_exprt &ret = static_cast<const address_of_exprt &>(expr);
402  validate_expr(ret);
403  return ret;
404 }
405 
408 {
409  PRECONDITION(expr.id() == ID_address_of);
410  address_of_exprt &ret = static_cast<address_of_exprt &>(expr);
411  validate_expr(ret);
412  return ret;
413 }
414 
417 {
418 public:
419  explicit object_address_exprt(const symbol_exprt &);
420 
422  {
423  return get(ID_identifier);
424  }
425 
426  const pointer_typet &type() const
427  {
428  return static_cast<const pointer_typet &>(exprt::type());
429  }
430 
432  {
433  return static_cast<pointer_typet &>(exprt::type());
434  }
435 
437  const typet &object_type() const
438  {
439  return type().base_type();
440  }
441 
442  symbol_exprt object_expr() const;
443 };
444 
445 template <>
447 {
448  return base.id() == ID_object_address;
449 }
450 
451 inline void validate_expr(const object_address_exprt &value)
452 {
453  validate_operands(value, 1, "object_address must have one operand");
454 }
455 
463 {
464  PRECONDITION(expr.id() == ID_object_address);
465  const object_address_exprt &ret =
466  static_cast<const object_address_exprt &>(expr);
467  validate_expr(ret);
468  return ret;
469 }
470 
473 {
474  PRECONDITION(expr.id() == ID_object_address);
475  object_address_exprt &ret = static_cast<object_address_exprt &>(expr);
476  validate_expr(ret);
477  return ret;
478 }
479 
483 {
484 public:
488  exprt base,
489  const irep_idt &component_name,
491 
493  {
494  return op0();
495  }
496 
497  const exprt &base() const
498  {
499  return op0();
500  }
501 
502  const pointer_typet &type() const
503  {
504  return static_cast<const pointer_typet &>(exprt::type());
505  }
506 
508  {
509  return static_cast<pointer_typet &>(exprt::type());
510  }
511 
513  const typet &field_type() const
514  {
515  return type().base_type();
516  }
517 
518  const typet &compound_type() const
519  {
520  return to_pointer_type(base().type()).base_type();
521  }
522 
523  const irep_idt &component_name() const
524  {
525  return get(ID_component_name);
526  }
527 };
528 
529 template <>
531 {
532  return expr.id() == ID_field_address;
533 }
534 
535 inline void validate_expr(const field_address_exprt &value)
536 {
537  validate_operands(value, 1, "field_address must have one operand");
538 }
539 
547 {
548  PRECONDITION(expr.id() == ID_field_address);
549  const field_address_exprt &ret =
550  static_cast<const field_address_exprt &>(expr);
551  validate_expr(ret);
552  return ret;
553 }
554 
557 {
558  PRECONDITION(expr.id() == ID_field_address);
559  field_address_exprt &ret = static_cast<field_address_exprt &>(expr);
560  validate_expr(ret);
561  return ret;
562 }
563 
567 {
568 public:
573 
574  const pointer_typet &type() const
575  {
576  return static_cast<const pointer_typet &>(exprt::type());
577  }
578 
580  {
581  return static_cast<pointer_typet &>(exprt::type());
582  }
583 
585  const typet &element_type() const
586  {
587  return type().base_type();
588  }
589 
591  {
592  return op0();
593  }
594 
595  const exprt &base() const
596  {
597  return op0();
598  }
599 
601  {
602  return op1();
603  }
604 
605  const exprt &index() const
606  {
607  return op1();
608  }
609 };
610 
611 template <>
613 {
614  return expr.id() == ID_element_address;
615 }
616 
617 inline void validate_expr(const element_address_exprt &value)
618 {
619  validate_operands(value, 2, "element_address must have two operands");
620 }
621 
629 {
630  PRECONDITION(expr.id() == ID_element_address);
631  const element_address_exprt &ret =
632  static_cast<const element_address_exprt &>(expr);
633  validate_expr(ret);
634  return ret;
635 }
636 
639 {
640  PRECONDITION(expr.id() == ID_element_address);
641  element_address_exprt &ret = static_cast<element_address_exprt &>(expr);
642  validate_expr(ret);
643  return ret;
644 }
645 
648 {
649 public:
650  // The given operand must have pointer type.
651  explicit dereference_exprt(const exprt &op)
652  : unary_exprt(ID_dereference, op, to_pointer_type(op.type()).base_type())
653  {
654  }
655 
657  : unary_exprt(ID_dereference, std::move(op), std::move(type))
658  {
659  }
660 
662  {
663  return op0();
664  }
665 
666  const exprt &pointer() const
667  {
668  return op0();
669  }
670 
671  static void check(
672  const exprt &expr,
674  {
675  DATA_CHECK(
676  vm,
677  expr.operands().size() == 1,
678  "dereference expression must have one operand");
679  }
680 
681  static void validate(
682  const exprt &expr,
683  const namespacet &ns,
685 };
686 
687 template <>
688 inline bool can_cast_expr<dereference_exprt>(const exprt &base)
689 {
690  return base.id() == ID_dereference;
691 }
692 
693 inline void validate_expr(const dereference_exprt &value)
694 {
695  validate_operands(value, 1, "Dereference must have one operand");
696 }
697 
704 inline const dereference_exprt &to_dereference_expr(const exprt &expr)
705 {
706  PRECONDITION(expr.id() == ID_dereference);
707  const dereference_exprt &ret = static_cast<const dereference_exprt &>(expr);
708  validate_expr(ret);
709  return ret;
710 }
711 
714 {
715  PRECONDITION(expr.id() == ID_dereference);
716  dereference_exprt &ret = static_cast<dereference_exprt &>(expr);
717  validate_expr(ret);
718  return ret;
719 }
720 
723 {
724 public:
726  : constant_exprt(ID_NULL, std::move(type))
727  {
728  }
729 };
730 
734 {
735 public:
737  : binary_predicate_exprt(std::move(pointer), id, std::move(size))
738  {
739  }
740 
741  const exprt &pointer() const
742  {
743  return op0();
744  }
745 
746  const exprt &size() const
747  {
748  return op1();
749  }
750 };
751 
752 inline const r_or_w_ok_exprt &to_r_or_w_ok_expr(const exprt &expr)
753 {
754  PRECONDITION(
755  expr.id() == ID_r_ok || expr.id() == ID_w_ok || expr.id() == ID_rw_ok);
756  auto &ret = static_cast<const r_or_w_ok_exprt &>(expr);
757  validate_expr(ret);
758  return ret;
759 }
760 
763 {
764 public:
766  : r_or_w_ok_exprt(ID_r_ok, std::move(pointer), std::move(size))
767  {
768  }
769 };
770 
771 inline const r_ok_exprt &to_r_ok_expr(const exprt &expr)
772 {
773  PRECONDITION(expr.id() == ID_r_ok);
774  const r_ok_exprt &ret = static_cast<const r_ok_exprt &>(expr);
775  validate_expr(ret);
776  return ret;
777 }
778 
781 {
782 public:
784  : r_or_w_ok_exprt(ID_w_ok, std::move(pointer), std::move(size))
785  {
786  }
787 };
788 
789 inline const w_ok_exprt &to_w_ok_expr(const exprt &expr)
790 {
791  PRECONDITION(expr.id() == ID_w_ok);
792  const w_ok_exprt &ret = static_cast<const w_ok_exprt &>(expr);
793  validate_expr(ret);
794  return ret;
795 }
796 
797 #endif // CPROVER_UTIL_POINTER_EXPR_H
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
Pre-defined bitvector types.
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:258
Operator to return the address of an object.
Definition: pointer_expr.h:361
address_of_exprt(const exprt &op)
const exprt & object() const
Definition: pointer_expr.h:375
address_of_exprt(exprt op, pointer_typet _type)
Definition: pointer_expr.h:365
exprt & object()
Definition: pointer_expr.h:370
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
Base class of fixed-width bit-vector types.
Definition: std_types.h:853
std::size_t get_width() const
Definition: std_types.h:864
A constant literal expression.
Definition: std_expr.h:2807
Operator to dereference a pointer.
Definition: pointer_expr.h:648
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:671
dereference_exprt(const exprt &op)
Definition: pointer_expr.h:651
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the dereference expression has the right number of operands, refers to something with a po...
const exprt & pointer() const
Definition: pointer_expr.h:666
dereference_exprt(exprt op, typet type)
Definition: pointer_expr.h:656
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Representation of heap-allocated objects.
Definition: pointer_expr.h:258
unsigned int get_instance() const
const exprt & valid() const
Definition: pointer_expr.h:278
void set_instance(unsigned int instance)
dynamic_object_exprt(typet type)
Definition: pointer_expr.h:260
Operator to return the address of an array element relative to a base address.
Definition: pointer_expr.h:567
const exprt & index() const
Definition: pointer_expr.h:605
const exprt & base() const
Definition: pointer_expr.h:595
const pointer_typet & type() const
Definition: pointer_expr.h:574
element_address_exprt(exprt base, exprt index)
constructor for element addresses.
const typet & element_type() const
returns the type of the array element whose address is represented
Definition: pointer_expr.h:585
pointer_typet & type()
Definition: pointer_expr.h:579
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Operator to return the address of a field relative to a base address.
Definition: pointer_expr.h:483
pointer_typet & type()
Definition: pointer_expr.h:507
const typet & compound_type() const
Definition: pointer_expr.h:518
const typet & field_type() const
returns the type of the field whose address is represented
Definition: pointer_expr.h:513
const exprt & base() const
Definition: pointer_expr.h:497
const pointer_typet & type() const
Definition: pointer_expr.h:502
const irep_idt & component_name() const
Definition: pointer_expr.h:523
field_address_exprt(exprt base, const irep_idt &component_name, pointer_typet type)
constructor for field addresses.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
subt & get_sub()
Definition: irep.h:456
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:321
is_dynamic_object_exprt(const exprt &op)
Definition: pointer_expr.h:323
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The null pointer constant.
Definition: pointer_expr.h:723
null_pointer_exprt(pointer_typet type)
Definition: pointer_expr.h:725
An expression without operands.
Definition: std_expr.h:22
Operator to return the address of an object.
Definition: pointer_expr.h:417
symbol_exprt object_expr() const
const typet & object_type() const
returns the type of the object whose address is represented
Definition: pointer_expr.h:437
pointer_typet & type()
Definition: pointer_expr.h:431
const pointer_typet & type() const
Definition: pointer_expr.h:426
irep_idt object_identifier() const
Definition: pointer_expr.h:421
object_address_exprt(const symbol_exprt &)
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:167
object_descriptor_exprt(exprt _object)
Definition: pointer_expr.h:178
const exprt & object() const
Definition: pointer_expr.h:198
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
const exprt & root_object() const
Definition: pointer_expr.h:204
const exprt & offset() const
Definition: pointer_expr.h:214
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:53
signedbv_typet difference_type() const
Definition: pointer_expr.h:48
typet & base_type()
The type of the data what we point to.
Definition: pointer_expr.h:43
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
pointer_typet(typet _base_type, std::size_t width)
Definition: pointer_expr.h:26
A predicate that indicates that an address range is ok to read.
Definition: pointer_expr.h:763
r_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:765
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:734
const exprt & size() const
Definition: pointer_expr.h:746
r_or_w_ok_exprt(irep_idt id, exprt pointer, exprt size)
Definition: pointer_expr.h:736
const exprt & pointer() const
Definition: pointer_expr.h:741
The reference type.
Definition: pointer_expr.h:107
reference_typet(typet _subtype, std::size_t _width)
Definition: pointer_expr.h:109
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: pointer_expr.h:115
Fixed-width bit-vector with two's complement interpretation.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
static void check(const typet &type, const validation_modet vm=validation_modet::INVARIANT)
Definition: type.h:168
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition: std_expr.h:495
A predicate that indicates that an address range is ok to write.
Definition: pointer_expr.h:781
w_ok_exprt(exprt pointer, exprt size)
Definition: pointer_expr.h:783
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition: expr_cast.h:250
void validate_expr(const object_descriptor_exprt &value)
Definition: pointer_expr.h:226
bool can_cast_type< reference_typet >(const typet &type)
Check whether a reference to a typet is a reference_typet.
Definition: pointer_expr.h:135
bool can_cast_expr< field_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:530
bool is_void_pointer(const typet &type)
This method tests, if the given typet is a pointer of type void.
Definition: pointer_expr.h:96
const r_or_w_ok_exprt & to_r_or_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:752
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:66
const w_ok_exprt & to_w_ok_expr(const exprt &expr)
Definition: pointer_expr.h:789
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:137
bool can_cast_expr< dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:285
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
Definition: pointer_expr.h:546
bool can_cast_expr< dereference_exprt >(const exprt &base)
Definition: pointer_expr.h:688
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:704
bool is_rvalue_reference(const typet &type)
Returns if the type is an R value reference.
Definition: std_types.cpp:144
bool can_cast_expr< is_dynamic_object_exprt >(const exprt &base)
Definition: pointer_expr.h:330
bool can_cast_expr< object_address_exprt >(const exprt &base)
Definition: pointer_expr.h:446
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
bool can_cast_expr< address_of_exprt >(const exprt &base)
Definition: pointer_expr.h:382
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:148
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: pointer_expr.h:238
const is_dynamic_object_exprt & to_is_dynamic_object_expr(const exprt &expr)
Definition: pointer_expr.h:341
bool can_cast_expr< element_address_exprt >(const exprt &expr)
Definition: pointer_expr.h:612
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
Definition: pointer_expr.h:462
bool can_cast_expr< object_descriptor_exprt >(const exprt &base)
Definition: pointer_expr.h:221
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
Definition: pointer_expr.h:301
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const r_ok_exprt & to_r_ok_expr(const exprt &expr)
Definition: pointer_expr.h:771
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
Definition: pointer_expr.h:628
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet