cprover
|
#include "as_const.h"
#include "expr_cast.h"
#include "invariant.h"
#include "narrow.h"
#include "std_types.h"
Go to the source code of this file.
Classes | |
class | nullary_exprt |
An expression without operands. More... | |
class | ternary_exprt |
An expression with three operands. More... | |
class | symbol_exprt |
Expression to hold a symbol (variable) More... | |
class | decorated_symbol_exprt |
Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local. More... | |
class | nondet_symbol_exprt |
Expression to hold a nondeterministic choice. More... | |
class | unary_exprt |
Generic base class for unary expressions. More... | |
class | abs_exprt |
Absolute value. More... | |
class | unary_minus_exprt |
The unary minus expression. More... | |
class | unary_plus_exprt |
The unary plus expression. More... | |
class | bswap_exprt |
The byte swap expression. More... | |
class | predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed. More... | |
class | unary_predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly one argument. More... | |
class | sign_exprt |
Sign of an expression Predicate is true if _op is negative, false otherwise. More... | |
class | binary_exprt |
A base class for binary expressions. More... | |
class | binary_predicate_exprt |
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two arguments. More... | |
class | binary_relation_exprt |
A base class for relations, i.e., binary predicates whose two operands have the same type. More... | |
class | multi_ary_exprt |
A base class for multi-ary expressions Associativity is not specified. More... | |
class | plus_exprt |
The plus expression Associativity is not specified. More... | |
class | minus_exprt |
Binary minus. More... | |
class | mult_exprt |
Binary multiplication Associativity is not specified. More... | |
class | div_exprt |
Division. More... | |
class | mod_exprt |
Modulo. More... | |
class | rem_exprt |
Remainder of division. More... | |
class | equal_exprt |
Equality. More... | |
class | notequal_exprt |
Disequality. More... | |
class | index_exprt |
Array index operator. More... | |
class | array_of_exprt |
Array constructor from single element. More... | |
class | array_exprt |
Array constructor from list of elements. More... | |
class | array_list_exprt |
Array constructor from a list of index-element pairs Operands are index/value pairs, alternating. More... | |
class | vector_exprt |
Vector constructor from list of elements. More... | |
class | union_exprt |
Union constructor from single element. More... | |
class | struct_exprt |
Struct constructor from list of elements. More... | |
class | complex_exprt |
Complex constructor from a pair of numbers. More... | |
class | complex_real_exprt |
Real part of the expression describing a complex number. More... | |
class | complex_imag_exprt |
Imaginary part of the expression describing a complex number. More... | |
class | object_descriptor_exprt |
Split an expression into a base object and a (byte) offset. More... | |
class | dynamic_object_exprt |
Representation of heap-allocated objects. More... | |
class | is_dynamic_object_exprt |
Evaluates to true if the operand is a pointer to a dynamic object. More... | |
class | typecast_exprt |
Semantic type conversion. More... | |
class | floatbv_typecast_exprt |
Semantic type conversion from/to floating-point formats. More... | |
class | and_exprt |
Boolean AND. More... | |
class | implies_exprt |
Boolean implication. More... | |
class | or_exprt |
Boolean OR. More... | |
class | xor_exprt |
Boolean XOR. More... | |
class | bitnot_exprt |
Bit-wise negation of bit-vectors. More... | |
class | bitor_exprt |
Bit-wise OR. More... | |
class | bitxor_exprt |
Bit-wise XOR. More... | |
class | bitand_exprt |
Bit-wise AND. More... | |
class | shift_exprt |
A base class for shift operators. More... | |
class | shl_exprt |
Left shift. More... | |
class | ashr_exprt |
Arithmetic right shift. More... | |
class | lshr_exprt |
Logical right shift. More... | |
class | extractbit_exprt |
Extracts a single bit of a bit-vector operand. More... | |
class | extractbits_exprt |
Extracts a sub-range of a bit-vector operand. More... | |
class | address_of_exprt |
Operator to return the address of an object. More... | |
class | not_exprt |
Boolean negation. More... | |
class | dereference_exprt |
Operator to dereference a pointer. More... | |
class | if_exprt |
The trinary if-then-else operator. More... | |
class | with_exprt |
Operator to update elements in structs and arrays. More... | |
class | index_designatort |
class | member_designatort |
class | update_exprt |
Operator to update elements in structs and arrays. More... | |
class | member_exprt |
Extract member of struct or union. More... | |
class | isnan_exprt |
Evaluates to true if the operand is NaN. More... | |
class | isinf_exprt |
Evaluates to true if the operand is infinite. More... | |
class | isfinite_exprt |
Evaluates to true if the operand is finite. More... | |
class | isnormal_exprt |
Evaluates to true if the operand is a normal number. More... | |
class | ieee_float_equal_exprt |
IEEE-floating-point equality. More... | |
class | ieee_float_notequal_exprt |
IEEE floating-point disequality. More... | |
class | ieee_float_op_exprt |
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2). More... | |
class | type_exprt |
An expression denoting a type. More... | |
class | constant_exprt |
A constant literal expression. More... | |
class | true_exprt |
The Boolean constant true. More... | |
class | false_exprt |
The Boolean constant false. More... | |
class | nil_exprt |
The NIL expression. More... | |
class | null_pointer_exprt |
The null pointer constant. More... | |
class | replication_exprt |
Bit-vector replication. More... | |
class | concatenation_exprt |
Concatenation of bit-vector operands. More... | |
class | infinity_exprt |
An expression denoting infinity. More... | |
class | binding_exprt |
A base class for variable bindings (quantifiers, let, lambda) More... | |
class | let_exprt |
A let expression. More... | |
class | popcount_exprt |
The popcount (counting the number of bits set to 1) expression. More... | |
class | cond_exprt |
this is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true. More... | |
class | array_comprehension_exprt |
Expression to define a mapping from an argument (index) to elements. More... | |
class | class_method_descriptor_exprt |
An expression describing a method on a class. More... | |
API to expression classes
Definition in file std_expr.h.
|
inline |
Definition at line 342 of file std_expr.h.
|
inline |
Definition at line 2836 of file std_expr.h.
|
inline |
Definition at line 2202 of file std_expr.h.
|
inline |
Definition at line 4497 of file std_expr.h.
|
inline |
Definition at line 1463 of file std_expr.h.
|
inline |
Definition at line 1515 of file std_expr.h.
|
inline |
Definition at line 1402 of file std_expr.h.
|
inline |
Definition at line 662 of file std_expr.h.
|
inline |
Definition at line 758 of file std_expr.h.
|
inline |
Definition at line 2498 of file std_expr.h.
|
inline |
Definition at line 2381 of file std_expr.h.
|
inline |
Definition at line 2426 of file std_expr.h.
|
inline |
Definition at line 2462 of file std_expr.h.
|
inline |
Definition at line 497 of file std_expr.h.
|
inline |
Definition at line 4637 of file std_expr.h.
|
inline |
Definition at line 1722 of file std_expr.h.
|
inline |
Definition at line 1811 of file std_expr.h.
|
inline |
Definition at line 1766 of file std_expr.h.
|
inline |
Definition at line 4113 of file std_expr.h.
|
inline |
Definition at line 4408 of file std_expr.h.
|
inline |
Definition at line 3957 of file std_expr.h.
|
inline |
Definition at line 2957 of file std_expr.h.
|
inline |
Definition at line 1070 of file std_expr.h.
|
inline |
Definition at line 1970 of file std_expr.h.
|
inline |
Definition at line 1220 of file std_expr.h.
|
inline |
Definition at line 2690 of file std_expr.h.
|
inline |
Definition at line 2779 of file std_expr.h.
|
inline |
Definition at line 2129 of file std_expr.h.
|
inline |
Definition at line 3730 of file std_expr.h.
|
inline |
Definition at line 3779 of file std_expr.h.
|
inline |
Definition at line 3862 of file std_expr.h.
|
inline |
Definition at line 3042 of file std_expr.h.
|
inline |
Definition at line 2238 of file std_expr.h.
|
inline |
Definition at line 3178 of file std_expr.h.
|
inline |
Definition at line 1337 of file std_expr.h.
|
inline |
Definition at line 3637 of file std_expr.h.
|
inline |
Definition at line 3592 of file std_expr.h.
|
inline |
Definition at line 3547 of file std_expr.h.
|
inline |
Definition at line 3682 of file std_expr.h.
|
inline |
Definition at line 4302 of file std_expr.h.
|
inline |
Definition at line 3227 of file std_expr.h.
|
inline |
Definition at line 3502 of file std_expr.h.
|
inline |
Definition at line 955 of file std_expr.h.
|
inline |
Definition at line 1115 of file std_expr.h.
|
inline |
Definition at line 1001 of file std_expr.h.
|
inline |
Definition at line 4011 of file std_expr.h.
|
inline |
Definition at line 232 of file std_expr.h.
|
inline |
Definition at line 2881 of file std_expr.h.
|
inline |
Definition at line 1263 of file std_expr.h.
|
inline |
Definition at line 1899 of file std_expr.h.
|
inline |
Definition at line 2310 of file std_expr.h.
|
inline |
Definition at line 910 of file std_expr.h.
|
inline |
Definition at line 4351 of file std_expr.h.
|
inline |
Definition at line 1160 of file std_expr.h.
|
inline |
Definition at line 4057 of file std_expr.h.
|
inline |
Definition at line 2556 of file std_expr.h.
|
inline |
Definition at line 566 of file std_expr.h.
|
inline |
Definition at line 1662 of file std_expr.h.
|
inline |
Definition at line 161 of file std_expr.h.
|
inline |
Definition at line 3907 of file std_expr.h.
|
inline |
Definition at line 2060 of file std_expr.h.
|
inline |
Definition at line 300 of file std_expr.h.
|
inline |
Definition at line 392 of file std_expr.h.
|
inline |
Definition at line 436 of file std_expr.h.
|
inline |
Definition at line 1609 of file std_expr.h.
|
inline |
Definition at line 3311 of file std_expr.h.
|
inline |
Definition at line 1552 of file std_expr.h.
|
inline |
Definition at line 3121 of file std_expr.h.
|
inline |
Definition at line 2346 of file std_expr.h.
exprt conjunction | ( | const exprt::operandst & | ) |
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise
Definition at line 51 of file std_expr.cpp.
exprt disjunction | ( | const exprt::operandst & | ) |
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise
Definition at line 29 of file std_expr.cpp.
Cast an exprt to a abs_exprt.
expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 358 of file std_expr.h.
Cast an exprt to a abs_exprt.
expr must be known to be abs_exprt.
expr | Source expression |
Definition at line 367 of file std_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 2852 of file std_expr.h.
|
inline |
Cast an exprt to an address_of_exprt.
expr must be known to be address_of_exprt.
expr | Source expression |
Definition at line 2861 of file std_expr.h.
Cast an exprt to a and_exprt.
expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2213 of file std_expr.h.
Cast an exprt to a and_exprt.
expr must be known to be and_exprt.
expr | Source expression |
Definition at line 2220 of file std_expr.h.
|
inline |
Cast an exprt to a array_comprehension_exprt.
expr must be known to be array_comprehension_exprt.
expr | Source expression |
Definition at line 4514 of file std_expr.h.
|
inline |
Cast an exprt to a array_comprehension_exprt.
expr must be known to be array_comprehension_exprt.
expr | Source expression |
Definition at line 4524 of file std_expr.h.
|
inline |
Cast an exprt to an array_exprt.
expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1474 of file std_expr.h.
|
inline |
Cast an exprt to an array_exprt.
expr must be known to be array_exprt.
expr | Source expression |
Definition at line 1481 of file std_expr.h.
|
inline |
Definition at line 1525 of file std_expr.h.
|
inline |
Definition at line 1533 of file std_expr.h.
|
inline |
Cast an exprt to an array_of_exprt.
expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1418 of file std_expr.h.
|
inline |
Cast an exprt to an array_of_exprt.
expr must be known to be array_of_exprt.
expr | Source expression |
Definition at line 1427 of file std_expr.h.
|
inline |
Cast an exprt to a binary_exprt.
expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 678 of file std_expr.h.
|
inline |
Cast an exprt to a binary_exprt.
expr must be known to be binary_exprt.
expr | Source expression |
Definition at line 685 of file std_expr.h.
|
inline |
Cast an exprt to a binary_relation_exprt.
expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 774 of file std_expr.h.
|
inline |
Cast an exprt to a binary_relation_exprt.
expr must be known to be binary_relation_exprt.
expr | Source expression |
Definition at line 781 of file std_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2509 of file std_expr.h.
|
inline |
Cast an exprt to a bitand_exprt.
expr must be known to be bitand_exprt.
expr | Source expression |
Definition at line 2516 of file std_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2397 of file std_expr.h.
|
inline |
Cast an exprt to a bitnot_exprt.
expr must be known to be bitnot_exprt.
expr | Source expression |
Definition at line 2406 of file std_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2437 of file std_expr.h.
|
inline |
Cast an exprt to a bitor_exprt.
expr must be known to be bitor_exprt.
expr | Source expression |
Definition at line 2444 of file std_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2473 of file std_expr.h.
|
inline |
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2480 of file std_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 515 of file std_expr.h.
|
inline |
Cast an exprt to a bswap_exprt.
expr must be known to be bswap_exprt.
expr | Source expression |
Definition at line 524 of file std_expr.h.
|
inline |
Cast an exprt to a class_method_descriptor_exprt.
expr must be known to be class_method_descriptor_exprt.
expr | Source expression |
Definition at line 4627 of file std_expr.h.
|
inline |
Cast an exprt to a complex_exprt.
expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1738 of file std_expr.h.
|
inline |
Cast an exprt to a complex_exprt.
expr must be known to be complex_exprt.
expr | Source expression |
Definition at line 1747 of file std_expr.h.
|
inline |
Cast an exprt to a complex_imag_exprt.
expr must be known to be a complex_imag_exprt.
expr | Source expression |
Definition at line 1828 of file std_expr.h.
|
inline |
Cast an exprt to a complex_imag_exprt.
expr must be known to be a complex_imag_exprt.
expr | Source expression |
Definition at line 1837 of file std_expr.h.
|
inline |
Cast an exprt to a complex_real_exprt.
expr must be known to be a complex_real_exprt.
expr | Source expression |
Definition at line 1783 of file std_expr.h.
|
inline |
Cast an exprt to a complex_real_exprt.
expr must be known to be a complex_real_exprt.
expr | Source expression |
Definition at line 1792 of file std_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4124 of file std_expr.h.
|
inline |
Cast an exprt to a concatenation_exprt.
expr must be known to be concatenation_exprt.
expr | Source expression |
Definition at line 4131 of file std_expr.h.
|
inline |
Cast an exprt to a cond_exprt.
expr must be known to be cond_exprt.
expr | Source expression |
Definition at line 4425 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4434 of file std_expr.h.
|
inline |
Cast an exprt to a constant_exprt.
expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 3968 of file std_expr.h.
|
inline |
Cast an exprt to a constant_exprt.
expr must be known to be constant_exprt.
expr | Source expression |
Definition at line 3975 of file std_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 2973 of file std_expr.h.
|
inline |
Cast an exprt to a dereference_exprt.
expr must be known to be dereference_exprt.
expr | Source expression |
Definition at line 2982 of file std_expr.h.
Cast an exprt to a div_exprt.
expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1086 of file std_expr.h.
Cast an exprt to a div_exprt.
expr must be known to be div_exprt.
expr | Source expression |
Definition at line 1095 of file std_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 1986 of file std_expr.h.
|
inline |
Cast an exprt to a dynamic_object_exprt.
expr must be known to be dynamic_object_exprt.
expr | Source expression |
Definition at line 1997 of file std_expr.h.
|
inline |
Cast an exprt to an equal_exprt.
expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1236 of file std_expr.h.
|
inline |
Cast an exprt to an equal_exprt.
expr must be known to be equal_exprt.
expr | Source expression |
Definition at line 1244 of file std_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 2706 of file std_expr.h.
|
inline |
Cast an exprt to an extractbit_exprt.
expr must be known to be extractbit_exprt.
expr | Source expression |
Definition at line 2715 of file std_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 2795 of file std_expr.h.
|
inline |
Cast an exprt to an extractbits_exprt.
expr must be known to be extractbits_exprt.
expr | Source expression |
Definition at line 2804 of file std_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2145 of file std_expr.h.
|
inline |
Cast an exprt to a floatbv_typecast_exprt.
expr must be known to be floatbv_typecast_exprt.
expr | Source expression |
Definition at line 2155 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 3746 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_equal_exprt.
expr must be known to be ieee_float_equal_exprt.
expr | Source expression |
Definition at line 3756 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 3795 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_notequal_exprt.
expr must be known to be ieee_float_notequal_exprt.
expr | Source expression |
Definition at line 3806 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 3880 of file std_expr.h.
|
inline |
Cast an exprt to an ieee_float_op_exprt.
expr must be known to be ieee_float_op_exprt.
expr | Source expression |
Definition at line 3889 of file std_expr.h.
Cast an exprt to an if_exprt.
expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3058 of file std_expr.h.
Cast an exprt to an if_exprt.
expr must be known to be if_exprt.
expr | Source expression |
Definition at line 3067 of file std_expr.h.
|
inline |
Cast an exprt to a implies_exprt.
expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2254 of file std_expr.h.
|
inline |
Cast an exprt to a implies_exprt.
expr must be known to be implies_exprt.
expr | Source expression |
Definition at line 2263 of file std_expr.h.
|
inline |
Cast an exprt to an index_designatort.
expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3194 of file std_expr.h.
|
inline |
Cast an exprt to an index_designatort.
expr must be known to be index_designatort.
expr | Source expression |
Definition at line 3203 of file std_expr.h.
|
inline |
Cast an exprt to an index_exprt.
expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1353 of file std_expr.h.
|
inline |
Cast an exprt to an index_exprt.
expr must be known to be index_exprt.
expr | Source expression |
Definition at line 1362 of file std_expr.h.
|
inline |
Definition at line 2022 of file std_expr.h.
|
inline |
Definition at line 2032 of file std_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 3653 of file std_expr.h.
|
inline |
Cast an exprt to a isfinite_exprt.
expr must be known to be isfinite_exprt.
expr | Source expression |
Definition at line 3662 of file std_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 3608 of file std_expr.h.
|
inline |
Cast an exprt to a isinf_exprt.
expr must be known to be isinf_exprt.
expr | Source expression |
Definition at line 3617 of file std_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 3563 of file std_expr.h.
|
inline |
Cast an exprt to a isnan_exprt.
expr must be known to be isnan_exprt.
expr | Source expression |
Definition at line 3572 of file std_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 3698 of file std_expr.h.
|
inline |
Cast an exprt to a isnormal_exprt.
expr must be known to be isnormal_exprt.
expr | Source expression |
Definition at line 3707 of file std_expr.h.
Cast an exprt to a let_exprt.
expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4318 of file std_expr.h.
Cast an exprt to a let_exprt.
expr must be known to be let_exprt.
expr | Source expression |
Definition at line 4327 of file std_expr.h.
|
inline |
Cast an exprt to an member_designatort.
expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3243 of file std_expr.h.
|
inline |
Cast an exprt to an member_designatort.
expr must be known to be member_designatort.
expr | Source expression |
Definition at line 3252 of file std_expr.h.
|
inline |
Cast an exprt to a member_exprt.
expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3518 of file std_expr.h.
|
inline |
Cast an exprt to a member_exprt.
expr must be known to be member_exprt.
expr | Source expression |
Definition at line 3527 of file std_expr.h.
|
inline |
Cast an exprt to a minus_exprt.
expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 971 of file std_expr.h.
|
inline |
Cast an exprt to a minus_exprt.
expr must be known to be minus_exprt.
expr | Source expression |
Definition at line 980 of file std_expr.h.
Cast an exprt to a mod_exprt.
expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1131 of file std_expr.h.
Cast an exprt to a mod_exprt.
expr must be known to be mod_exprt.
expr | Source expression |
Definition at line 1140 of file std_expr.h.
|
inline |
Cast an exprt to a mult_exprt.
expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1017 of file std_expr.h.
|
inline |
Cast an exprt to a mult_exprt.
expr must be known to be mult_exprt.
expr | Source expression |
Definition at line 1026 of file std_expr.h.
|
inline |
Cast an exprt to a multi_ary_exprt.
expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 872 of file std_expr.h.
|
inline |
Cast an exprt to a multi_ary_exprt.
expr must be known to be multi_ary_exprt.
expr | Source expression |
Definition at line 878 of file std_expr.h.
|
inline |
Cast an exprt to a nondet_symbol_exprt.
expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 248 of file std_expr.h.
|
inline |
Cast an exprt to a nondet_symbol_exprt.
expr must be known to be nondet_symbol_exprt.
expr | Source expression |
Definition at line 258 of file std_expr.h.
Cast an exprt to an not_exprt.
expr must be known to be not_exprt.
expr | Source expression |
Definition at line 2897 of file std_expr.h.
Cast an exprt to an not_exprt.
expr must be known to be not_exprt.
expr | Source expression |
Definition at line 2906 of file std_expr.h.
|
inline |
Cast an exprt to an notequal_exprt.
expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1279 of file std_expr.h.
|
inline |
Cast an exprt to an notequal_exprt.
expr must be known to be notequal_exprt.
expr | Source expression |
Definition at line 1288 of file std_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 1915 of file std_expr.h.
|
inline |
Cast an exprt to an object_descriptor_exprt.
expr must be known to be object_descriptor_exprt.
expr | Source expression |
Definition at line 1926 of file std_expr.h.
Cast an exprt to a or_exprt.
expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2321 of file std_expr.h.
Cast an exprt to a or_exprt.
expr must be known to be or_exprt.
expr | Source expression |
Definition at line 2328 of file std_expr.h.
|
inline |
Cast an exprt to a plus_exprt.
expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 926 of file std_expr.h.
|
inline |
Cast an exprt to a plus_exprt.
expr must be known to be plus_exprt.
expr | Source expression |
Definition at line 935 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4367 of file std_expr.h.
|
inline |
Cast an exprt to a popcount_exprt.
expr must be known to be popcount_exprt.
expr | Source expression |
Definition at line 4376 of file std_expr.h.
Cast an exprt to a rem_exprt.
expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1176 of file std_expr.h.
Cast an exprt to a rem_exprt.
expr must be known to be rem_exprt.
expr | Source expression |
Definition at line 1185 of file std_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 4073 of file std_expr.h.
|
inline |
Cast an exprt to a replication_exprt.
expr must be known to be replication_exprt.
expr | Source expression |
Definition at line 4082 of file std_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2572 of file std_expr.h.
|
inline |
Cast an exprt to a shift_exprt.
expr must be known to be shift_exprt.
expr | Source expression |
Definition at line 2580 of file std_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 2609 of file std_expr.h.
Cast an exprt to a shl_exprt.
expr must be known to be shl_exprt.
expr | Source expression |
Definition at line 2618 of file std_expr.h.
|
inline |
Cast an exprt to a sign_exprt.
expr must be known to be a sign_exprt.
expr | Source expression |
Definition at line 582 of file std_expr.h.
|
inline |
Cast an exprt to a sign_exprt.
expr must be known to be a sign_exprt.
expr | Source expression |
Definition at line 591 of file std_expr.h.
|
inline |
Cast an exprt to a struct_exprt.
expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1673 of file std_expr.h.
|
inline |
Cast an exprt to a struct_exprt.
expr must be known to be struct_exprt.
expr | Source expression |
Definition at line 1680 of file std_expr.h.
|
inline |
Cast an exprt to a symbol_exprt.
expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 177 of file std_expr.h.
|
inline |
Cast an exprt to a symbol_exprt.
expr must be known to be symbol_exprt.
expr | Source expression |
Definition at line 186 of file std_expr.h.
|
inline |
Cast an exprt to an type_exprt.
expr must be known to be type_exprt.
expr | Source expression |
Definition at line 3918 of file std_expr.h.
|
inline |
Cast an exprt to an type_exprt.
expr must be known to be type_exprt.
expr | Source expression |
Definition at line 3926 of file std_expr.h.
|
inline |
Cast an exprt to a typecast_exprt.
expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2076 of file std_expr.h.
|
inline |
Cast an exprt to a typecast_exprt.
expr must be known to be typecast_exprt.
expr | Source expression |
Definition at line 2085 of file std_expr.h.
|
inline |
Cast an exprt to a unary_exprt.
expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 316 of file std_expr.h.
|
inline |
Cast an exprt to a unary_exprt.
expr must be known to be unary_exprt.
expr | Source expression |
Definition at line 324 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 408 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 417 of file std_expr.h.
|
inline |
Cast an exprt to a unary_plus_exprt.
expr must be known to be unary_plus_exprt.
expr | Source expression |
Definition at line 452 of file std_expr.h.
|
inline |
Cast an exprt to a unary_minus_exprt.
expr must be known to be unary_minus_exprt.
expr | Source expression |
Definition at line 461 of file std_expr.h.
|
inline |
Cast an exprt to a union_exprt.
expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1625 of file std_expr.h.
|
inline |
Cast an exprt to a union_exprt.
expr must be known to be union_exprt.
expr | Source expression |
Definition at line 1634 of file std_expr.h.
|
inline |
Cast an exprt to an update_exprt.
expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3328 of file std_expr.h.
|
inline |
Cast an exprt to an update_exprt.
expr must be known to be update_exprt.
expr | Source expression |
Definition at line 3337 of file std_expr.h.
|
inline |
Cast an exprt to an vector_exprt.
expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1563 of file std_expr.h.
|
inline |
Cast an exprt to an vector_exprt.
expr must be known to be vector_exprt.
expr | Source expression |
Definition at line 1570 of file std_expr.h.
|
inline |
Cast an exprt to a with_exprt.
expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3141 of file std_expr.h.
|
inline |
Cast an exprt to a with_exprt.
expr must be known to be with_exprt.
expr | Source expression |
Definition at line 3150 of file std_expr.h.
Cast an exprt to a xor_exprt.
expr must be known to be xor_exprt.
expr | Source expression |
Definition at line 2357 of file std_expr.h.
Cast an exprt to a bitxor_exprt.
expr must be known to be bitxor_exprt.
expr | Source expression |
Definition at line 2364 of file std_expr.h.
|
inline |
Definition at line 347 of file std_expr.h.
|
inline |
Definition at line 2841 of file std_expr.h.
|
inline |
Definition at line 4502 of file std_expr.h.
|
inline |
Definition at line 1520 of file std_expr.h.
|
inline |
Definition at line 1407 of file std_expr.h.
|
inline |
Definition at line 667 of file std_expr.h.
|
inline |
Definition at line 763 of file std_expr.h.
|
inline |
Definition at line 2386 of file std_expr.h.
|
inline |
Definition at line 502 of file std_expr.h.
|
inline |
Definition at line 4603 of file std_expr.h.
|
inline |
Definition at line 1727 of file std_expr.h.
|
inline |
Definition at line 1816 of file std_expr.h.
|
inline |
Definition at line 1771 of file std_expr.h.
|
inline |
Definition at line 4413 of file std_expr.h.
|
inline |
Definition at line 2962 of file std_expr.h.
|
inline |
Definition at line 1075 of file std_expr.h.
|
inline |
Definition at line 1975 of file std_expr.h.
|
inline |
Definition at line 1225 of file std_expr.h.
|
inline |
Definition at line 2695 of file std_expr.h.
|
inline |
Definition at line 2784 of file std_expr.h.
|
inline |
Definition at line 2134 of file std_expr.h.
|
inline |
Definition at line 3735 of file std_expr.h.
|
inline |
Definition at line 3784 of file std_expr.h.
|
inline |
Definition at line 3868 of file std_expr.h.
|
inline |
Definition at line 3047 of file std_expr.h.
|
inline |
Definition at line 2243 of file std_expr.h.
|
inline |
Definition at line 3183 of file std_expr.h.
|
inline |
Definition at line 1342 of file std_expr.h.
|
inline |
Definition at line 3642 of file std_expr.h.
|
inline |
Definition at line 3597 of file std_expr.h.
|
inline |
Definition at line 3552 of file std_expr.h.
|
inline |
Definition at line 3687 of file std_expr.h.
|
inline |
Definition at line 4307 of file std_expr.h.
|
inline |
Definition at line 3232 of file std_expr.h.
|
inline |
Definition at line 3507 of file std_expr.h.
|
inline |
Definition at line 960 of file std_expr.h.
|
inline |
Definition at line 1120 of file std_expr.h.
|
inline |
Definition at line 1006 of file std_expr.h.
|
inline |
Definition at line 237 of file std_expr.h.
|
inline |
Definition at line 2886 of file std_expr.h.
|
inline |
Definition at line 1268 of file std_expr.h.
|
inline |
Definition at line 1904 of file std_expr.h.
|
inline |
Definition at line 915 of file std_expr.h.
|
inline |
Definition at line 4356 of file std_expr.h.
|
inline |
Definition at line 1165 of file std_expr.h.
|
inline |
Definition at line 4062 of file std_expr.h.
|
inline |
Definition at line 2561 of file std_expr.h.
|
inline |
Definition at line 571 of file std_expr.h.
|
inline |
Definition at line 166 of file std_expr.h.
|
inline |
Definition at line 2065 of file std_expr.h.
|
inline |
Definition at line 305 of file std_expr.h.
|
inline |
Definition at line 397 of file std_expr.h.
|
inline |
Definition at line 441 of file std_expr.h.
|
inline |
Definition at line 1614 of file std_expr.h.
|
inline |
Definition at line 3316 of file std_expr.h.
|
inline |
Definition at line 3126 of file std_expr.h.