cprover
Conversion to specific expressions

Functions

const literal_exprtto_literal_expr (const exprt &expr)
 Cast a generic exprt to a literal_exprt. More...
 
literal_exprtto_literal_expr (exprt &expr)
 Cast a generic exprt to a literal_exprt. More...
 
const ssa_exprtto_ssa_expr (const exprt &expr)
 Cast a generic exprt to an ssa_exprt. More...
 
ssa_exprtto_ssa_expr (exprt &expr)
 Cast a generic exprt to an ssa_exprt. More...
 
const transtto_trans_expr (const exprt &expr)
 Cast a generic exprt to a transt. More...
 
transtto_trans_expr (exprt &expr)
 
const symbol_exprtto_symbol_expr (const exprt &expr)
 Cast a generic exprt to a symbol_exprt. More...
 
symbol_exprtto_symbol_expr (exprt &expr)
 Cast a generic exprt to a symbol_exprt. More...
 
const unary_exprtto_unary_expr (const exprt &expr)
 Cast a generic exprt to a unary_exprt. More...
 
unary_exprtto_unary_expr (exprt &expr)
 Cast a generic exprt to a unary_exprt. More...
 
const abs_exprtto_abs_expr (const exprt &expr)
 Cast a generic exprt to a abs_exprt. More...
 
abs_exprtto_abs_expr (exprt &expr)
 Cast a generic exprt to a abs_exprt. More...
 
const unary_minus_exprtto_unary_minus_expr (const exprt &expr)
 Cast a generic exprt to a unary_minus_exprt. More...
 
unary_minus_exprtto_unary_minus_expr (exprt &expr)
 Cast a generic exprt to a unary_minus_exprt. More...
 
const binary_exprtto_binary_expr (const exprt &expr)
 Cast a generic exprt to a binary_exprt. More...
 
binary_exprtto_binary_expr (exprt &expr)
 Cast a generic exprt to a binary_exprt. More...
 
const binary_relation_exprtto_binary_relation_expr (const exprt &expr)
 Cast a generic exprt to a binary_relation_exprt. More...
 
binary_relation_exprtto_binary_relation_expr (exprt &expr)
 Cast a generic exprt to a binary_relation_exprt. More...
 
const multi_ary_exprtto_multi_ary_expr (const exprt &expr)
 Cast a generic exprt to a multi_ary_exprt. More...
 
multi_ary_exprtto_multi_ary_expr (exprt &expr)
 Cast a generic exprt to a multi_ary_exprt. More...
 
const plus_exprtto_plus_expr (const exprt &expr)
 Cast a generic exprt to a plus_exprt. More...
 
plus_exprtto_plus_expr (exprt &expr)
 Cast a generic exprt to a plus_exprt. More...
 
const minus_exprtto_minus_expr (const exprt &expr)
 Cast a generic exprt to a minus_exprt. More...
 
minus_exprtto_minus_expr (exprt &expr)
 Cast a generic exprt to a minus_exprt. More...
 
const mult_exprtto_mult_expr (const exprt &expr)
 Cast a generic exprt to a mult_exprt. More...
 
mult_exprtto_mult_expr (exprt &expr)
 Cast a generic exprt to a mult_exprt. More...
 
const div_exprtto_div_expr (const exprt &expr)
 Cast a generic exprt to a div_exprt. More...
 
div_exprtto_div_expr (exprt &expr)
 Cast a generic exprt to a div_exprt. More...
 
const mod_exprtto_mod_expr (const exprt &expr)
 Cast a generic exprt to a mod_exprt. More...
 
mod_exprtto_mod_expr (exprt &expr)
 Cast a generic exprt to a mod_exprt. More...
 
const rem_exprtto_rem_expr (const exprt &expr)
 Cast a generic exprt to a rem_exprt. More...
 
rem_exprtto_rem_expr (exprt &expr)
 Cast a generic exprt to a rem_exprt. More...
 
const power_exprtto_power_expr (const exprt &expr)
 Cast a generic exprt to a power_exprt. More...
 
power_exprtto_power_expr (exprt &expr)
 Cast a generic exprt to a power_exprt. More...
 
const factorial_power_exprtto_factorial_power_expr (const exprt &expr)
 Cast a generic exprt to a factorial_power_exprt. More...
 
factorial_power_exprtto_factorial_expr (exprt &expr)
 Cast a generic exprt to a factorial_power_exprt. More...
 
const equal_exprtto_equal_expr (const exprt &expr)
 Cast a generic exprt to an equal_exprt. More...
 
equal_exprtto_equal_expr (exprt &expr)
 Cast a generic exprt to an equal_exprt. More...
 
const notequal_exprtto_notequal_expr (const exprt &expr)
 Cast a generic exprt to an notequal_exprt. More...
 
notequal_exprtto_notequal_expr (exprt &expr)
 Cast a generic exprt to an notequal_exprt. More...
 
const index_exprtto_index_expr (const exprt &expr)
 Cast a generic exprt to an index_exprt. More...
 
index_exprtto_index_expr (exprt &expr)
 Cast a generic exprt to an index_exprt. More...
 
const array_of_exprtto_array_of_expr (const exprt &expr)
 Cast a generic exprt to an array_of_exprt. More...
 
array_of_exprtto_array_of_expr (exprt &expr)
 Cast a generic exprt to an array_of_exprt. More...
 
const array_exprtto_array_expr (const exprt &expr)
 Cast a generic exprt to an array_exprt. More...
 
array_exprtto_array_expr (exprt &expr)
 Cast a generic exprt to an array_exprt. More...
 
const vector_exprtto_vector_expr (const exprt &expr)
 Cast a generic exprt to an vector_exprt. More...
 
vector_exprtto_vector_expr (exprt &expr)
 Cast a generic exprt to an vector_exprt. More...
 
const union_exprtto_union_expr (const exprt &expr)
 Cast a generic exprt to a union_exprt. More...
 
union_exprtto_union_expr (exprt &expr)
 Cast a generic exprt to a union_exprt. More...
 
const struct_exprtto_struct_expr (const exprt &expr)
 Cast a generic exprt to a struct_exprt. More...
 
struct_exprtto_struct_expr (exprt &expr)
 Cast a generic exprt to a struct_exprt. More...
 
const complex_exprtto_complex_expr (const exprt &expr)
 Cast a generic exprt to a complex_exprt. More...
 
complex_exprtto_complex_expr (exprt &expr)
 Cast a generic exprt to a complex_exprt. More...
 
const object_descriptor_exprtto_object_descriptor_expr (const exprt &expr)
 Cast a generic exprt to an object_descriptor_exprt. More...
 
object_descriptor_exprtto_object_descriptor_expr (exprt &expr)
 Cast a generic exprt to an object_descriptor_exprt. More...
 
const dynamic_object_exprtto_dynamic_object_expr (const exprt &expr)
 Cast a generic exprt to a dynamic_object_exprt. More...
 
dynamic_object_exprtto_dynamic_object_expr (exprt &expr)
 Cast a generic exprt to a dynamic_object_exprt. More...
 
const typecast_exprtto_typecast_expr (const exprt &expr)
 Cast a generic exprt to a typecast_exprt. More...
 
typecast_exprtto_typecast_expr (exprt &expr)
 Cast a generic exprt to a typecast_exprt. More...
 
const floatbv_typecast_exprtto_floatbv_typecast_expr (const exprt &expr)
 Cast a generic exprt to a floatbv_typecast_exprt. More...
 
floatbv_typecast_exprtto_floatbv_typecast_expr (exprt &expr)
 Cast a generic exprt to a floatbv_typecast_exprt. More...
 
const and_exprtto_and_expr (const exprt &expr)
 Cast a generic exprt to a and_exprt. More...
 
and_exprtto_and_expr (exprt &expr)
 Cast a generic exprt to a and_exprt. More...
 
const implies_exprtto_implies_expr (const exprt &expr)
 Cast a generic exprt to a implies_exprt. More...
 
implies_exprtto_implies_expr (exprt &expr)
 Cast a generic exprt to a implies_exprt. More...
 
const or_exprtto_or_expr (const exprt &expr)
 Cast a generic exprt to a or_exprt. More...
 
or_exprtto_or_expr (exprt &expr)
 Cast a generic exprt to a or_exprt. More...
 
const bitnot_exprtto_bitnot_expr (const exprt &expr)
 Cast a generic exprt to a bitnot_exprt. More...
 
bitnot_exprtto_bitnot_expr (exprt &expr)
 Cast a generic exprt to a bitnot_exprt. More...
 
const bitor_exprtto_bitor_expr (const exprt &expr)
 Cast a generic exprt to a bitor_exprt. More...
 
bitor_exprtto_bitor_expr (exprt &expr)
 Cast a generic exprt to a bitor_exprt. More...
 
const bitxor_exprtto_bitxor_expr (const exprt &expr)
 Cast a generic exprt to a bitxor_exprt. More...
 
bitxor_exprtto_bitxor_expr (exprt &expr)
 Cast a generic exprt to a bitxor_exprt. More...
 
const bitand_exprtto_bitand_expr (const exprt &expr)
 Cast a generic exprt to a bitand_exprt. More...
 
bitand_exprtto_bitand_expr (exprt &expr)
 Cast a generic exprt to a bitand_exprt. More...
 
const shift_exprtto_shift_expr (const exprt &expr)
 Cast a generic exprt to a shift_exprt. More...
 
shift_exprtto_shift_expr (exprt &expr)
 Cast a generic exprt to a shift_exprt. More...
 
const replication_exprtto_replication_expr (const exprt &expr)
 Cast a generic exprt to a replication_exprt. More...
 
replication_exprtto_replication_expr (exprt &expr)
 Cast a generic exprt to a replication_exprt. More...
 
const extractbit_exprtto_extractbit_expr (const exprt &expr)
 Cast a generic exprt to an extractbit_exprt. More...
 
extractbit_exprtto_extractbit_expr (exprt &expr)
 Cast a generic exprt to an extractbit_exprt. More...
 
const extractbits_exprtto_extractbits_expr (const exprt &expr)
 Cast a generic exprt to an extractbits_exprt. More...
 
extractbits_exprtto_extractbits_expr (exprt &expr)
 Cast a generic exprt to an extractbits_exprt. More...
 
const address_of_exprtto_address_of_expr (const exprt &expr)
 Cast a generic exprt to an address_of_exprt. More...
 
address_of_exprtto_address_of_expr (exprt &expr)
 Cast a generic exprt to an address_of_exprt. More...
 
const not_exprtto_not_expr (const exprt &expr)
 Cast a generic exprt to an not_exprt. More...
 
not_exprtto_not_expr (exprt &expr)
 Cast a generic exprt to an not_exprt. More...
 
const dereference_exprtto_dereference_expr (const exprt &expr)
 Cast a generic exprt to a dereference_exprt. More...
 
dereference_exprtto_dereference_expr (exprt &expr)
 Cast a generic exprt to a dereference_exprt. More...
 
const if_exprtto_if_expr (const exprt &expr)
 Cast a generic exprt to an if_exprt. More...
 
if_exprtto_if_expr (exprt &expr)
 Cast a generic exprt to an if_exprt. More...
 
const with_exprtto_with_expr (const exprt &expr)
 Cast a generic exprt to a with_exprt. More...
 
with_exprtto_with_expr (exprt &expr)
 Cast a generic exprt to a with_exprt. More...
 
const index_designatortto_index_designator (const exprt &expr)
 Cast a generic exprt to an index_designatort. More...
 
index_designatortto_index_designator (exprt &expr)
 Cast a generic exprt to an index_designatort. More...
 
const member_designatortto_member_designator (const exprt &expr)
 Cast a generic exprt to an member_designatort. More...
 
member_designatortto_member_designator (exprt &expr)
 Cast a generic exprt to an member_designatort. More...
 
const update_exprtto_update_expr (const exprt &expr)
 Cast a generic exprt to an update_exprt. More...
 
update_exprtto_update_expr (exprt &expr)
 Cast a generic exprt to an update_exprt. More...
 
const member_exprtto_member_expr (const exprt &expr)
 Cast a generic exprt to a member_exprt. More...
 
member_exprtto_member_expr (exprt &expr)
 Cast a generic exprt to a member_exprt. More...
 
const isnan_exprtto_isnan_expr (const exprt &expr)
 Cast a generic exprt to a isnan_exprt. More...
 
isnan_exprtto_isnan_expr (exprt &expr)
 Cast a generic exprt to a isnan_exprt. More...
 
const isinf_exprtto_isinf_expr (const exprt &expr)
 Cast a generic exprt to a isinf_exprt. More...
 
isinf_exprtto_isinf_expr (exprt &expr)
 Cast a generic exprt to a isinf_exprt. More...
 
const isfinite_exprtto_isfinite_expr (const exprt &expr)
 Cast a generic exprt to a isfinite_exprt. More...
 
isfinite_exprtto_isfinite_expr (exprt &expr)
 Cast a generic exprt to a isfinite_exprt. More...
 
const isnormal_exprtto_isnormal_expr (const exprt &expr)
 Cast a generic exprt to a isnormal_exprt. More...
 
isnormal_exprtto_isnormal_expr (exprt &expr)
 Cast a generic exprt to a isnormal_exprt. More...
 
const ieee_float_equal_exprtto_ieee_float_equal_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_equal_exprt. More...
 
ieee_float_equal_exprtto_ieee_float_equal_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_equal_exprt. More...
 
const ieee_float_notequal_exprtto_ieee_float_notequal_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_notequal_exprt. More...
 
ieee_float_notequal_exprtto_ieee_float_notequal_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_notequal_exprt. More...
 
const ieee_float_op_exprtto_ieee_float_op_expr (const exprt &expr)
 Cast a generic exprt to an ieee_float_op_exprt. More...
 
ieee_float_op_exprtto_ieee_float_op_expr (exprt &expr)
 Cast a generic exprt to an ieee_float_op_exprt. More...
 
const constant_exprtto_constant_expr (const exprt &expr)
 Cast a generic exprt to a constant_exprt. More...
 
constant_exprtto_constant_expr (exprt &expr)
 Cast a generic exprt to a constant_exprt. More...
 
const function_application_exprtto_function_application_expr (const exprt &expr)
 Cast a generic exprt to a function_application_exprt. More...
 
function_application_exprtto_function_application_expr (exprt &expr)
 Cast a generic exprt to a function_application_exprt. More...
 
const concatenation_exprtto_concatenation_expr (const exprt &expr)
 Cast a generic exprt to a concatenation_exprt. More...
 
concatenation_exprtto_concatenation_expr (exprt &expr)
 Cast a generic exprt to a concatenation_exprt. More...
 
const let_exprtto_let_expr (const exprt &expr)
 Cast a generic exprt to a let_exprt. More...
 
let_exprtto_let_expr (exprt &expr)
 Cast a generic exprt to a let_exprt. More...
 

Detailed Description

Conversion to subclasses of exprt

Function Documentation

◆ to_abs_expr() [1/2]

const abs_exprt& to_abs_expr ( const exprt expr)
inline

Cast a generic exprt to a abs_exprt.

This is an unchecked conversion. expr must be known to be abs_exprt.

Parameters
exprSource expression
Returns
Object of type abs_exprt

Definition at line 323 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by float_bvt::convert().

◆ to_abs_expr() [2/2]

abs_exprt& to_abs_expr ( exprt expr)
inline

Cast a generic exprt to a abs_exprt.

This is an unchecked conversion. expr must be known to be abs_exprt.

Parameters
exprSource expression
Returns
Object of type abs_exprt

Definition at line 335 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_address_of_expr() [1/2]

const address_of_exprt& to_address_of_expr ( const exprt expr)
inline

◆ to_address_of_expr() [2/2]

address_of_exprt& to_address_of_expr ( exprt expr)
inline

Cast a generic exprt to an address_of_exprt.

This is an unchecked conversion. expr must be known to be address_of_exprt.

Parameters
exprSource expression
Returns
Object of type address_of_exprt

Definition at line 2639 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_and_expr() [1/2]

const and_exprt& to_and_expr ( const exprt expr)
inline

Cast a generic exprt to a and_exprt.

This is an unchecked conversion. expr must be known to be and_exprt.

Parameters
exprSource expression
Returns
Object of type and_exprt

Definition at line 1903 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_and_expr() [2/2]

and_exprt& to_and_expr ( exprt expr)
inline

Cast a generic exprt to a and_exprt.

This is an unchecked conversion. expr must be known to be and_exprt.

Parameters
exprSource expression
Returns
Object of type and_exprt

Definition at line 1915 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_array_expr() [1/2]

const array_exprt& to_array_expr ( const exprt expr)
inline

Cast a generic exprt to an array_exprt.

This is an unchecked conversion. expr must be known to be array_exprt.

Parameters
exprSource expression
Returns
Object of type array_exprt

Definition at line 1332 of file std_expr.h.

References irept::id(), and PRECONDITION.

Referenced by string_abstractiont::build(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_expr(), and rw_range_sett::get_objects_rec().

◆ to_array_expr() [2/2]

array_exprt& to_array_expr ( exprt expr)
inline

Cast a generic exprt to an array_exprt.

This is an unchecked conversion. expr must be known to be array_exprt.

Parameters
exprSource expression
Returns
Object of type array_exprt

Definition at line 1341 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_array_of_expr() [1/2]

const array_of_exprt& to_array_of_expr ( const exprt expr)
inline

Cast a generic exprt to an array_of_exprt.

This is an unchecked conversion. expr must be known to be array_of_exprt.

Parameters
exprSource expression
Returns
Object of type array_of_exprt

Definition at line 1286 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by arrayst::add_array_constraints(), boolbvt::convert_bitvector(), and path_symext::propagate().

◆ to_array_of_expr() [2/2]

array_of_exprt& to_array_of_expr ( exprt expr)
inline

Cast a generic exprt to an array_of_exprt.

This is an unchecked conversion. expr must be known to be array_of_exprt.

Parameters
exprSource expression
Returns
Object of type array_of_exprt

Definition at line 1298 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_binary_expr() [1/2]

const binary_exprt& to_binary_expr ( const exprt expr)
inline

Cast a generic exprt to a binary_exprt.

This is an unchecked conversion. expr must be known to be binary_exprt.

Parameters
exprSource expression
Returns
Object of type binary_exprt

Definition at line 524 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

Referenced by boolbvt::convert_bitvector().

◆ to_binary_expr() [2/2]

binary_exprt& to_binary_expr ( exprt expr)
inline

Cast a generic exprt to a binary_exprt.

This is an unchecked conversion. expr must be known to be binary_exprt.

Parameters
exprSource expression
Returns
Object of type binary_exprt

Definition at line 535 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

◆ to_binary_relation_expr() [1/2]

const binary_relation_exprt& to_binary_relation_expr ( const exprt expr)
inline

Cast a generic exprt to a binary_relation_exprt.

This is an unchecked conversion. expr must be known to be binary_relation_exprt.

Parameters
exprSource expression
Returns
Object of type binary_relation_exprt

Definition at line 619 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

Referenced by boolbvt::convert_rest(), and c_typecheck_baset::typecheck_expr_main().

◆ to_binary_relation_expr() [2/2]

binary_relation_exprt& to_binary_relation_expr ( exprt expr)
inline

Cast a generic exprt to a binary_relation_exprt.

This is an unchecked conversion. expr must be known to be binary_relation_exprt.

Parameters
exprSource expression
Returns
Object of type binary_relation_exprt

Definition at line 630 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

◆ to_bitand_expr() [1/2]

const bitand_exprt& to_bitand_expr ( const exprt expr)
inline

Cast a generic exprt to a bitand_exprt.

This is an unchecked conversion. expr must be known to be bitand_exprt.

Parameters
exprSource expression
Returns
Object of type bitand_exprt

Definition at line 2204 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitand_expr() [2/2]

bitand_exprt& to_bitand_expr ( exprt expr)
inline

Cast a generic exprt to a bitand_exprt.

This is an unchecked conversion. expr must be known to be bitand_exprt.

Parameters
exprSource expression
Returns
Object of type bitand_exprt

Definition at line 2216 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitnot_expr() [1/2]

const bitnot_exprt& to_bitnot_expr ( const exprt expr)
inline

Cast a generic exprt to a bitnot_exprt.

This is an unchecked conversion. expr must be known to be bitnot_exprt.

Parameters
exprSource expression
Returns
Object of type bitnot_exprt

Definition at line 2065 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitnot_expr() [2/2]

bitnot_exprt& to_bitnot_expr ( exprt expr)
inline

Cast a generic exprt to a bitnot_exprt.

This is an unchecked conversion. expr must be known to be bitnot_exprt.

Parameters
exprSource expression
Returns
Object of type bitnot_exprt

Definition at line 2076 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitor_expr() [1/2]

const bitor_exprt& to_bitor_expr ( const exprt expr)
inline

Cast a generic exprt to a bitor_exprt.

This is an unchecked conversion. expr must be known to be bitor_exprt.

Parameters
exprSource expression
Returns
Object of type bitor_exprt

Definition at line 2111 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitor_expr() [2/2]

bitor_exprt& to_bitor_expr ( exprt expr)
inline

Cast a generic exprt to a bitor_exprt.

This is an unchecked conversion. expr must be known to be bitor_exprt.

Parameters
exprSource expression
Returns
Object of type bitor_exprt

Definition at line 2123 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitxor_expr() [1/2]

const bitxor_exprt& to_bitxor_expr ( const exprt expr)
inline

Cast a generic exprt to a bitxor_exprt.

This is an unchecked conversion. expr must be known to be bitxor_exprt.

Parameters
exprSource expression
Returns
Object of type bitxor_exprt

Definition at line 2157 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_bitxor_expr() [2/2]

bitxor_exprt& to_bitxor_expr ( exprt expr)
inline

Cast a generic exprt to a bitxor_exprt.

This is an unchecked conversion. expr must be known to be bitxor_exprt.

Parameters
exprSource expression
Returns
Object of type bitxor_exprt

Definition at line 2169 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_complex_expr() [1/2]

const complex_exprt& to_complex_expr ( const exprt expr)
inline

Cast a generic exprt to a complex_exprt.

This is an unchecked conversion. expr must be known to be complex_exprt.

Parameters
exprSource expression
Returns
Object of type complex_exprt

Definition at line 1553 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_complex_expr() [2/2]

complex_exprt& to_complex_expr ( exprt expr)
inline

Cast a generic exprt to a complex_exprt.

This is an unchecked conversion. expr must be known to be complex_exprt.

Parameters
exprSource expression
Returns
Object of type complex_exprt

Definition at line 1565 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_concatenation_expr() [1/2]

const concatenation_exprt& to_concatenation_expr ( const exprt expr)
inline

Cast a generic exprt to a concatenation_exprt.

This is an unchecked conversion. expr must be known to be concatenation_exprt.

Parameters
exprSource expression
Returns
Object of type concatenation_exprt

Definition at line 3885 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_concatenation_expr() [2/2]

concatenation_exprt& to_concatenation_expr ( exprt expr)
inline

Cast a generic exprt to a concatenation_exprt.

This is an unchecked conversion. expr must be known to be concatenation_exprt.

Parameters
exprSource expression
Returns
Object of type concatenation_exprt

Definition at line 3897 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_constant_expr() [1/2]

const constant_exprt& to_constant_expr ( const exprt expr)
inline

Cast a generic exprt to a constant_exprt.

This is an unchecked conversion. expr must be known to be constant_exprt.

Parameters
exprSource expression
Returns
Object of type constant_exprt

Definition at line 3725 of file std_expr.h.

References irept::id(), and PRECONDITION.

Referenced by interval_domaint::assume_rec(), build_ssa_identifier_rec(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::convert_assign_varargs(), boolbvt::convert_bitvector(), expr2ct::convert_constant(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), smt2_convt::convert_rounding_mode_FPA(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), simplify_exprt::eliminate_common_addends(), custom_bitvector_domaint::eval(), interpretert::evaluate(), simplify_exprt::expr2bits(), acceleration_utilst::extract_polynomial(), polynomial_acceleratort::fit_const(), polynomialt::from_expr(), dynamic_object_exprt::get_instance(), goto_convertt::get_string_constant(), is_dereference_integer_object(), exprt::is_one(), is_store_to_slot(), exprt::is_zero(), json(), unsignedbv_typet::largest_expr(), signedbv_typet::largest_expr(), exprt::mul(), exprt::negate(), format_constantt::operator()(), smt2_convt::parse_struct(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_div(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), unsignedbv_typet::smallest_expr(), signedbv_typet::smallest_expr(), string_refinementt::string_of_array(), exprt::sum(), string_refinementt::sum_over_map(), to_integer(), custom_bitvector_domaint::transform(), remove_const_function_pointerst::try_resolve_index_value(), c_typecheck_baset::typecheck_expr_trinary(), unsigned_from_ns(), java_bytecode_convert_methodt::variable(), xml(), unsignedbv_typet::zero_expr(), and signedbv_typet::zero_expr().

◆ to_constant_expr() [2/2]

constant_exprt& to_constant_expr ( exprt expr)
inline

Cast a generic exprt to a constant_exprt.

This is an unchecked conversion. expr must be known to be constant_exprt.

Parameters
exprSource expression
Returns
Object of type constant_exprt

Definition at line 3734 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_dereference_expr() [1/2]

◆ to_dereference_expr() [2/2]

dereference_exprt& to_dereference_expr ( exprt expr)
inline

Cast a generic exprt to a dereference_exprt.

This is an unchecked conversion. expr must be known to be dereference_exprt.

Parameters
exprSource expression
Returns
Object of type dereference_exprt

Definition at line 2760 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_div_expr() [1/2]

const div_exprt& to_div_expr ( const exprt expr)
inline

Cast a generic exprt to a div_exprt.

This is an unchecked conversion. expr must be known to be div_exprt.

Parameters
exprSource expression
Returns
Object of type div_exprt

Definition at line 879 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), and smt2_convt::convert_expr().

◆ to_div_expr() [2/2]

div_exprt& to_div_expr ( exprt expr)
inline

Cast a generic exprt to a div_exprt.

This is an unchecked conversion. expr must be known to be div_exprt.

Parameters
exprSource expression
Returns
Object of type div_exprt

Definition at line 891 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_dynamic_object_expr() [1/2]

◆ to_dynamic_object_expr() [2/2]

dynamic_object_exprt& to_dynamic_object_expr ( exprt expr)
inline

Cast a generic exprt to a dynamic_object_exprt.

This is an unchecked conversion. expr must be known to be dynamic_object_exprt.

Parameters
exprSource expression
Returns
Object of type dynamic_object_exprt

Definition at line 1714 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_equal_expr() [1/2]

const equal_exprt& to_equal_expr ( const exprt expr)
inline

Cast a generic exprt to an equal_exprt.

This is an unchecked conversion. expr must be known to be equal_exprt.

Parameters
exprSource expression
Returns
Object of type equal_exprt

Definition at line 1105 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by boolbvt::convert_equality(), goto_program2codet::convert_goto_switch(), boolbvt::convert_rest(), bdd_exprt::from_expr_rec(), goto_program2codet::get_cases(), boolbvt::set_to(), prop_conv_solvert::set_to(), and smt2_convt::set_to().

◆ to_equal_expr() [2/2]

equal_exprt& to_equal_expr ( exprt expr)
inline

Cast a generic exprt to an equal_exprt.

This is an unchecked conversion. expr must be known to be equal_exprt.

Parameters
exprSource expression
Returns
Object of type equal_exprt

Definition at line 1115 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_extractbit_expr() [1/2]

const extractbit_exprt& to_extractbit_expr ( const exprt expr)
inline

Cast a generic exprt to an extractbit_exprt.

This is an unchecked conversion. expr must be known to be extractbit_exprt.

Parameters
exprSource expression
Returns
Object of type extractbit_exprt

Definition at line 2482 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by boolbvt::convert_rest().

◆ to_extractbit_expr() [2/2]

extractbit_exprt& to_extractbit_expr ( exprt expr)
inline

Cast a generic exprt to an extractbit_exprt.

This is an unchecked conversion. expr must be known to be extractbit_exprt.

Parameters
exprSource expression
Returns
Object of type extractbit_exprt

Definition at line 2494 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_extractbits_expr() [1/2]

const extractbits_exprt& to_extractbits_expr ( const exprt expr)
inline

Cast a generic exprt to an extractbits_exprt.

This is an unchecked conversion. expr must be known to be extractbits_exprt.

Parameters
exprSource expression
Returns
Object of type extractbits_exprt

Definition at line 2570 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by boolbvt::convert_bitvector().

◆ to_extractbits_expr() [2/2]

extractbits_exprt& to_extractbits_expr ( exprt expr)
inline

Cast a generic exprt to an extractbits_exprt.

This is an unchecked conversion. expr must be known to be extractbits_exprt.

Parameters
exprSource expression
Returns
Object of type extractbits_exprt

Definition at line 2582 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_factorial_expr()

factorial_power_exprt& to_factorial_expr ( exprt expr)
inline

Cast a generic exprt to a factorial_power_exprt.

This is an unchecked conversion. expr must be known to be factorial_power_exprt.

Parameters
exprSource expression
Returns
Object of type factorial_power_exprt

Definition at line 1071 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_factorial_power_expr()

const factorial_power_exprt& to_factorial_power_expr ( const exprt expr)
inline

Cast a generic exprt to a factorial_power_exprt.

This is an unchecked conversion. expr must be known to be factorial_power_exprt.

Parameters
exprSource expression
Returns
Object of type factorial_power_exprt

Definition at line 1059 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_floatbv_typecast_expr() [1/2]

const floatbv_typecast_exprt& to_floatbv_typecast_expr ( const exprt expr)
inline

Cast a generic exprt to a floatbv_typecast_exprt.

This is an unchecked conversion. expr must be known to be floatbv_typecast_exprt.

Parameters
exprSource expression
Returns
Object of type floatbv_typecast_exprt

Definition at line 1829 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by boolbvt::convert_bitvector(), and smt2_convt::convert_expr().

◆ to_floatbv_typecast_expr() [2/2]

floatbv_typecast_exprt& to_floatbv_typecast_expr ( exprt expr)
inline

Cast a generic exprt to a floatbv_typecast_exprt.

This is an unchecked conversion. expr must be known to be floatbv_typecast_exprt.

Parameters
exprSource expression
Returns
Object of type floatbv_typecast_exprt

Definition at line 1841 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_function_application_expr() [1/2]

const function_application_exprt& to_function_application_expr ( const exprt expr)
inline

Cast a generic exprt to a function_application_exprt.

This is an unchecked conversion. expr must be known to be function_application_exprt.

Parameters
exprSource expression
Returns
Object of type function_application_exprt

Definition at line 3826 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by string_constraint_generatort::add_axioms_for_string_expr(), boolbvt::convert_bitvector(), string_refinementt::convert_rest(), and expr2ct::convert_with_precedence().

◆ to_function_application_expr() [2/2]

function_application_exprt& to_function_application_expr ( exprt expr)
inline

Cast a generic exprt to a function_application_exprt.

This is an unchecked conversion. expr must be known to be function_application_exprt.

Parameters
exprSource expression
Returns
Object of type function_application_exprt

Definition at line 3839 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_ieee_float_equal_expr() [1/2]

const ieee_float_equal_exprt& to_ieee_float_equal_expr ( const exprt expr)
inline

Cast a generic exprt to an ieee_float_equal_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_equal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_equal_exprt

Definition at line 3520 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_ieee_float_equal_expr() [2/2]

ieee_float_equal_exprt& to_ieee_float_equal_expr ( exprt expr)
inline

Cast a generic exprt to an ieee_float_equal_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_equal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_equal_exprt

Definition at line 3532 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_ieee_float_notequal_expr() [1/2]

const ieee_float_notequal_exprt& to_ieee_float_notequal_expr ( const exprt expr)
inline

Cast a generic exprt to an ieee_float_notequal_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_notequal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_notequal_exprt

Definition at line 3567 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_ieee_float_notequal_expr() [2/2]

ieee_float_notequal_exprt& to_ieee_float_notequal_expr ( exprt expr)
inline

Cast a generic exprt to an ieee_float_notequal_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_notequal_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_notequal_exprt

Definition at line 3580 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_ieee_float_op_expr() [1/2]

const ieee_float_op_exprt& to_ieee_float_op_expr ( const exprt expr)
inline

Cast a generic exprt to an ieee_float_op_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_op_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_op_exprt

Definition at line 3650 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

Referenced by smt2_convt::convert_expr().

◆ to_ieee_float_op_expr() [2/2]

ieee_float_op_exprt& to_ieee_float_op_expr ( exprt expr)
inline

Cast a generic exprt to an ieee_float_op_exprt.

This is an unchecked conversion. expr must be known to be ieee_float_op_exprt.

Parameters
exprSource expression
Returns
Object of type ieee_float_op_exprt

Definition at line 3661 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

◆ to_if_expr() [1/2]

const if_exprt& to_if_expr ( const exprt expr)
inline

Cast a generic exprt to an if_exprt.

This is an unchecked conversion. expr must be known to be if_exprt.

Parameters
exprSource expression
Returns
Object of type if_exprt

Definition at line 2836 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by arrayst::add_array_constraints(), string_constraint_generatort::add_axioms_for_string_expr(), goto_symext::address_arithmetic(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), path_symext::assign_rec(), string_abstractiont::build(), build_full_lhs_rec(), goto_convertt::clean_expr(), arrayst::collect_arrays(), rw_set_functiont::compute_rec(), bv_pointerst::convert_address_of_rec(), boolbvt::convert_bitvector(), goto_convertt::convert_expression(), bv_pointerst::convert_pointer_type(), value_set_dereferencet::dereference(), dereferencet::dereference_rec(), goto_symext::dereference_rec_address_of(), goto_convertt::do_function_call(), dirtyt::find_dirty_address_of(), bdd_exprt::from_expr_rec(), path_symext::function_call_rec(), function_modifiest::get_modifies_function(), function_modifiest::get_modifies_lhs(), get_modifies_lhs(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), custom_bitvector_domaint::get_rhs(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_cleanup(), interval_domaint::havoc_rec(), path_symex_statet::instantiate_rec_address(), goto_symext::is_index_member_symbol_if(), lift_if(), nondet_volatile_lhs(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), path_symext::propagate(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_if(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_node(), simplify_exprt::simplify_node_preorder(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_typecast(), goto_symext::symex_assign_rec(), c_typecheck_baset::typecheck_expr_main(), and string_abstractiont::value_assignments().

◆ to_if_expr() [2/2]

if_exprt& to_if_expr ( exprt expr)
inline

Cast a generic exprt to an if_exprt.

This is an unchecked conversion. expr must be known to be if_exprt.

Parameters
exprSource expression
Returns
Object of type if_exprt

Definition at line 2848 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_implies_expr() [1/2]

const implies_exprt& to_implies_expr ( const exprt expr)
inline

Cast a generic exprt to a implies_exprt.

This is an unchecked conversion. expr must be known to be implies_exprt.

Parameters
exprSource expression
Returns
Object of type implies_exprt

Definition at line 1949 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by bv_refinementt::arrays_overapproximated(), and bdd_exprt::from_expr_rec().

◆ to_implies_expr() [2/2]

implies_exprt& to_implies_expr ( exprt expr)
inline

Cast a generic exprt to a implies_exprt.

This is an unchecked conversion. expr must be known to be implies_exprt.

Parameters
exprSource expression
Returns
Object of type implies_exprt

Definition at line 1959 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_index_designator() [1/2]

const index_designatort& to_index_designator ( const exprt expr)
inline

Cast a generic exprt to an index_designatort.

This is an unchecked conversion. expr must be known to be index_designatort.

Parameters
exprSource expression
Returns
Object of type index_designatort

Definition at line 2970 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by make_with_expr().

◆ to_index_designator() [2/2]

index_designatort& to_index_designator ( exprt expr)
inline

Cast a generic exprt to an index_designatort.

This is an unchecked conversion. expr must be known to be index_designatort.

Parameters
exprSource expression
Returns
Object of type index_designatort

Definition at line 2982 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_index_expr() [1/2]

const index_exprt& to_index_expr ( const exprt expr)
inline

Cast a generic exprt to an index_exprt.

This is an unchecked conversion. expr must be known to be index_exprt.

Parameters
exprSource expression
Returns
Object of type index_exprt

Definition at line 1229 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by string_abstractiont::abstract_char_assign(), ai_domain_baset::ai_simplify_lhs(), acceleration_utilst::array_assignments2polys(), path_symex_statet::array_theory(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), string_abstractiont::build_pointer(), build_ssa_identifier_rec(), goto_checkt::check_rec(), arrayst::collect_indices(), goto_symex_statet::constant_propagation_reference(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), smt1_convt::convert_with(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec(), goto_symext::dereference_rec_address_of(), dirtyt::find_dirty_address_of(), acceleration_utilst::gather_array_assignments(), smt1_convt::get(), custom_bitvector_analysist::get_bit_nr(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), path_symex_statet::is_symbol_member_index(), boolbvt::literal(), goto_convertt::needs_cleaning(), nondet_volatile_lhs(), find_index_visitort::operator()(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), pointer_arithmetict::read(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), goto_symex_statet::rename_address(), rewrite_assignment(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality_address_of(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), and remove_const_function_pointerst::try_resolve_function_call().

◆ to_index_expr() [2/2]

index_exprt& to_index_expr ( exprt expr)
inline

Cast a generic exprt to an index_exprt.

This is an unchecked conversion. expr must be known to be index_exprt.

Parameters
exprSource expression
Returns
Object of type index_exprt

Definition at line 1241 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isfinite_expr() [1/2]

const isfinite_exprt& to_isfinite_expr ( const exprt expr)
inline

Cast a generic exprt to a isfinite_exprt.

This is an unchecked conversion. expr must be known to be isfinite_exprt.

Parameters
exprSource expression
Returns
Object of type isfinite_exprt

Definition at line 3436 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isfinite_expr() [2/2]

isfinite_exprt& to_isfinite_expr ( exprt expr)
inline

Cast a generic exprt to a isfinite_exprt.

This is an unchecked conversion. expr must be known to be isfinite_exprt.

Parameters
exprSource expression
Returns
Object of type isfinite_exprt

Definition at line 3446 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isinf_expr() [1/2]

const isinf_exprt& to_isinf_expr ( const exprt expr)
inline

Cast a generic exprt to a isinf_exprt.

This is an unchecked conversion. expr must be known to be isinf_exprt.

Parameters
exprSource expression
Returns
Object of type isinf_exprt

Definition at line 3390 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isinf_expr() [2/2]

isinf_exprt& to_isinf_expr ( exprt expr)
inline

Cast a generic exprt to a isinf_exprt.

This is an unchecked conversion. expr must be known to be isinf_exprt.

Parameters
exprSource expression
Returns
Object of type isinf_exprt

Definition at line 3402 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isnan_expr() [1/2]

const isnan_exprt& to_isnan_expr ( const exprt expr)
inline

Cast a generic exprt to a isnan_exprt.

This is an unchecked conversion. expr must be known to be isnan_exprt.

Parameters
exprSource expression
Returns
Object of type isnan_exprt

Definition at line 3348 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isnan_expr() [2/2]

isnan_exprt& to_isnan_expr ( exprt expr)
inline

Cast a generic exprt to a isnan_exprt.

This is an unchecked conversion. expr must be known to be isnan_exprt.

Parameters
exprSource expression
Returns
Object of type isnan_exprt

Definition at line 3358 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isnormal_expr() [1/2]

const isnormal_exprt& to_isnormal_expr ( const exprt expr)
inline

Cast a generic exprt to a isnormal_exprt.

This is an unchecked conversion. expr must be known to be isnormal_exprt.

Parameters
exprSource expression
Returns
Object of type isnormal_exprt

Definition at line 3478 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_isnormal_expr() [2/2]

isnormal_exprt& to_isnormal_expr ( exprt expr)
inline

Cast a generic exprt to a isnormal_exprt.

This is an unchecked conversion. expr must be known to be isnormal_exprt.

Parameters
exprSource expression
Returns
Object of type isnormal_exprt

Definition at line 3488 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_let_expr() [1/2]

const let_exprt& to_let_expr ( const exprt expr)
inline

Cast a generic exprt to a let_exprt.

This is an unchecked conversion. expr must be known to be let_exprt.

Parameters
exprSource expression
Returns
Object of type let_exprt

Definition at line 3969 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by smt2_convt::convert_expr().

◆ to_let_expr() [2/2]

let_exprt& to_let_expr ( exprt expr)
inline

Cast a generic exprt to a let_exprt.

This is an unchecked conversion. expr must be known to be let_exprt.

Parameters
exprSource expression
Returns
Object of type let_exprt

Definition at line 3979 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_literal_expr() [1/2]

const literal_exprt& to_literal_expr ( const exprt expr)
inline

Cast a generic exprt to a literal_exprt.

This is an unchecked conversion. expr must be known to be literal_exprt.

Parameters
exprSource expression
Returns
Object of type literal_exprt

Definition at line 49 of file literal_expr.h.

References exprt::has_operands(), and irept::id().

Referenced by cvc_convt::convert(), smt1_convt::convert(), smt2_convt::convert(), prop_conv_solvert::convert_bool(), smt1_convt::convert_expr(), and smt2_convt::convert_expr().

◆ to_literal_expr() [2/2]

literal_exprt& to_literal_expr ( exprt expr)
inline

Cast a generic exprt to a literal_exprt.

This is an unchecked conversion. expr must be known to be literal_exprt.

Parameters
exprSource expression
Returns
Object of type literal_exprt

Definition at line 58 of file literal_expr.h.

References exprt::has_operands(), and irept::id().

◆ to_member_designator() [1/2]

const member_designatort& to_member_designator ( const exprt expr)
inline

Cast a generic exprt to an member_designatort.

This is an unchecked conversion. expr must be known to be member_designatort.

Parameters
exprSource expression
Returns
Object of type member_designatort

Definition at line 3016 of file std_expr.h.

References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.

◆ to_member_designator() [2/2]

member_designatort& to_member_designator ( exprt expr)
inline

Cast a generic exprt to an member_designatort.

This is an unchecked conversion. expr must be known to be member_designatort.

Parameters
exprSource expression
Returns
Object of type member_designatort

Definition at line 3028 of file std_expr.h.

References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.

◆ to_member_expr() [1/2]

const member_exprt& to_member_expr ( const exprt expr)
inline

Cast a generic exprt to a member_exprt.

This is an unchecked conversion. expr must be known to be member_exprt.

Parameters
exprSource expression
Returns
Object of type member_exprt

Definition at line 3302 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by arrayst::add_array_constraints(), ai_domain_baset::ai_simplify_lhs(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), path_symext::assign_rec(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), build_ssa_identifier_rec(), goto_checkt::check_rec(), arrayst::collect_arrays(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), bv_pointerst::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), graphml_witnesst::convert_assign_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), smt1_convt::convert_member(), smt2_convt::convert_member(), bv_pointerst::convert_pointer_type(), boolbvt::convert_rest(), smt1_convt::convert_with(), expr2ct::convert_with_precedence(), goto_symext::dereference_rec_address_of(), interpretert::evaluate_address(), dirtyt::find_dirty_address_of(), smt1_convt::get(), smt2_convt::get(), rw_range_sett::get_objects_address_of(), get_objects_rec(), rw_range_sett::get_objects_rec(), have_to_rewrite_union(), path_symex_statet::instantiate_rec(), path_symex_statet::instantiate_rec_address(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_constant_address_of(), goto_symext::is_index_member_symbol_if(), is_lvalue(), path_symex_statet::is_symbol_member_index(), boolbvt::literal(), nondet_volatile_lhs(), path_symext::propagate(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), goto_symex_statet::rename_address(), rewrite_assignment(), rewrite_union(), java_bytecode_convert_methodt::save_stack_entries(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_member(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), remove_const_function_pointerst::try_resolve_function_call(), and java_bytecode_typecheckt::typecheck_expr().

◆ to_member_expr() [2/2]

member_exprt& to_member_expr ( exprt expr)
inline

Cast a generic exprt to a member_exprt.

This is an unchecked conversion. expr must be known to be member_exprt.

Parameters
exprSource expression
Returns
Object of type member_exprt

Definition at line 3314 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_minus_expr() [1/2]

const minus_exprt& to_minus_expr ( const exprt expr)
inline

Cast a generic exprt to a minus_exprt.

This is an unchecked conversion. expr must be known to be minus_exprt.

Parameters
exprSource expression
Returns
Object of type minus_exprt

Definition at line 783 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by smt1_convt::convert_expr(), and smt2_convt::convert_expr().

◆ to_minus_expr() [2/2]

minus_exprt& to_minus_expr ( exprt expr)
inline

Cast a generic exprt to a minus_exprt.

This is an unchecked conversion. expr must be known to be minus_exprt.

Parameters
exprSource expression
Returns
Object of type minus_exprt

Definition at line 795 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_mod_expr() [1/2]

const mod_exprt& to_mod_expr ( const exprt expr)
inline

Cast a generic exprt to a mod_exprt.

This is an unchecked conversion. expr must be known to be mod_exprt.

Parameters
exprSource expression
Returns
Object of type mod_exprt

Definition at line 927 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), and smt2_convt::convert_expr().

◆ to_mod_expr() [2/2]

mod_exprt& to_mod_expr ( exprt expr)
inline

Cast a generic exprt to a mod_exprt.

This is an unchecked conversion. expr must be known to be mod_exprt.

Parameters
exprSource expression
Returns
Object of type mod_exprt

Definition at line 937 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_mult_expr() [1/2]

const mult_exprt& to_mult_expr ( const exprt expr)
inline

Cast a generic exprt to a mult_exprt.

This is an unchecked conversion. expr must be known to be mult_exprt.

Parameters
exprSource expression
Returns
Object of type mult_exprt

Definition at line 831 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by smt1_convt::convert_expr(), and smt2_convt::convert_expr().

◆ to_mult_expr() [2/2]

mult_exprt& to_mult_expr ( exprt expr)
inline

Cast a generic exprt to a mult_exprt.

This is an unchecked conversion. expr must be known to be mult_exprt.

Parameters
exprSource expression
Returns
Object of type mult_exprt

Definition at line 843 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_multi_ary_expr() [1/2]

const multi_ary_exprt& to_multi_ary_expr ( const exprt expr)
inline

Cast a generic exprt to a multi_ary_exprt.

This is an unchecked conversion. expr must be known to be multi_ary_exprt.

Parameters
exprSource expression
Returns
Object of type multi_ary_exprt

Definition at line 687 of file std_expr.h.

◆ to_multi_ary_expr() [2/2]

multi_ary_exprt& to_multi_ary_expr ( exprt expr)
inline

Cast a generic exprt to a multi_ary_exprt.

This is an unchecked conversion. expr must be known to be multi_ary_exprt.

Parameters
exprSource expression
Returns
Object of type multi_ary_exprt

Definition at line 695 of file std_expr.h.

◆ to_not_expr() [1/2]

const not_exprt& to_not_expr ( const exprt expr)
inline

Cast a generic exprt to an not_exprt.

This is an unchecked conversion. expr must be known to be not_exprt.

Parameters
exprSource expression
Returns
Object of type not_exprt

Definition at line 2682 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by interval_domaint::assume_rec(), collect_mcdc_controlling_rec(), boolbvt::convert_bitvector(), and bdd_exprt::from_expr_rec().

◆ to_not_expr() [2/2]

not_exprt& to_not_expr ( exprt expr)
inline

Cast a generic exprt to an not_exprt.

This is an unchecked conversion. expr must be known to be not_exprt.

Parameters
exprSource expression
Returns
Object of type not_exprt

Definition at line 2692 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_notequal_expr() [1/2]

const notequal_exprt& to_notequal_expr ( const exprt expr)
inline

Cast a generic exprt to an notequal_exprt.

This is an unchecked conversion. expr must be known to be notequal_exprt.

Parameters
exprSource expression
Returns
Object of type notequal_exprt

Definition at line 1147 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_notequal_expr() [2/2]

notequal_exprt& to_notequal_expr ( exprt expr)
inline

Cast a generic exprt to an notequal_exprt.

This is an unchecked conversion. expr must be known to be notequal_exprt.

Parameters
exprSource expression
Returns
Object of type notequal_exprt

Definition at line 1159 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_object_descriptor_expr() [1/2]

const object_descriptor_exprt& to_object_descriptor_expr ( const exprt expr)
inline

Cast a generic exprt to an object_descriptor_exprt.

This is an unchecked conversion. expr must be known to be object_descriptor_exprt.

Parameters
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 1634 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by value_set_dereferencet::build_reference_to(), flow_insensitive_analysis_baset::do_function_call_rec(), and static_analysis_baset::do_function_call_rec().

◆ to_object_descriptor_expr() [2/2]

object_descriptor_exprt& to_object_descriptor_expr ( exprt expr)
inline

Cast a generic exprt to an object_descriptor_exprt.

This is an unchecked conversion. expr must be known to be object_descriptor_exprt.

Parameters
exprSource expression
Returns
Object of type object_descriptor_exprt

Definition at line 1647 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_or_expr() [1/2]

const or_exprt& to_or_expr ( const exprt expr)
inline

Cast a generic exprt to a or_exprt.

This is an unchecked conversion. expr must be known to be or_exprt.

Parameters
exprSource expression
Returns
Object of type or_exprt

Definition at line 2019 of file std_expr.h.

References irept::id(), and PRECONDITION.

Referenced by bv_refinementt::arrays_overapproximated().

◆ to_or_expr() [2/2]

or_exprt& to_or_expr ( exprt expr)
inline

Cast a generic exprt to a or_exprt.

This is an unchecked conversion. expr must be known to be or_exprt.

Parameters
exprSource expression
Returns
Object of type or_exprt

Definition at line 2031 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_plus_expr() [1/2]

const plus_exprt& to_plus_expr ( const exprt expr)
inline

Cast a generic exprt to a plus_exprt.

This is an unchecked conversion. expr must be known to be plus_exprt.

Parameters
exprSource expression
Returns
Object of type plus_exprt

Definition at line 735 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by smt1_convt::convert_expr(), smt2_convt::convert_expr(), and smt2_convt::convert_plus().

◆ to_plus_expr() [2/2]

plus_exprt& to_plus_expr ( exprt expr)
inline

Cast a generic exprt to a plus_exprt.

This is an unchecked conversion. expr must be known to be plus_exprt.

Parameters
exprSource expression
Returns
Object of type plus_exprt

Definition at line 747 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_power_expr() [1/2]

const power_exprt& to_power_expr ( const exprt expr)
inline

Cast a generic exprt to a power_exprt.

This is an unchecked conversion. expr must be known to be power_exprt.

Parameters
exprSource expression
Returns
Object of type power_exprt

Definition at line 1015 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_power_expr() [2/2]

power_exprt& to_power_expr ( exprt expr)
inline

Cast a generic exprt to a power_exprt.

This is an unchecked conversion. expr must be known to be power_exprt.

Parameters
exprSource expression
Returns
Object of type power_exprt

Definition at line 1025 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_rem_expr() [1/2]

const rem_exprt& to_rem_expr ( const exprt expr)
inline

Cast a generic exprt to a rem_exprt.

This is an unchecked conversion. expr must be known to be rem_exprt.

Parameters
exprSource expression
Returns
Object of type rem_exprt

Definition at line 971 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_rem_expr() [2/2]

rem_exprt& to_rem_expr ( exprt expr)
inline

Cast a generic exprt to a rem_exprt.

This is an unchecked conversion. expr must be known to be rem_exprt.

Parameters
exprSource expression
Returns
Object of type rem_exprt

Definition at line 981 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_replication_expr() [1/2]

const replication_exprt& to_replication_expr ( const exprt expr)
inline

Cast a generic exprt to a replication_exprt.

This is an unchecked conversion. expr must be known to be replication_exprt.

Parameters
exprSource expression
Returns
Object of type replication_exprt

Definition at line 2411 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by boolbvt::convert_bitvector().

◆ to_replication_expr() [2/2]

replication_exprt& to_replication_expr ( exprt expr)
inline

Cast a generic exprt to a replication_exprt.

This is an unchecked conversion. expr must be known to be replication_exprt.

Parameters
exprSource expression
Returns
Object of type replication_exprt

Definition at line 2423 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_shift_expr() [1/2]

const shift_exprt& to_shift_expr ( const exprt expr)
inline

Cast a generic exprt to a shift_exprt.

This is an unchecked conversion. expr must be known to be shift_exprt.

Parameters
exprSource expression
Returns
Object of type shift_exprt

Definition at line 2280 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

Referenced by goto_checkt::check_rec(), boolbvt::convert_bitvector(), bv_pointerst::convert_pointer_type(), rw_range_sett::get_objects_rec(), and c_typecheck_baset::typecheck_expr_main().

◆ to_shift_expr() [2/2]

shift_exprt& to_shift_expr ( exprt expr)
inline

Cast a generic exprt to a shift_exprt.

This is an unchecked conversion. expr must be known to be shift_exprt.

Parameters
exprSource expression
Returns
Object of type shift_exprt

Definition at line 2291 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

◆ to_ssa_expr() [1/2]

◆ to_ssa_expr() [2/2]

ssa_exprt& to_ssa_expr ( exprt expr)
inline

Cast a generic exprt to an ssa_exprt.

This is an unchecked conversion. expr must be known to be ssa_exprt.

Parameters
exprSource expression
Returns
Object of type ssa_exprt

Definition at line 161 of file ssa_expr.h.

References irept::get_bool(), exprt::has_operands(), and irept::id().

◆ to_struct_expr() [1/2]

const struct_exprt& to_struct_expr ( const exprt expr)
inline

Cast a generic exprt to a struct_exprt.

This is an unchecked conversion. expr must be known to be struct_exprt.

Parameters
exprSource expression
Returns
Object of type struct_exprt

Definition at line 1487 of file std_expr.h.

References irept::id(), and PRECONDITION.

Referenced by boolbvt::convert_bitvector(), smt2_convt::convert_expr(), goto_convertt::do_java_new(), rw_range_sett::get_objects_rec(), set_class_identifier(), and remove_const_function_pointerst::try_resolve_member().

◆ to_struct_expr() [2/2]

struct_exprt& to_struct_expr ( exprt expr)
inline

Cast a generic exprt to a struct_exprt.

This is an unchecked conversion. expr must be known to be struct_exprt.

Parameters
exprSource expression
Returns
Object of type struct_exprt

Definition at line 1496 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_symbol_expr() [1/2]

const symbol_exprt& to_symbol_expr ( const exprt expr)
inline

Cast a generic exprt to a symbol_exprt.

This is an unchecked conversion. expr must be known to be symbol_exprt.

Parameters
exprSource expression
Returns
Object of type symbol_exprt

Definition at line 202 of file std_expr.h.

References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.

Referenced by call_grapht::add(), const_function_pointer_propagationt::arg_stackt::add_args(), uninitializedt::add_assertions(), string_constraint_generatort::add_axioms_for_function_application(), string_constraint_generatort::add_axioms_for_string_expr(), string_constraint_generatort::add_axioms_from_literal(), aliasing(), value_sett::apply_code(), code_contractst::apply_contract(), uninitialized_domaint::assign(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), global_may_alias_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_aliases(), escape_domaint::assign_lhs_cleanup(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), string_refinementt::boolbv_set_equality_to_true(), boolbvt::boolbv_set_equality_to_true(), localst::build(), local_may_aliast::build(), string_abstractiont::build(), build_ssa_identifier_rec(), escape_domaint::check_lhs(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), concurrency_instrumentationt::collect(), goto_checkt::collect_allocations(), compute_address_taken_functions(), cfg_baset< cfg_nodet >::compute_edges_function_call(), compute_functions(), rw_set_functiont::compute_rec(), boolbvt::convert_bitvector(), prop_conv_solvert::convert_bool(), jsil_convertt::convert_code(), expr2ct::convert_code_decl(), goto_program2codet::convert_decl(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv(), boolbvt::convert_index(), java_bytecode_convert_methodt::convert_instructions(), bv_pointerst::convert_pointer_type(), string_refinementt::convert_symbol(), string_instrumentationt::do_function_call(), goto_convertt::do_function_call(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), c_typecheck_baset::do_special_functions(), const_function_pointer_propagationt::dup_caller_and_inline_callee(), goto_inlinet::expand_function_call(), fence_all_shared_aegt::fence_all_shared_aeg_explore(), dirtyt::find_dirty_address_of(), find_symbols(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), polynomialt::from_expr(), path_symext::function_call_rec(), gather_needed_globals(), gather_symbol_live_ranges(), smt1_convt::get(), smt2_convt::get(), prop_conv_solvert::get_bool(), goto_inlinet::get_call(), remove_virtual_functionst::get_child_functions_rec(), goto_convertt::get_constant(), goto_programt::get_decl_identifiers(), escape_domaint::get_function(), remove_virtual_functionst::get_functions(), code_declt::get_identifier(), code_deadt::get_identifier(), function_modifiest::get_modifies_function(), ssa_exprt::get_object_name(), get_objects_rec(), rw_range_sett::get_objects_rec(), get_old_va_symbol(), local_bitvector_analysist::get_rec(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), global_may_alias_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_aliases_address_of(), escape_domaint::get_rhs_cleanup(), symex_slicet::get_symbols(), uninitializedt::get_tracking(), value_sett::get_value_set_rec(), goto_checkt::goto_check(), goto_partial_inline(), cpp_typecheck_resolvet::guess_function_template_args(), symex_dereference_statet::has_failed_symbol(), interval_domaint::havoc_rec(), implicit(), taint_analysist::instrument(), concurrency_instrumentationt::instrument(), instrument_cover_goals(), remove_exceptionst::instrument_function_call(), goto_checkt::invalidate(), constant_propagator_domaint::valuest::is_array_constant(), constant_propagator_domaint::valuest::is_constant(), pointer_logict::is_dynamic_object(), acceleratet::is_underapproximate(), link_functions(), list_calls_and_arguments(), prop_conv_solvert::literal(), mm_io(), nondet_static(), custom_bitvector_domaint::object2id(), full_slicert::operator()(), check_call_sequencet::operator()(), const_function_pointer_propagationt::propagate(), path_symex_statet::read_symbol_member_index(), _rw_set_loct::read_write_rec(), graphml_witnesst::remove_l0_l1(), rename_symbolt::rename(), goto_symex_statet::rename(), replace_async(), character_refine_preprocesst::replace_character_call(), remove_returnst::restore_returns(), goto_symext::rewrite_quantifiers(), java_bytecode_convert_methodt::save_stack_entries(), prop_conv_solvert::set_equality_to_true(), string_constraint_generatort::set_string_symbol_equal_to_expr(), smt2_convt::set_to(), show_call_sequences(), cpp_typecheck_resolvet::show_identifiers(), simplify_exprt::simplify_dynamic_object(), slice_global_inits(), acceleration_utilst::stash_variables(), polynomial_acceleratort::stash_variables(), polynomialt::substitute(), goto_symext::symex_assign(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_function_call_symbol(), thread_exit_instrumentation(), jsil_declarationt::to_symbol(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), escape_domaint::transform(), rd_range_domaint::transform_dead(), rd_range_domaint::transform_function_call(), java_bytecode_typecheckt::typecheck_expr(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_symbol(), jsil_typecheckt::typecheck_function_call(), c_typecheck_baset::typecheck_side_effect_function_call(), undefined_function_abort_path(), remove_returnst::undo_function_calls(), string_constraintt::univ_var(), jsil_typecheckt::update_expr_type(), value_set_dereferencet::valid_check(), instrumentert::cfg_visitort::visit_cfg_function_call(), shared_bufferst::cfg_visitort::weak_memory(), and yyjsilparse().

◆ to_symbol_expr() [2/2]

symbol_exprt& to_symbol_expr ( exprt expr)
inline

Cast a generic exprt to a symbol_exprt.

This is an unchecked conversion. expr must be known to be symbol_exprt.

Parameters
exprSource expression
Returns
Object of type symbol_exprt

Definition at line 212 of file std_expr.h.

References DATA_INVARIANT, exprt::has_operands(), irept::id(), and PRECONDITION.

◆ to_trans_expr() [1/2]

const transt& to_trans_expr ( const exprt expr)
inline

Cast a generic exprt to a transt.

This is an unchecked conversion. expr must be known to be transt.

Parameters
exprSource expression
Returns
Object of type transt

Definition at line 59 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_trans_expr() [2/2]

transt& to_trans_expr ( exprt expr)
inline

Definition at line 71 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_typecast_expr() [1/2]

const typecast_exprt& to_typecast_expr ( const exprt expr)
inline

Cast a generic exprt to a typecast_exprt.

This is an unchecked conversion. expr must be known to be typecast_exprt.

Parameters
exprSource expression
Returns
Object of type typecast_exprt

Definition at line 1760 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by string_constraint_generatort::add_axioms_for_string_expr(), adjust_float_expressions(), custom_bitvector_analysist::aliases(), local_may_aliast::assign_lhs(), local_bitvector_analysist::assign_lhs(), path_symext::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), value_set_fivrnst::assign_rec(), value_set_fivrt::assign_rec(), interval_domaint::assume_rec(), string_refinementt::boolbv_set_equality_to_true(), string_abstractiont::build(), build_full_lhs_rec(), build_object_descriptor_rec(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), goto_symex_statet::constant_propagation(), boolbvt::convert_bitvector(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), boolbvt::convert_rest(), expr2ct::convert_with_precedence(), dereferencet::dereference_rec(), goto_symext::dereference_rec(), path_symext::function_call_rec(), smt1_convt::get(), custom_bitvector_analysist::get_bit_nr(), escape_domaint::get_function(), rw_range_sett::get_objects_address_of(), rw_range_sett::get_objects_rec(), get_old_va_symbol(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), custom_bitvector_domaint::get_rhs(), global_may_alias_domaint::get_rhs_aliases(), escape_domaint::get_rhs_aliases(), escape_domaint::get_rhs_cleanup(), get_symbol(), have_to_adjust_float_expressions(), have_to_remove_complex(), interval_domaint::havoc_rec(), is_skip(), make_va_list(), custom_bitvector_domaint::object2id(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), path_symext::propagate(), java_bytecode_convert_methodt::save_stack_entries(), goto_program2codet::scan_for_varargs(), skip_typecast(), goto_symext::symex_assign_rec(), remove_const_function_pointerst::try_resolve_expression(), and remove_const_function_pointerst::try_resolve_function_call().

◆ to_typecast_expr() [2/2]

typecast_exprt& to_typecast_expr ( exprt expr)
inline

Cast a generic exprt to a typecast_exprt.

This is an unchecked conversion. expr must be known to be typecast_exprt.

Parameters
exprSource expression
Returns
Object of type typecast_exprt

Definition at line 1772 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_unary_expr() [1/2]

const unary_exprt& to_unary_expr ( const exprt expr)
inline

Cast a generic exprt to a unary_exprt.

This is an unchecked conversion. expr must be known to be unary_exprt.

Parameters
exprSource expression
Returns
Object of type unary_exprt

Definition at line 279 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

Referenced by boolbvt::convert_bitvector(), and boolbvt::convert_rest().

◆ to_unary_expr() [2/2]

unary_exprt& to_unary_expr ( exprt expr)
inline

Cast a generic exprt to a unary_exprt.

This is an unchecked conversion. expr must be known to be unary_exprt.

Parameters
exprSource expression
Returns
Object of type unary_exprt

Definition at line 290 of file std_expr.h.

References DATA_INVARIANT, and exprt::operands().

◆ to_unary_minus_expr() [1/2]

const unary_minus_exprt& to_unary_minus_expr ( const exprt expr)
inline

Cast a generic exprt to a unary_minus_exprt.

This is an unchecked conversion. expr must be known to be unary_minus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_minus_exprt

Definition at line 376 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by float_bvt::convert().

◆ to_unary_minus_expr() [2/2]

unary_minus_exprt& to_unary_minus_expr ( exprt expr)
inline

Cast a generic exprt to a unary_minus_exprt.

This is an unchecked conversion. expr must be known to be unary_minus_exprt.

Parameters
exprSource expression
Returns
Object of type unary_minus_exprt

Definition at line 388 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_union_expr() [1/2]

const union_exprt& to_union_expr ( const exprt expr)
inline

Cast a generic exprt to a union_exprt.

This is an unchecked conversion. expr must be known to be union_exprt.

Parameters
exprSource expression
Returns
Object of type union_exprt

Definition at line 1441 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), boolbvt::convert_bitvector(), smt2_convt::convert_expr(), simplify_exprt::expr2bits(), json(), path_symext::propagate(), rewrite_union(), simplify_exprt::simplify_member(), and xml().

◆ to_union_expr() [2/2]

union_exprt& to_union_expr ( exprt expr)
inline

Cast a generic exprt to a union_exprt.

This is an unchecked conversion. expr must be known to be union_exprt.

Parameters
exprSource expression
Returns
Object of type union_exprt

Definition at line 1453 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_update_expr() [1/2]

const update_exprt& to_update_expr ( const exprt expr)
inline

Cast a generic exprt to an update_exprt.

This is an unchecked conversion. expr must be known to be update_exprt.

Parameters
exprSource expression
Returns
Object of type update_exprt

Definition at line 3108 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by arrayst::add_array_constraints(), arrayst::collect_arrays(), simplify_exprt::simplify_member(), and simplify_exprt::simplify_update().

◆ to_update_expr() [2/2]

update_exprt& to_update_expr ( exprt expr)
inline

Cast a generic exprt to an update_exprt.

This is an unchecked conversion. expr must be known to be update_exprt.

Parameters
exprSource expression
Returns
Object of type update_exprt

Definition at line 3120 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

◆ to_vector_expr() [1/2]

const vector_exprt& to_vector_expr ( const exprt expr)
inline

Cast a generic exprt to an vector_exprt.

This is an unchecked conversion. expr must be known to be vector_exprt.

Parameters
exprSource expression
Returns
Object of type vector_exprt

Definition at line 1372 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_vector_expr() [2/2]

vector_exprt& to_vector_expr ( exprt expr)
inline

Cast a generic exprt to an vector_exprt.

This is an unchecked conversion. expr must be known to be vector_exprt.

Parameters
exprSource expression
Returns
Object of type vector_exprt

Definition at line 1381 of file std_expr.h.

References irept::id(), and PRECONDITION.

◆ to_with_expr() [1/2]

const with_exprt& to_with_expr ( const exprt expr)
inline

Cast a generic exprt to a with_exprt.

This is an unchecked conversion. expr must be known to be with_exprt.

Parameters
exprSource expression
Returns
Object of type with_exprt

Definition at line 2919 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.

Referenced by arrayst::add_array_constraints(), arrayst::collect_arrays(), smt2_convt::convert_expr(), make_with_expr(), goto_symex_statet::rename(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_member(), and smt2_convt::use_array_theory().

◆ to_with_expr() [2/2]

with_exprt& to_with_expr ( exprt expr)
inline

Cast a generic exprt to a with_exprt.

This is an unchecked conversion. expr must be known to be with_exprt.

Parameters
exprSource expression
Returns
Object of type with_exprt

Definition at line 2931 of file std_expr.h.

References DATA_INVARIANT, irept::id(), exprt::operands(), and PRECONDITION.