cprover
Loading...
Searching...
No Matches
bitvector_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: API to expression classes for bitvectors
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
10#define CPROVER_UTIL_BITVECTOR_EXPR_H
11
14
15#include "std_expr.h"
16
19{
20public:
22 : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
23 {
25 }
26
32
33 std::size_t get_bits_per_byte() const
34 {
36 }
37
42};
43
44template <>
45inline bool can_cast_expr<bswap_exprt>(const exprt &base)
46{
47 return base.id() == ID_bswap;
48}
49
50inline void validate_expr(const bswap_exprt &value)
51{
52 validate_operands(value, 1, "bswap must have one operand");
54 value.op().type() == value.type(), "bswap type must match operand type");
55}
56
63inline const bswap_exprt &to_bswap_expr(const exprt &expr)
64{
65 PRECONDITION(expr.id() == ID_bswap);
66 const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
68 return ret;
69}
70
73{
74 PRECONDITION(expr.id() == ID_bswap);
75 bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
77 return ret;
78}
79
82{
83public:
85 {
86 }
87};
88
89template <>
90inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
91{
92 return base.id() == ID_bitnot;
93}
94
95inline void validate_expr(const bitnot_exprt &value)
96{
97 validate_operands(value, 1, "Bit-wise not must have one operand");
98}
99
106inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
107{
108 PRECONDITION(expr.id() == ID_bitnot);
109 const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
111 return ret;
112}
113
116{
117 PRECONDITION(expr.id() == ID_bitnot);
118 bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
120 return ret;
121}
122
125{
126public:
129 {
130 }
131};
132
133template <>
134inline bool can_cast_expr<bitor_exprt>(const exprt &base)
135{
136 return base.id() == ID_bitor;
137}
138
145inline const bitor_exprt &to_bitor_expr(const exprt &expr)
146{
147 PRECONDITION(expr.id() == ID_bitor);
148 return static_cast<const bitor_exprt &>(expr);
149}
150
153{
154 PRECONDITION(expr.id() == ID_bitor);
155 return static_cast<bitor_exprt &>(expr);
156}
157
160{
161public:
163 : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
164 {
165 }
166};
167
168template <>
169inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
170{
171 return base.id() == ID_bitxor;
172}
173
180inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
181{
182 PRECONDITION(expr.id() == ID_bitxor);
183 return static_cast<const bitxor_exprt &>(expr);
184}
185
188{
189 PRECONDITION(expr.id() == ID_bitxor);
190 return static_cast<bitxor_exprt &>(expr);
191}
192
195{
196public:
199 {
200 }
201};
202
203template <>
204inline bool can_cast_expr<bitand_exprt>(const exprt &base)
205{
206 return base.id() == ID_bitand;
207}
208
215inline const bitand_exprt &to_bitand_expr(const exprt &expr)
216{
217 PRECONDITION(expr.id() == ID_bitand);
218 return static_cast<const bitand_exprt &>(expr);
219}
220
223{
224 PRECONDITION(expr.id() == ID_bitand);
225 return static_cast<bitand_exprt &>(expr);
226}
227
230{
231public:
233 : binary_exprt(std::move(_src), _id, std::move(_distance))
234 {
235 }
236
237 shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
238
240 {
241 return op0();
242 }
243
244 const exprt &op() const
245 {
246 return op0();
247 }
248
250 {
251 return op1();
252 }
253
254 const exprt &distance() const
255 {
256 return op1();
257 }
258};
259
260template <>
261inline bool can_cast_expr<shift_exprt>(const exprt &base)
262{
263 return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
264 base.id() == ID_ror || base.id() == ID_rol;
265}
266
267inline void validate_expr(const shift_exprt &value)
268{
269 validate_operands(value, 2, "Shifts must have two operands");
270}
271
278inline const shift_exprt &to_shift_expr(const exprt &expr)
279{
280 const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
282 return ret;
283}
284
287{
288 shift_exprt &ret = static_cast<shift_exprt &>(expr);
290 return ret;
291}
292
294class shl_exprt : public shift_exprt
295{
296public:
298 : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
299 {
300 }
301
302 shl_exprt(exprt _src, const std::size_t _distance)
304 {
305 }
306};
307
314inline const shl_exprt &to_shl_expr(const exprt &expr)
315{
316 PRECONDITION(expr.id() == ID_shl);
317 const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
319 return ret;
320}
321
324{
325 PRECONDITION(expr.id() == ID_shl);
326 shl_exprt &ret = static_cast<shl_exprt &>(expr);
328 return ret;
329}
330
333{
334public:
339
340 ashr_exprt(exprt _src, const std::size_t _distance)
342 {
343 }
344};
345
348{
349public:
354
355 lshr_exprt(exprt _src, const std::size_t _distance)
356 : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
357 {
358 }
359};
360
363{
364public:
370
371 extractbit_exprt(exprt _src, const std::size_t _index);
372
374 {
375 return op0();
376 }
377
379 {
380 return op1();
381 }
382
383 const exprt &src() const
384 {
385 return op0();
386 }
387
388 const exprt &index() const
389 {
390 return op1();
391 }
392};
393
394template <>
396{
397 return base.id() == ID_extractbit;
398}
399
400inline void validate_expr(const extractbit_exprt &value)
401{
402 validate_operands(value, 2, "Extract bit must have two operands");
403}
404
411inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
412{
413 PRECONDITION(expr.id() == ID_extractbit);
414 const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
416 return ret;
417}
418
421{
422 PRECONDITION(expr.id() == ID_extractbit);
423 extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
425 return ret;
426}
427
430{
431public:
440 std::move(_type),
441 {std::move(_src), std::move(_upper), std::move(_lower)})
442 {
443 }
444
446 exprt _src,
447 const std::size_t _upper,
448 const std::size_t _lower,
449 typet _type);
450
452 {
453 return op0();
454 }
455
457 {
458 return op1();
459 }
460
462 {
463 return op2();
464 }
465
466 const exprt &src() const
467 {
468 return op0();
469 }
470
471 const exprt &upper() const
472 {
473 return op1();
474 }
475
476 const exprt &lower() const
477 {
478 return op2();
479 }
480};
481
482template <>
484{
485 return base.id() == ID_extractbits;
486}
487
488inline void validate_expr(const extractbits_exprt &value)
489{
490 validate_operands(value, 3, "Extract bits must have three operands");
491}
492
500{
501 PRECONDITION(expr.id() == ID_extractbits);
502 const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
504 return ret;
505}
506
509{
510 PRECONDITION(expr.id() == ID_extractbits);
511 extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
513 return ret;
514}
515
518{
519public:
521 : binary_exprt(
522 std::move(_times),
524 std::move(_src),
525 std::move(_type))
526 {
527 }
528
530 {
531 return static_cast<constant_exprt &>(op0());
532 }
533
534 const constant_exprt &times() const
535 {
536 return static_cast<const constant_exprt &>(op0());
537 }
538
540 {
541 return op1();
542 }
543
544 const exprt &op() const
545 {
546 return op1();
547 }
548};
549
550template <>
552{
553 return base.id() == ID_replication;
554}
555
556inline void validate_expr(const replication_exprt &value)
557{
558 validate_operands(value, 2, "Bit-wise replication must have two operands");
559}
560
568{
569 PRECONDITION(expr.id() == ID_replication);
570 const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
572 return ret;
573}
574
577{
578 PRECONDITION(expr.id() == ID_replication);
579 replication_exprt &ret = static_cast<replication_exprt &>(expr);
581 return ret;
582}
583
590{
591public:
596
600 {std::move(_op0), std::move(_op1)},
601 std::move(_type))
602 {
603 }
604};
605
606template <>
608{
609 return base.id() == ID_concatenation;
610}
611
619{
621 return static_cast<const concatenation_exprt &>(expr);
622}
623
626{
628 return static_cast<concatenation_exprt &>(expr);
629}
630
633{
634public:
636 : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
637 {
638 }
639
640 explicit popcount_exprt(const exprt &_op)
642 {
643 }
644
647 exprt lower() const;
648};
649
650template <>
651inline bool can_cast_expr<popcount_exprt>(const exprt &base)
652{
653 return base.id() == ID_popcount;
654}
655
656inline void validate_expr(const popcount_exprt &value)
657{
658 validate_operands(value, 1, "popcount must have one operand");
659}
660
667inline const popcount_exprt &to_popcount_expr(const exprt &expr)
668{
669 PRECONDITION(expr.id() == ID_popcount);
670 const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
672 return ret;
673}
674
677{
678 PRECONDITION(expr.id() == ID_popcount);
679 popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
681 return ret;
682}
683
687{
688public:
691 std::move(_lhs),
692 "overflow-" + id2string(kind),
693 std::move(_rhs))
694 {
695 }
696
697 static void check(
698 const exprt &expr,
700 {
701 binary_exprt::check(expr, vm);
702
703 if(expr.id() != ID_overflow_shl)
704 {
707 vm,
708 binary_expr.lhs().type() == binary_expr.rhs().type(),
709 "operand types must match");
710 }
711 }
712
713 static void validate(
714 const exprt &expr,
715 const namespacet &,
717 {
718 check(expr, vm);
719 }
720};
721
722template <>
724{
725 return base.id() == ID_overflow_plus || base.id() == ID_overflow_mult ||
726 base.id() == ID_overflow_minus || base.id() == ID_overflow_shl;
727}
728
729inline void validate_expr(const binary_overflow_exprt &value)
730{
732 value, 2, "binary overflow expression must have two operands");
733}
734
742{
744 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
745 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
747 static_cast<const binary_overflow_exprt &>(expr);
749 return ret;
750}
751
754{
756 expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
757 expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
758 binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
760 return ret;
761}
762
766{
767public:
769 : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
770 {
771 }
772
773 static void check(
774 const exprt &expr,
776 {
777 unary_exprt::check(expr, vm);
778 }
779
780 static void validate(
781 const exprt &expr,
782 const namespacet &,
784 {
785 check(expr, vm);
786 }
787};
788
789template <>
791{
792 return base.id() == ID_overflow_unary_minus;
793}
794
795inline void validate_expr(const unary_overflow_exprt &value)
796{
798 value, 1, "unary overflow expression must have one operand");
799}
800
808{
811 static_cast<const unary_overflow_exprt &>(expr);
813 return ret;
814}
815
818{
820 unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
822 return ret;
823}
824
831{
832public:
838
843
844 bool zero_permitted() const
845 {
847 }
848
849 void zero_permitted(bool value)
850 {
851 set(ID_C_bounds_check, !value);
852 }
853
854 static void check(
855 const exprt &expr,
857 {
859 vm,
860 expr.operands().size() == 1,
861 "unary expression must have a single operand");
863 vm,
865 "operand must be of bitvector type");
866 }
867
868 static void validate(
869 const exprt &expr,
870 const namespacet &,
872 {
873 check(expr, vm);
874 }
875
878 exprt lower() const;
879};
880
881template <>
883{
884 return base.id() == ID_count_leading_zeros;
885}
886
888{
889 validate_operands(value, 1, "count_leading_zeros must have one operand");
890}
891
898inline const count_leading_zeros_exprt &
900{
903 static_cast<const count_leading_zeros_exprt &>(expr);
905 return ret;
906}
907
917
924{
925public:
931
936
937 bool zero_permitted() const
938 {
940 }
941
942 void zero_permitted(bool value)
943 {
944 set(ID_C_bounds_check, !value);
945 }
946
947 static void check(
948 const exprt &expr,
950 {
952 vm,
953 expr.operands().size() == 1,
954 "unary expression must have a single operand");
956 vm,
958 "operand must be of bitvector type");
959 }
960
961 static void validate(
962 const exprt &expr,
963 const namespacet &,
965 {
966 check(expr, vm);
967 }
968
971 exprt lower() const;
972};
973
974template <>
976{
977 return base.id() == ID_count_trailing_zeros;
978}
979
981{
982 validate_operands(value, 1, "count_trailing_zeros must have one operand");
983}
984
991inline const count_trailing_zeros_exprt &
993{
996 static_cast<const count_trailing_zeros_exprt &>(expr);
998 return ret;
999}
1000
1010
1013{
1014public:
1016 : unary_exprt(ID_bitreverse, std::move(op))
1017 {
1018 }
1019
1022 exprt lower() const;
1023};
1024
1025template <>
1027{
1028 return base.id() == ID_bitreverse;
1029}
1030
1031inline void validate_expr(const bitreverse_exprt &value)
1032{
1033 validate_operands(value, 1, "Bit-wise reverse must have one operand");
1034}
1035
1043{
1044 PRECONDITION(expr.id() == ID_bitreverse);
1045 const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
1047 return ret;
1048}
1049
1052{
1053 PRECONDITION(expr.id() == ID_bitreverse);
1054 bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
1056 return ret;
1057}
1058
1059#endif // CPROVER_UTIL_BITVECTOR_EXPR_H
bool can_cast_expr< count_trailing_zeros_exprt >(const exprt &base)
const replication_exprt & to_replication_expr(const exprt &expr)
Cast an exprt to a replication_exprt.
bool can_cast_expr< replication_exprt >(const exprt &base)
bool can_cast_expr< bswap_exprt >(const exprt &base)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
const shl_exprt & to_shl_expr(const exprt &expr)
Cast an exprt to a shl_exprt.
bool can_cast_expr< bitreverse_exprt >(const exprt &base)
bool can_cast_expr< count_leading_zeros_exprt >(const exprt &base)
const popcount_exprt & to_popcount_expr(const exprt &expr)
Cast an exprt to a popcount_exprt.
bool can_cast_expr< shift_exprt >(const exprt &base)
bool can_cast_expr< bitand_exprt >(const exprt &base)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast an exprt to an extractbits_exprt.
bool can_cast_expr< popcount_exprt >(const exprt &base)
bool can_cast_expr< extractbits_exprt >(const exprt &base)
bool can_cast_expr< bitxor_exprt >(const exprt &base)
const binary_overflow_exprt & to_binary_overflow_expr(const exprt &expr)
Cast an exprt to a binary_overflow_exprt.
bool can_cast_expr< bitor_exprt >(const exprt &base)
void validate_expr(const bswap_exprt &value)
const bitor_exprt & to_bitor_expr(const exprt &expr)
Cast an exprt to a bitor_exprt.
const bitand_exprt & to_bitand_expr(const exprt &expr)
Cast an exprt to a bitand_exprt.
const bitnot_exprt & to_bitnot_expr(const exprt &expr)
Cast an exprt to a bitnot_exprt.
const unary_overflow_exprt & to_unary_overflow_expr(const exprt &expr)
Cast an exprt to a unary_overflow_exprt.
bool can_cast_expr< concatenation_exprt >(const exprt &base)
bool can_cast_expr< unary_overflow_exprt >(const exprt &base)
const bitxor_exprt & to_bitxor_expr(const exprt &expr)
Cast an exprt to a bitxor_exprt.
const bswap_exprt & to_bswap_expr(const exprt &expr)
Cast an exprt to a bswap_exprt.
const count_leading_zeros_exprt & to_count_leading_zeros_expr(const exprt &expr)
Cast an exprt to a count_leading_zeros_exprt.
bool can_cast_expr< bitnot_exprt >(const exprt &base)
bool can_cast_expr< binary_overflow_exprt >(const exprt &base)
const bitreverse_exprt & to_bitreverse_expr(const exprt &expr)
Cast an exprt to a bitreverse_exprt.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast an exprt to an extractbit_exprt.
bool can_cast_expr< extractbit_exprt >(const exprt &base)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const count_trailing_zeros_exprt & to_count_trailing_zeros_expr(const exprt &expr)
Cast an exprt to a count_trailing_zeros_exprt.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Arithmetic right shift.
ashr_exprt(exprt _src, exprt _distance)
ashr_exprt(exprt _src, const std::size_t _distance)
A base class for binary expressions.
Definition std_expr.h:550
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition std_expr.h:562
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:643
Bit-wise AND.
bitand_exprt(const exprt &_op0, exprt _op1)
Bit-wise negation of bit-vectors.
bitnot_exprt(exprt op)
Bit-wise OR.
bitor_exprt(const exprt &_op0, exprt _op1)
Reverse the order of bits in a bit-vector.
bitreverse_exprt(exprt op)
exprt lower() const
Lower a bitreverse_exprt to arithmetic and logic expressions.
Bit-wise XOR.
bitxor_exprt(exprt _op0, exprt _op1)
The byte swap expression.
bswap_exprt(exprt _op, std::size_t bits_per_byte)
std::size_t get_bits_per_byte() const
bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
void set_bits_per_byte(std::size_t bits_per_byte)
Concatenation of bit-vector operands.
concatenation_exprt(operandst _operands, typet _type)
concatenation_exprt(exprt _op0, exprt _op1, typet _type)
A constant literal expression.
Definition std_expr.h:2807
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_leading_zeros_exprt to arithmetic and logic expressions.
count_leading_zeros_exprt(const exprt &_op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
count_trailing_zeros_exprt(const exprt &_op)
count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
void zero_permitted(bool value)
exprt lower() const
Lower a count_trailing_zeros_exprt to arithmetic and logic expressions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:343
exprt & op0()
Definition expr.h:99
exprt & op1()
Definition expr.h:102
exprt & op2()
Definition expr.h:105
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
Definition expr.h:253
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
Extracts a single bit of a bit-vector operand.
extractbit_exprt(exprt _src, exprt _index)
Extract the _index-th least significant bit from _src.
const exprt & index() const
const exprt & src() const
Extracts a sub-range of a bit-vector operand.
const exprt & upper() const
extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type)
Extract the bits [_lower .
const exprt & lower() const
const exprt & src() const
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:87
const irep_idt & id() const
Definition irep.h:396
Logical right shift.
lshr_exprt(exprt _src, const std::size_t _distance)
lshr_exprt(exprt _src, exprt _distance)
A base class for multi-ary expressions Associativity is not specified.
Definition std_expr.h:824
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The popcount (counting the number of bits set to 1) expression.
exprt lower() const
Lower a popcount_exprt to arithmetic and logic expressions.
popcount_exprt(exprt _op, typet _type)
popcount_exprt(const exprt &_op)
Bit-vector replication.
const exprt & op() const
const constant_exprt & times() const
constant_exprt & times()
replication_exprt(constant_exprt _times, exprt _src, typet _type)
A base class for shift and rotate operators.
exprt & distance()
shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
const exprt & distance() const
const exprt & op() const
Left shift.
shl_exprt(exprt _src, const std::size_t _distance)
shl_exprt(exprt _src, exprt _distance)
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:281
const exprt & op() const
Definition std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
unary_overflow_exprt(const irep_idt &kind, exprt _op)
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argu...
Definition std_expr.h:495
void validate_operands(const exprt &value, exprt::operandst::size_type number, const char *message, bool allow_more=false)
Definition expr_cast.h:250
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#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.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
#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