cprover
|
#include "base_type.h"
#include "expr_cast.h"
#include "invariant.h"
#include "mathematical_types.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 | transt |
Transition system, consisting of state invariant, initial state predicate, and transition predicate. 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. 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 | power_exprt |
Exponentiation. More... | |
class | factorial_power_exprt |
Falling factorial power. 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 | 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 | replication_exprt |
Bit-vector replication. 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 | function_application_exprt |
Application of (mathematical) function. More... | |
class | concatenation_exprt |
Concatenation of bit-vector operands. More... | |
class | infinity_exprt |
An expression denoting infinity. More... | |
class | let_exprt |
A let expression. More... | |
class | quantifier_exprt |
A base class for quantifier expressions. More... | |
class | forall_exprt |
A forall expression. More... | |
class | exists_exprt |
An exists 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... | |
API to expression classes
Definition in file std_expr.h.
|
inline |
Definition at line 458 of file std_expr.h.
|
inline |
Definition at line 3297 of file std_expr.h.
|
inline |
Definition at line 2474 of file std_expr.h.
|
inline |
Definition at line 1772 of file std_expr.h.
|
inline |
Definition at line 1789 of file std_expr.h.
|
inline |
Definition at line 1728 of file std_expr.h.
|
inline |
Definition at line 827 of file std_expr.h.
|
inline |
Definition at line 965 of file std_expr.h.
|
inline |
Definition at line 2851 of file std_expr.h.
|
inline |
Definition at line 2691 of file std_expr.h.
|
inline |
Definition at line 2742 of file std_expr.h.
|
inline |
Definition at line 2796 of file std_expr.h.
|
inline |
Definition at line 620 of file std_expr.h.
|
inline |
Definition at line 2030 of file std_expr.h.
|
inline |
Definition at line 2122 of file std_expr.h.
|
inline |
Definition at line 2075 of file std_expr.h.
|
inline |
Definition at line 4608 of file std_expr.h.
|
inline |
Definition at line 4436 of file std_expr.h.
|
inline |
Definition at line 3416 of file std_expr.h.
|
inline |
Definition at line 1276 of file std_expr.h.
|
inline |
Definition at line 2265 of file std_expr.h.
|
inline |
Definition at line 1534 of file std_expr.h.
|
inline |
Definition at line 3146 of file std_expr.h.
|
inline |
Definition at line 3244 of file std_expr.h.
|
inline |
Definition at line 1472 of file std_expr.h.
|
inline |
Definition at line 2398 of file std_expr.h.
|
inline |
Definition at line 4544 of file std_expr.h.
|
inline |
Definition at line 4217 of file std_expr.h.
|
inline |
Definition at line 4270 of file std_expr.h.
|
inline |
Definition at line 3501 of file std_expr.h.
|
inline |
Definition at line 2520 of file std_expr.h.
|
inline |
Definition at line 3646 of file std_expr.h.
|
inline |
Definition at line 1667 of file std_expr.h.
|
inline |
Definition at line 4120 of file std_expr.h.
|
inline |
Definition at line 4074 of file std_expr.h.
|
inline |
Definition at line 4024 of file std_expr.h.
|
inline |
Definition at line 4166 of file std_expr.h.
|
inline |
Definition at line 4698 of file std_expr.h.
|
inline |
Definition at line 3696 of file std_expr.h.
|
inline |
Definition at line 3978 of file std_expr.h.
|
inline |
Definition at line 1147 of file std_expr.h.
|
inline |
Definition at line 1324 of file std_expr.h.
|
inline |
Definition at line 1200 of file std_expr.h.
|
inline |
Definition at line 320 of file std_expr.h.
|
inline |
Definition at line 3343 of file std_expr.h.
|
inline |
Definition at line 1584 of file std_expr.h.
|
inline |
Definition at line 2197 of file std_expr.h.
|
inline |
Definition at line 2596 of file std_expr.h.
|
inline |
Definition at line 1095 of file std_expr.h.
|
inline |
Definition at line 4856 of file std_expr.h.
|
inline |
Definition at line 1420 of file std_expr.h.
|
inline |
Definition at line 4765 of file std_expr.h.
|
inline |
Definition at line 1372 of file std_expr.h.
|
inline |
Definition at line 3069 of file std_expr.h.
|
inline |
Definition at line 728 of file std_expr.h.
|
inline |
Definition at line 1955 of file std_expr.h.
|
inline |
Definition at line 266 of file std_expr.h.
|
inline |
Definition at line 132 of file std_expr.h.
|
inline |
Definition at line 2325 of file std_expr.h.
|
inline |
Definition at line 412 of file std_expr.h.
|
inline |
Definition at line 515 of file std_expr.h.
|
inline |
Definition at line 558 of file std_expr.h.
|
inline |
Definition at line 1909 of file std_expr.h.
|
inline |
Definition at line 3789 of file std_expr.h.
|
inline |
Definition at line 1833 of file std_expr.h.
|
inline |
Definition at line 3588 of file std_expr.h.
|
inline |
Definition at line 2639 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 50 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 26 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 439 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 449 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 3282 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 3290 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 2455 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 2465 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 1759 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 1766 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 1709 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 1719 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 810 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 819 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 948 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 957 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 2832 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 2842 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 2674 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 2683 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 2723 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 2733 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 2777 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 2787 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 600 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 610 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 2011 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 2021 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 2102 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 2112 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 2055 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 2065 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 4589 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 4599 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 4893 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 4902 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 4423 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 4430 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 3397 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 3407 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 1257 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 1267 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 2245 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 2256 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 1519 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 1527 of file std_expr.h.
|
inline |
Definition at line 4796 of file std_expr.h.
|
inline |
Definition at line 4805 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 3127 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 3137 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 3225 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 3235 of file std_expr.h.
|
inline |
Cast an exprt to a factorial_power_exprt.
expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 1463 of file std_expr.h.
|
inline |
Cast an exprt to a factorial_power_exprt.
expr must be known to be factorial_power_exprt.
expr | Source expression |
Definition at line 1453 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 2378 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 2388 of file std_expr.h.
|
inline |
Cast an exprt to a function_application_exprt.
expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 4523 of file std_expr.h.
|
inline |
Cast an exprt to a function_application_exprt.
expr must be known to be function_application_exprt.
expr | Source expression |
Definition at line 4534 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 4197 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 4207 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 4249 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 4260 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 4338 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 4347 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 3482 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 3492 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 2505 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 2513 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 3627 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 3637 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 1648 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 1658 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 4105 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 4113 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 4055 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 4065 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 4009 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 4017 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 4151 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 4159 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 4683 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 4691 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 3677 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 3687 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 3959 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 3969 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 1128 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 1138 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 1309 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 1317 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 1181 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 1191 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 1028 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 1034 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 305 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 313 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 3328 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 3336 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 1565 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 1575 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 2176 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 2187 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 2577 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 2587 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 1076 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 1086 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 4840 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 4848 of file std_expr.h.
|
inline |
Cast an exprt to a power_exprt.
expr must be known to be power_exprt.
expr | Source expression |
Definition at line 1405 of file std_expr.h.
|
inline |
Cast an exprt to a power_exprt.
expr must be known to be power_exprt.
expr | Source expression |
Definition at line 1413 of file std_expr.h.
|
inline |
Cast an exprt to a quantifier_exprt.
expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 4746 of file std_expr.h.
|
inline |
Cast an exprt to a quantifier_exprt.
expr must be known to be quantifier_exprt.
expr | Source expression |
Definition at line 4756 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 1357 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 1365 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 3050 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 3060 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 2917 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 2926 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 710 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 719 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 1942 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 1949 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 251 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 259 of file std_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 113 of file std_expr.h.
Cast an exprt to a transt expr must be known to be transt.
expr | Source expression |
Definition at line 123 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 2306 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 2316 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 395 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 404 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 496 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 506 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 540 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 549 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 1890 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 1900 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 3770 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 3780 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 1820 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 1827 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 3569 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 3579 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 2626 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 2633 of file std_expr.h.
|
inline |
Definition at line 462 of file std_expr.h.
|
inline |
Definition at line 3301 of file std_expr.h.
|
inline |
Definition at line 1794 of file std_expr.h.
|
inline |
Definition at line 1732 of file std_expr.h.
|
inline |
Definition at line 624 of file std_expr.h.
|
inline |
Definition at line 2034 of file std_expr.h.
|
inline |
Definition at line 2127 of file std_expr.h.
|
inline |
Definition at line 2080 of file std_expr.h.
|
inline |
Definition at line 3420 of file std_expr.h.
|
inline |
Definition at line 1280 of file std_expr.h.
|
inline |
Definition at line 2270 of file std_expr.h.
|
inline |
Definition at line 1538 of file std_expr.h.
|
inline |
Definition at line 3150 of file std_expr.h.
|
inline |
Definition at line 3248 of file std_expr.h.
|
inline |
Definition at line 1477 of file std_expr.h.
|
inline |
Definition at line 2402 of file std_expr.h.
|
inline |
Definition at line 4548 of file std_expr.h.
|
inline |
Definition at line 4221 of file std_expr.h.
|
inline |
Definition at line 4274 of file std_expr.h.
|
inline |
Definition at line 3505 of file std_expr.h.
|
inline |
Definition at line 2524 of file std_expr.h.
|
inline |
Definition at line 3650 of file std_expr.h.
|
inline |
Definition at line 1671 of file std_expr.h.
|
inline |
Definition at line 4124 of file std_expr.h.
|
inline |
Definition at line 4078 of file std_expr.h.
|
inline |
Definition at line 4028 of file std_expr.h.
|
inline |
Definition at line 4170 of file std_expr.h.
|
inline |
Definition at line 4702 of file std_expr.h.
|
inline |
Definition at line 3700 of file std_expr.h.
|
inline |
Definition at line 3982 of file std_expr.h.
|
inline |
Definition at line 1151 of file std_expr.h.
|
inline |
Definition at line 1328 of file std_expr.h.
|
inline |
Definition at line 1204 of file std_expr.h.
|
inline |
Definition at line 324 of file std_expr.h.
|
inline |
Definition at line 3348 of file std_expr.h.
|
inline |
Definition at line 1588 of file std_expr.h.
|
inline |
Definition at line 2201 of file std_expr.h.
|
inline |
Definition at line 1099 of file std_expr.h.
|
inline |
Definition at line 4860 of file std_expr.h.
|
inline |
Definition at line 1424 of file std_expr.h.
|
inline |
Definition at line 4770 of file std_expr.h.
|
inline |
Definition at line 1376 of file std_expr.h.
|
inline |
Definition at line 3073 of file std_expr.h.
|
inline |
Definition at line 732 of file std_expr.h.
|
inline |
Definition at line 270 of file std_expr.h.
|
inline |
Definition at line 136 of file std_expr.h.
|
inline |
Definition at line 2329 of file std_expr.h.
|
inline |
Definition at line 519 of file std_expr.h.
|
inline |
Definition at line 562 of file std_expr.h.
|
inline |
Definition at line 1913 of file std_expr.h.
|
inline |
Definition at line 3793 of file std_expr.h.
|
inline |
Definition at line 3592 of file std_expr.h.