cprover
exprt Class Reference

Base class for all expressions. More...

#include <expr.h>

Inheritance diagram for exprt:
[legend]
Collaboration diagram for exprt:
[legend]

Public Types

typedef std::vector< exprtoperandst
 
- Public Types inherited from irept
typedef std::vector< ireptsubt
 
typedef std::map< irep_namet, ireptnamed_subt
 

Public Member Functions

 exprt ()
 
 exprt (const irep_idt &_id)
 
 exprt (const irep_idt &_id, const typet &_type)
 
typettype ()
 
const typettype () const
 
bool has_operands () const
 
operandstoperands ()
 
const operandstoperands () const
 
exprtop0 ()
 
exprtop1 ()
 
exprtop2 ()
 
exprtop3 ()
 
const exprtop0 () const
 
const exprtop1 () const
 
const exprtop2 () const
 
const exprtop3 () const
 
void reserve_operands (operandst::size_type n)
 
void move_to_operands (exprt &expr)
 
void move_to_operands (exprt &e1, exprt &e2)
 
void move_to_operands (exprt &e1, exprt &e2, exprt &e3)
 
void copy_to_operands (const exprt &expr)
 
void copy_to_operands (const exprt &e1, const exprt &e2)
 
void copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3)
 
void make_typecast (const typet &_type)
 
void make_not ()
 
void make_true ()
 
void make_false ()
 
void make_bool (bool value)
 
void negate ()
 
bool sum (const exprt &expr)
 
bool mul (const exprt &expr)
 
bool subtract (const exprt &expr)
 
bool is_constant () const
 
bool is_true () const
 
bool is_false () const
 
bool is_zero () const
 
bool is_one () const
 
bool is_boolean () const
 
const source_locationtfind_source_location () const
 
const source_locationtsource_location () const
 
source_locationtadd_source_location ()
 
exprtadd_expr (const irep_idt &name)
 
const exprtfind_expr (const irep_idt &name) const
 
void visit (class expr_visitort &visitor)
 
void visit (class const_expr_visitort &visitor) const
 
- Public Member Functions inherited from irept
bool is_nil () const
 
bool is_not_nil () const
 
 irept (const irep_idt &_id)
 
 irept ()
 
 irept (const irept &irep)
 
 irept (irept &&irep)
 
ireptoperator= (const irept &irep)
 
ireptoperator= (irept &&irep)
 
 ~irept ()
 
const irep_idtid () const
 
const std::string & id_string () const
 
void id (const irep_idt &_data)
 
const ireptfind (const irep_namet &name) const
 
ireptadd (const irep_namet &name)
 
ireptadd (const irep_namet &name, const irept &irep)
 
const std::string & get_string (const irep_namet &name) const
 
const irep_idtget (const irep_namet &name) const
 
bool get_bool (const irep_namet &name) const
 
signed int get_int (const irep_namet &name) const
 
unsigned int get_unsigned_int (const irep_namet &name) const
 
std::size_t get_size_t (const irep_namet &name) const
 
long long get_long_long (const irep_namet &name) const
 
void set (const irep_namet &name, const irep_idt &value)
 
void set (const irep_namet &name, const irept &irep)
 
void set (const irep_namet &name, const long long value)
 
void remove (const irep_namet &name)
 
void move_to_sub (irept &irep)
 
void move_to_named_sub (const irep_namet &name, irept &irep)
 
bool operator== (const irept &other) const
 
bool operator!= (const irept &other) const
 
void swap (irept &irep)
 
bool operator< (const irept &other) const
 defines ordering on the internal representation More...
 
bool ordering (const irept &other) const
 defines ordering on the internal representation More...
 
int compare (const irept &i) const
 defines ordering on the internal representation More...
 
void clear ()
 
void make_nil ()
 
subtget_sub ()
 
const subtget_sub () const
 
named_subtget_named_sub ()
 
const named_subtget_named_sub () const
 
named_subtget_comments ()
 
const named_subtget_comments () const
 
std::size_t hash () const
 
std::size_t full_hash () const
 
bool full_eq (const irept &other) const
 
std::string pretty (unsigned indent=0, unsigned max_indent=0) const
 
const dtread () const
 
dtwrite ()
 

Additional Inherited Members

- Protected Member Functions inherited from irept
void detach ()
 
- Static Protected Member Functions inherited from irept
static bool is_comment (const irep_namet &name)
 
static void remove_ref (dt *old_data)
 
static void nonrecursive_destructor (dt *old_data)
 Does the same as remove_ref, but using an explicit stack instead of recursion. More...
 
- Protected Attributes inherited from irept
dtdata
 
- Static Protected Attributes inherited from irept
static dt empty_d
 

Detailed Description

Base class for all expressions.

Definition at line 46 of file expr.h.

Member Typedef Documentation

§ operandst

typedef std::vector<exprt> exprt::operandst

Definition at line 49 of file expr.h.

Constructor & Destructor Documentation

§ exprt() [1/3]

exprt::exprt ( )
inline

§ exprt() [2/3]

exprt::exprt ( const irep_idt _id)
inlineexplicit

Definition at line 53 of file expr.h.

§ exprt() [3/3]

exprt::exprt ( const irep_idt _id,
const typet _type 
)
inline

Definition at line 54 of file expr.h.

References irept::add().

Member Function Documentation

§ add_expr()

exprt& exprt::add_expr ( const irep_idt name)
inline

Definition at line 152 of file expr.h.

References irept::add().

§ add_source_location()

source_locationt& exprt::add_source_location ( )
inline

Definition at line 147 of file expr.h.

References irept::add().

Referenced by adjust_float_expressions(), java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), ansi_c_entry_point(), cpp_typecheck_resolvet::apply_template_args(), ansi_c_declaratort::build(), c_nondet_symbol_factory(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), cpp_declarator_convertert::combine_types(), cpp_typecheckt::convert_anon_struct_union_member(), jsil_convertt::convert_code(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_decl(), goto_convertt::convert_expression(), cpp_typecheck_resolvet::convert_identifier(), goto_convertt::convert_ifthenelse(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), goto_convertt::convert_msc_leave(), goto_program2codet::convert_start_thread(), cpp_typecheck_resolvet::convert_template_parameter(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), cpp_declaratort::cpp_declaratort(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), goto_convertt::do_array_equal(), goto_convertt::do_array_op(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_write(), string_instrumentationt::do_fscanf(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer_list(), goto_convertt::do_input(), cpp_typecheckt::do_not_typechecked(), goto_convertt::do_output(), goto_convertt::do_printf(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), goto_convertt::do_scanf(), string_instrumentationt::do_snprintf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_sprintf(), cpp_typecheckt::dtor(), cpp_typecheckt::explicit_typecast_ambiguity(), cpp_typecheckt::full_member_initialization(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_struct_init(), cpp_typecheckt::get_component(), java_object_factoryt::get_null_assignment(), has_and_or(), escape_analysist::insert_cleanup(), goto_inlinet::insert_function_nobody(), dump_ct::insert_local_type_decls(), interrupt(), is_empty(), java_entry_point(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), goto_convertt::make_compound_literal(), goto_convertt::make_temp_symbol(), cpp_typecheckt::new_temporary(), goto_convertt::new_tmp_symbol(), object_factory(), cpp_typecheckt::operator_is_overloaded(), goto_inlinet::parameter_assignments(), goto_inlinet::parameter_destruction(), cpp_convert_typet::read_function_type(), record_function_outputs(), cpp_typecheckt::reference_binding(), goto_convertt::remove_assignment(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_malloc(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_statement_expression(), constant_propagator_ait::replace(), replace_location(), cpp_typecheck_resolvet::resolve(), rewrite_index(), Parser::rExprStatement(), Parser::rStatement(), Parser::rTemplateArgs(), parsert::set_source_location(), simplify_exprt::simplify_typecast(), static_lifetime_init(), goto_symext::symex_function_call_code(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_dowhile(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_cpp_name(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_expr_function_identifier(), c_typecheck_baset::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_function_expr(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_typeof_type(), c_typecheck_baset::typecheck_while(), goto_convertt::unwind_destructor_stack(), cpp_typecheckt::user_defined_conversion_sequence(), yyansi_cparse(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

§ copy_to_operands() [1/3]

void exprt::copy_to_operands ( const exprt expr)

Definition at line 61 of file expr.cpp.

References operands().

Referenced by disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), guardt::add(), code_blockt::add(), c_typecheck_baset::add_argc_argv(), code_try_catcht::add_catch(), pointer_arithmetict::add_to_offset(), java_bytecode_vtable_factoryt::add_vtable_entry(), java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), already_typechecked(), and_exprt::and_exprt(), ansi_c_entry_point(), smt1_convt::array_index(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), acceleration_utilst::assign_array(), binary_exprt::binary_exprt(), bitand_exprt::bitand_exprt(), bitor_exprt::bitor_exprt(), buffer_size(), value_set_dereferencet::build_reference_to(), bv_pointerst::bv_get_rec(), boolbvt::bv_get_unbounded_array(), byte_extract_exprt::byte_extract_exprt(), byte_update_exprt::byte_update_exprt(), smt1_convt::ce_value(), code_asmt::code_asmt(), code_assertt::code_assertt(), code_assignt::code_assignt(), code_assumet::code_assumet(), code_deadt::code_deadt(), code_declt::code_declt(), code_expressiont::code_expressiont(), code_returnt::code_returnt(), code_switch_caset::code_switch_caset(), collect_comma_expression(), symex_slice_by_tracet::compute_ts_back(), concatenation_exprt::concatenation_exprt(), prop_minimizet::constraint(), cpp_typecheckt::convert_anonymous_union(), dplib_convt::convert_array_index(), cvc_convt::convert_array_index(), symex_target_equationt::convert_assertions(), goto_program2codet::convert_assign_rec(), goto_convertt::convert_cpp_delete(), goto_program2codet::convert_decl(), cpp_typecheckt::convert_function(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_if(), cpp_typecheck_resolvet::convert_identifier(), goto_program2codet::convert_instruction(), java_bytecode_convert_methodt::convert_instructions(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), smt1_convt::convert_plus(), goto_program2codet::convert_return(), bv_cbmct::convert_waitfor(), copy_array(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), goto_convertt::cpp_new_initializer(), java_bytecode_convert_methodt::create_stack_tmp_var(), cpp_typecheckt::default_cpctor(), dereference_exprt::dereference_exprt(), goto_checkt::div_by_zero_check(), acceleration_utilst::do_arrays(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_write(), goto_convertt::do_function_call_symbol(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), dynamic_object(), character_refine_preprocesst::expr_of_to_chars(), extractbits_exprt::extractbits_exprt(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), flatten_byte_extract(), floatbv_typecast_exprt::floatbv_typecast_exprt(), java_object_factoryt::gen_nondet_array_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_nondet_struct_init(), invariant_sett::get_constant(), invariant_propagationt::get_objects_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), guardt::guard_expr(), ieee_float_op_exprt::ieee_float_op_exprt(), if_exprt::if_exprt(), index_designatort::index_designatort(), index_exprt::index_exprt(), string_instrumentationt::invalidate_buffer(), is_empty(), is_zero_string(), member_exprt::member_exprt(), value_set_dereferencet::memory_model_bytes(), goto_checkt::mod_by_zero_check(), float_bvt::mul(), multi_ary_exprt::multi_ary_exprt(), not_exprt::not_exprt(), cpp_typecheckt::operator_is_overloaded(), or_exprt::or_exprt(), pointer_logict::pointer_expr(), pointer_offset_sum(), predicate_exprt::predicate_exprt(), cpp_typecheckt::reference_binding(), float_bvt::relation(), goto_convertt::remove_assignment(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_temporary_object(), goto_inlinet::replace_return(), reserve_operands(), smt1_convt::set_value(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_index(), simplify_exprt::simplify_member(), simplify_exprt::simplify_plus(), c_sizeoft::sizeof_rec(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), string_constraintt::string_constraintt(), string_exprt::string_exprt(), string_not_contains_constraintt::string_not_contains_constraintt(), goto_symext::symex_assign_array(), goto_symext::symex_assign_byte_extract(), goto_symext::symex_assign_struct_member(), goto_symext::symex_cpp_new(), goto_symext::symex_macro(), to_update_expr(), typecast_exprt::typecast_exprt(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_expr_dereference(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), c_typecheck_baset::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_expr_sizeof(), c_typecheck_baset::typecheck_expr_typecast(), cpp_typecheckt::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_expr(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_return(), cpp_typecheckt::typecheck_side_effect_function_call(), unary_exprt::unary_exprt(), unpack_rec(), update_exprt::update_exprt(), cpp_typecheckt::user_defined_conversion_sequence(), utf16_to_array(), with_exprt::with_exprt(), cpp_typecheckt::zero_initializer(), zero_initializert::zero_initializer_rec(), and zero_string_length().

§ copy_to_operands() [2/3]

void exprt::copy_to_operands ( const exprt e1,
const exprt e2 
)

Definition at line 66 of file expr.cpp.

References operands().

§ copy_to_operands() [3/3]

void exprt::copy_to_operands ( const exprt e1,
const exprt e2,
const exprt e3 
)

Definition at line 76 of file expr.cpp.

References operands().

§ find_expr()

const exprt& exprt::find_expr ( const irep_idt name) const
inline

Definition at line 157 of file expr.h.

References irept::find(), and visit().

§ find_source_location()

const source_locationt & exprt::find_source_location ( ) const

Definition at line 466 of file expr.cpp.

References forall_operands, get_nil_irep(), irept::is_not_nil(), and source_location().

Referenced by goto_checkt::bounds_check(), goto_convertt::clean_expr(), goto_checkt::conversion_check(), goto_convertt::convert(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_break(), boolbvt::convert_constant(), goto_convertt::convert_continue(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), goto_convertt::convert_dowhile(), goto_convertt::convert_end_thread(), goto_convertt::convert_expression(), boolbvt::convert_extractbits(), goto_convert_functionst::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_ifthenelse(), goto_convertt::convert_init(), goto_convertt::convert_label(), goto_convertt::convert_loop_invariant(), boolbvt::convert_member(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), cpp_typecheckt::convert_pmop(), goto_convertt::convert_return(), goto_convertt::convert_specc_event(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), boolbvt::convert_struct(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), boolbvt::convert_with(), goto_program_dereferencet::dereference_rec(), goto_checkt::div_by_zero_check(), goto_convertt::do_atomic_begin(), goto_convertt::do_atomic_end(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer_list(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), linkingt::duplicate_object_symbol(), typecheckt::err_location(), goto_checkt::float_overflow_check(), goto_convertt::get_array_argument(), goto_convertt::get_string_constant(), has_and_or(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), goto_checkt::integer_overflow_check(), is_empty(), goto_convertt::make_compound_literal(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), goto_convertt::make_temp_symbol(), goto_checkt::mod_by_zero_check(), goto_checkt::nan_check(), goto_inlinet::parameter_assignments(), goto_checkt::pointer_overflow_check(), goto_checkt::pointer_rel_check(), goto_checkt::pointer_validity_check(), cpp_typecheckt::reference_initializer(), goto_convertt::remove_assignment(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), reserve_operands(), goto_convertt::rewrite_boolean(), c_typecheck_baset::typecheck_array_type(), cpp_typecheckt::typecheck_assign(), cpp_typecheckt::typecheck_cast_expr(), c_typecheck_baset::typecheck_custom_type(), cpp_typecheckt::typecheck_decl(), cpp_typecheckt::typecheck_enum_body(), cpp_typecheckt::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), cpp_typecheckt::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_throw(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_redefinition_non_type(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_symbol(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_vector_type(), and goto_checkt::undefined_shift_check().

§ has_operands()

§ is_boolean()

§ is_constant()

bool exprt::is_constant ( ) const

Definition at line 128 of file expr.cpp.

References irept::id().

Referenced by path_symex_statet::array_theory(), value_set_dereferencet::build_reference_to(), inv_object_storet::build_string(), goto_program2codet::cleanup_expr(), collect_conditions_rec(), collect_decisions_rec(), goto_symex_statet::constant_propagation(), prop_conv_solvert::convert_bool(), bv_refinementt::convert_div(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), goto_program2codet::convert_goto_switch(), bv_refinementt::convert_mod(), boolbvt::convert_shift(), expr2cppt::convert_with_precedence(), c_typecheck_baset::do_special_functions(), simplify_exprt::eliminate_common_addends(), custom_bitvector_domaint::eval(), path_symex_statet::expand_structs_and_arrays(), bv_arithmetict::from_expr(), bdd_exprt::from_expr_rec(), invariant_sett::get_constant(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), simplify_exprt::get_values(), inv_object_storet::is_constant(), inv_object_storet::is_constant_address_rec(), is_dereference_integer_object(), is_false(), is_one(), is_skip(), is_true(), is_zero(), c_typecheck_baset::make_constant(), c_typecheck_baset::make_constant_index(), mul(), negate(), format_constantt::operator()(), smt2_convt::parse_struct(), path_symext::propagate(), reserve_operands(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_div(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), subtract(), sum(), path_symext::symex_malloc(), goto_symext::symex_malloc(), to_integer(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_expr_trinary(), and c_typecheck_baset::typecheck_redefinition_non_type().

§ is_false()

bool exprt::is_false ( ) const

Definition at line 140 of file expr.cpp.

References irept::id(), is_constant(), and type().

Referenced by guardt::add(), guardt::as_expr(), boolean_negate(), custom_bitvector_analysist::check(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_ifthenelse(), symex_slice_by_tracet::compute_ts_back(), cvc_convt::convert(), smt1_convt::convert(), smt2_convt::convert(), cpp_typecheckt::convert(), cvc_convt::convert_as_bv(), prop_conv_solvert::convert_bool(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), cvc_convt::convert_constant_expr(), dplib_convt::convert_dplib_expr(), path_searcht::drop_state(), bdd_exprt::from_expr_rec(), memory_model_sct::from_read(), prop_conv_solvert::get_bool(), rw_range_sett::get_objects_if(), rw_guarded_range_set_value_sett::get_objects_if(), guardt::guard_expr(), instantiate_quantifier(), goto_symex_statet::l2_thread_read_encoding(), make_not(), symex_bmct::merge_goto(), goto_symext::merge_value_sets(), invariant_sett::nnf(), operator|=(), goto_symext::phi_function(), postcondition(), precondition(), memory_model_tsot::program_order(), reserve_operands(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_not(), simplify_exprt::simplify_typecast(), invariant_sett::strengthen_rec(), goto_symext::symex_assign_if(), goto_symext::symex_assume(), goto_symext::symex_atomic_begin(), goto_symext::symex_atomic_end(), goto_symext::symex_goto(), goto_symext::symex_start_thread(), goto_symext::symex_step(), symex_bmct::symex_step(), cpp_typecheckt::template_suffix(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), and c_typecheck_baset::typecheck_c_enum_type().

§ is_one()

§ is_true()

bool exprt::is_true ( ) const

Definition at line 133 of file expr.cpp.

References irept::id(), is_constant(), and type().

Referenced by guardt::add(), goto_checkt::add_guarded_claim(), string_refinementt::add_lemma(), interval_domaint::ai_simplify(), guardt::as_expr(), boolean_negate(), sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), custom_bitvector_analysist::check(), path_searcht::check_assertion(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code_ifthenelse(), goto_program2codet::cleanup_expr(), cvc_convt::convert(), smt1_convt::convert(), smt2_convt::convert(), cpp_typecheckt::convert(), cvc_convt::convert_as_bv(), prop_conv_solvert::convert_bool(), goto_convertt::convert_bp_enforce(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), dplib_convt::convert_dplib_expr(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_while(), goto_program_dereferencet::dereference_failure(), value_sett::do_free(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), path_searcht::do_show_vcc(), interpretert::evaluate(), prop_conv_solvert::get_bool(), rw_range_sett::get_objects_if(), rw_guarded_range_set_value_sett::get_objects_if(), guardt::guard_expr(), invariant_sett::implies_rec(), instantiate_quantifier(), instrument_intervals(), is_empty(), json(), goto_symex_statet::l2_thread_read_encoding(), goto_symext::loop_bound_exceeded(), make_not(), invariant_sett::nnf(), taint_analysist::operator()(), operator|=(), sat_path_enumeratort::record_path(), disjunctive_polynomial_accelerationt::record_path(), goto_inlinet::replace_return(), reserve_operands(), dplib_convt::set_to(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_not(), simplify_exprt::simplify_typecast(), symex_slice_by_tracet::slice_SSA_steps(), postconditiont::strengthen(), invariant_sett::strengthen_rec(), goto_symext::symex_assign_if(), goto_symext::symex_assign_symbol(), goto_symext::symex_assume(), goto_symext::symex_goto(), cpp_typecheckt::template_suffix(), trace_value_binary(), c_typecheck_baset::typecheck_c_enum_type(), goto_symext::vcc(), and xml().

§ is_zero()

bool exprt::is_zero ( ) const

Definition at line 236 of file expr.cpp.

References CHECK_RETURN, constant_exprt::get_value(), irept::id_string(), is_constant(), rationalt::is_zero(), to_constant_expr(), to_rational(), type(), and constant_exprt::value_is_zero_string().

Referenced by string_abstractiont::abstract_char_assign(), linkingt::adjust_object_type_rec(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), value_set_dereferencet::build_reference_to(), dump_ct::cleanup_expr(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), goto_program2codet::convert_assign_varargs(), expr2ct::convert_complex(), expr2javat::convert_constant(), expr2ct::convert_with_precedence(), dereferencet::dereference_typecast(), c_typecheck_baset::do_designated_initializer(), simplify_exprt::eliminate_common_addends(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_string_argument_rec(), value_sett::get_value_set_rec(), c_typecastt::implicit_typecast_followed(), value_set_dereferencet::memory_model_bytes(), goto_convertt::needs_cleaning(), pointer_offset_sum(), pointer_arithmetict::read(), dereferencet::read_object(), cpp_typecheckt::reinterpret_typecast(), reserve_operands(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_typecast(), cpp_typecheckt::standard_conversion_pointer(), c_typecheck_baset::typecheck_expr_rel(), and cpp_typecheckt::typecheck_method_bodies().

§ make_bool()

§ make_false()

§ make_not()

§ make_true()

§ make_typecast()

void exprt::make_typecast ( const typet _type)

Definition at line 90 of file expr.cpp.

References move_to_operands(), irept::set(), and irept::swap().

Referenced by pointer_arithmetict::add_to_offset(), functionst::arguments_equal(), goto_checkt::bounds_check(), string_abstractiont::build(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), goto_program2codet::cleanup_expr(), cpp_typecheckt::convert(), goto_convertt::convert(), goto_convertt::convert_assign(), boolbvt::convert_extractbit(), java_bytecode_convert_methodt::convert_instructions(), dereferencet::dereference_plus(), goto_convertt::do_cpp_new(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), c_typecheck_baset::do_special_functions(), c_typecastt::do_typecast(), dynamic_object_upper_bound(), flatten_byte_update(), path_symext::function_call_rec(), value_sett::get_reference_set_rec(), goto_checkt::goto_check(), cpp_typecheck_resolvet::guess_template_args(), escape_analysist::insert_cleanup(), is_empty(), cpp_typecheckt::make_ptr_typecast(), printf_formattert::make_type(), string_abstractiont::make_type(), string_instrumentationt::make_type(), value_set_dereferencet::memory_model_bytes(), value_set_dereferencet::memory_model_conversion(), object_upper_bound(), goto_inlinet::parameter_assignments(), dereferencet::read_object(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_assignment(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_inlinet::replace_return(), reserve_operands(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_index(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_pointer_offset(), size_of_expr(), cpp_typecheckt::standard_conversion_boolean(), cpp_typecheckt::standard_conversion_floating_integral_conversion(), cpp_typecheckt::standard_conversion_floating_point_conversion(), cpp_typecheckt::standard_conversion_floating_point_promotion(), cpp_typecheckt::standard_conversion_integral_conversion(), cpp_typecheckt::standard_conversion_integral_promotion(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_typecast(), goto_symext::symex_assign_typecast(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_malloc(), goto_symext::symex_malloc(), path_symext::symex_va_arg_next(), java_bytecode_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), and cpp_typecheckt::zero_initializer().

§ move_to_operands() [1/3]

void exprt::move_to_operands ( exprt expr)

Definition at line 28 of file expr.cpp.

References get_nil_irep(), and operands().

Referenced by goto_checkt::add_guarded_claim(), java_object_factoryt::allocate_nondet_length_array(), ansi_c_entry_point(), basic_blocks(), simplify_exprt::bits2expr(), goto_convertt::case_guard(), goto_program2codet::cleanup_code_ifthenelse(), dump_ct::cleanup_expr(), symex_slice_by_tracet::compute_ts_back(), cpp_typecheckt::convert_anonymous_union(), goto_program2codet::convert_assign_varargs(), goto_program2codet::convert_decl(), goto_program2codet::convert_do_while(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_goto(), goto_program2codet::convert_goto_if(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), cpp_typecheck_resolvet::convert_identifier(), goto_program2codet::convert_instruction(), java_bytecode_convert_methodt::convert_instructions(), goto_program2codet::convert_labels(), goto_program2codet::convert_start_thread(), bv_cbmct::convert_waitfor(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), string_instrumentationt::do_format_string_write(), cpp_typecheckt::dtor(), character_refine_preprocesst::expr_of_to_chars(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get_cnf(), qbf_squolem_coret::f_get_dnf(), flatten_byte_extract(), cpp_typecheckt::full_member_initialization(), java_object_factoryt::gen_nondet_array_init(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), c_typecastt::implicit_typecast_followed(), is_empty(), java_entry_point(), java_record_outputs(), jsil_entry_point(), codet::make_block(), make_not(), make_typecast(), negate(), cpp_typecheckt::new_temporary(), cpp_typecheckt::operator_is_overloaded(), Parser::rAdditiveExpr(), Parser::rAllocateExpr(), Parser::rAllocateInitializer(), Parser::rAndExpr(), Parser::rCastExpr(), Parser::rClassBody(), Parser::rCommaExpression(), Parser::rCompoundStatement(), Parser::rCondition(), Parser::rConditionalExpr(), Parser::rDoStatement(), record_function_outputs(), cpp_typecheckt::reference_binding(), goto_convertt::remove_malloc(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_temporary_object(), goto_inlinet::replace_return(), Parser::rEqualityExpr(), reserve_operands(), Parser::rExclusiveOrExpr(), Parser::rExpression(), Parser::rExprStatement(), Parser::rForStatement(), Parser::rFunctionArguments(), Parser::rInclusiveOrExpr(), Parser::rInitializeExpr(), Parser::rIntegralDeclStatement(), Parser::rLogicalAndExpr(), Parser::rLogicalOrExpr(), Parser::rMSC_if_existsExpr(), Parser::rMSC_if_existsStatement(), Parser::rMSC_tryStatement(), Parser::rMSCAsmStatement(), Parser::rMSCuuidof(), Parser::rMultiplyExpr(), Parser::rNoexceptExpr(), Parser::rOtherDeclStatement(), Parser::rPmExpr(), Parser::rPostfixExpr(), Parser::rPrimaryExpr(), Parser::rRelationalExpr(), Parser::rShiftExpr(), Parser::rSizeofExpr(), Parser::rStatement(), Parser::rSwitchStatement(), Parser::rThrowExpr(), Parser::rTryStatement(), Parser::rUnaryExpr(), Parser::rWhileStatement(), simplify_exprt::simplify_address_of(), c_sizeoft::sizeof_rec(), symex_slice_by_tracet::slice_by_trace(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), c_typecheck_baset::typecheck_block(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_dowhile(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_switch(), c_typecheck_baset::typecheck_while(), yyansi_cparse(), and yyjsilparse().

§ move_to_operands() [2/3]

void exprt::move_to_operands ( exprt e1,
exprt e2 
)

Definition at line 35 of file expr.cpp.

References get_nil_irep(), and operands().

§ move_to_operands() [3/3]

void exprt::move_to_operands ( exprt e1,
exprt e2,
exprt e3 
)

Definition at line 47 of file expr.cpp.

References get_nil_irep(), and operands().

§ mul()

§ negate()

§ op0() [1/2]

exprt& exprt::op0 ( )
inline

Definition at line 84 of file expr.h.

References operands().

Referenced by string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_pointer_assign(), bv_refinementt::add_approximation(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraints(), arrayst::add_array_constraints_array_of(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), string_constraint_generatort::add_axioms_for_string_expr(), string_constraint_generatort::add_axioms_from_literal(), acceleratet::add_dirty_checks(), string_abstractiont::add_dummy_symbol_and_value(), pointer_logict::add_object(), goto_symext::add_to_lhs(), c_typecheck_baset::adjust_float_rel(), aliasing(), and_exprt::and_exprt(), ansi_c_entry_point(), invariant_sett::apply_code(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), index_exprt::array(), array_name(), bv_refinementt::arrays_overapproximated(), as_vcd_binary(), code_assertt::assertion(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), acceleration_utilst::assign_array(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), interval_domaint::assume_rec(), code_assumet::assumption(), boolean_negate(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), string_abstractiont::build(), satcheck_smvsat_interpolatort::build_aig(), build_full_lhs_rec(), inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), c_nondet_symbol_factory(), goto_convertt::case_guard(), code_switch_caset::case_op(), mm2cppt::check_acyclic(), goto_checkt::check_rec(), check_renaming(), clean_deref(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), dump_ct::cleanup_decl(), dump_ct::cleanup_expr(), code_labelt::code(), code_returnt::code_returnt(), arrayst::collect_arrays(), collect_comma_expression(), collect_decisions_rec(), complex_member(), member_exprt::compound(), preconditiont::compute_address_of(), compute_address_taken_functions(), compute_pointer_offset(), preconditiont::compute_rec(), symex_slice_by_tracet::compute_ts_back(), concatenate_array_id(), cpp_static_assertt::cond(), code_ifthenelset::cond(), code_whilet::cond(), code_dowhilet::cond(), if_exprt::cond(), goto_symex_statet::constant_propagation(), goto_symex_statet::constant_propagation_reference(), goto_checkt::conversion_check(), float_bvt::convert(), cpp_typecheckt::convert(), goto_convertt::convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), 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(), expr2ct::convert_array_member_value(), expr2ct::convert_array_of(), boolbvt::convert_array_of(), goto_convertt::convert_assign(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), smt1_convt::convert_byte_update(), boolbvt::convert_byte_update(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), jsil_convertt::convert_code(), expr2ct::convert_code_asm(), expr2ct::convert_code_assert(), expr2ct::convert_code_assume(), expr2cppt::convert_code_cpp_delete(), expr2ct::convert_code_dead(), expr2ct::convert_code_decl(), expr2ct::convert_code_expression(), expr2ct::convert_code_for(), expr2ct::convert_code_free(), expr2javat::convert_code_java_delete(), expr2ct::convert_code_lock(), expr2ct::convert_code_return(), expr2ct::convert_code_switch(), expr2ct::convert_code_unlock(), expr2ct::convert_comma(), cvc_convt::convert_comparison_expr(), expr2ct::convert_complex(), boolbvt::convert_complex_imag(), boolbvt::convert_complex_real(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), boolbvt::convert_constraint_select_one(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), expr2ct::convert_designated_initializer(), smt1_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_div(), goto_convertt::convert_dowhile(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_equality_expr(), cvc_convt::convert_expr(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), goto_convertt::convert_expression(), expr2cppt::convert_extractbit(), expr2ct::convert_extractbit(), expr2cppt::convert_extractbits(), expr2ct::convert_extractbits(), boolbvt::convert_extractbits(), convert_float_literal(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), boolbvt::convert_floatbv_typecast(), goto_program2codet::convert_goto_switch(), expr2ct::convert_Hoare(), boolbvt::convert_ieee_float_rel(), goto_convertt::convert_ifthenelse(), expr2ct::convert_index(), boolbvt::convert_index(), expr2ct::convert_index_designator(), cpp_typecheckt::convert_initializer(), convert_integer_literal(), smt1_convt::convert_is_dynamic_object(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), goto_convertt::convert_java_try_catch(), goto_convertt::convert_label(), boolbvt::convert_lambda(), expr2ct::convert_malloc(), expr2ct::convert_member(), smt1_convt::convert_minus(), smt2_convt::convert_minus(), cvc_convt::convert_minus_expr(), smt1_convt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), smt1_convt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), smt1_convt::convert_nary(), expr2ct::convert_object_descriptor(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cvc_convt::convert_plus_expr(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), expr2ct::convert_pointer_object_has_type(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_prob_coin(), expr2ct::convert_prob_uniform(), expr2ct::convert_quantifier(), smt1_convt::convert_relation(), smt2_convt::convert_relation(), boolbvt::convert_replication(), dplib_convt::convert_rest(), boolbvt::convert_rest(), boolbvt::convert_shift(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), expr2ct::convert_statement_expression(), smt1_convt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct_member_value(), expr2ct::convert_symbol(), goto_convertt::convert_try_catch(), smt1_convt::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), cvc_convt::convert_typecast_expr(), expr2ct::convert_unary(), boolbvt::convert_unary_minus(), expr2ct::convert_unary_post(), smt1_convt::convert_union(), boolbvt::convert_union(), expr2ct::convert_union(), expr2ct::convert_update(), boolbvt::convert_update_rec(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), smt1_convt::convert_with(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), cvc_convt::convert_with_expr(), expr2ct::convert_with_precedence(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), smt2_convt::define_object_size(), dereferencet::dereference_plus(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_sett::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), goto_convertt::do_array_equal(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), goto_convertt::do_function_call_symbol(), c_typecheck_baset::do_initializer_list(), goto_convertt::do_java_new_array(), acceleration_utilst::do_nonrecursive(), cpp_typecheckt::do_not_typechecked(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), dynamic_object_exprt::dynamic_object_exprt(), cpp_typecheckt::dynamic_typecast(), custom_bitvector_domaint::eval(), value_sett::eval_pointer_offset(), interpretert::evaluate(), interpretert::evaluate_address(), exists_exprt::exists_exprt(), cpp_typecheckt::explicit_typecast_ambiguity(), expr_eq(), code_expressiont::expression(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get_cnf(), qbf_squolem_coret::f_get_dnf(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), goto_convertt::finish_computed_gotos(), codet::first_statement(), overflow_instrumentert::fix_types(), fix_types(), flatten_byte_update(), goto_checkt::float_overflow_check(), smt2_convt::floatbv_suffix(), forall_exprt::forall_exprt(), polynomialt::from_expr(), bdd_exprt::from_expr_rec(), side_effect_expr_function_callt::function(), function_application_exprt::function(), acceleration_utilst::gather_array_accesses(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_pointer_target_init(), goto_convertt::generate_conditional_branch(), goto_convertt::get_array_argument(), prop_conv_solvert::get_bool(), goto_inlinet::get_call(), goto_convertt::get_constant(), dynamic_object_exprt::get_instance(), rw_range_sett::get_objects_complex(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_string_argument_rec(), goto_convertt::get_string_constant(), value_set_dereferencet::get_symbol(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), goto_checkt::goto_check(), value_sett::guard(), guardt::guard_expr(), has_and_or(), c_typecastt::implicit_typecast_followed(), invariant_sett::implies_rec(), index_designatort::index(), code_fort::init(), string_refinementt::initial_index_set(), instantiate_quantifier(), path_symex_statet::instantiate_rec(), path_symex_statet::instantiate_rec_address(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_throw(), goto_checkt::integer_overflow_check(), transt::invar(), constant_propagator_domaint::valuest::is_array_constant(), inv_object_storet::is_constant_address(), inv_object_storet::is_constant_address_rec(), is_dereference_integer_object(), is_empty(), is_index_member_symbol(), is_lvalue(), postconditiont::is_used(), postconditiont::is_used_address_of(), java_record_outputs(), json(), string_exprt::length(), let_exprt::let_exprt(), code_assignt::lhs(), binary_relation_exprt::lhs(), code_function_callt::lhs(), ieee_float_op_exprt::lhs(), boolbvt::literal(), look_through_casts(), remove_instanceoft::lower_instanceof(), make_clean_pointer_cast(), c_typecheck_baset::make_designator(), value_sett::make_member(), make_va_list(), string_refinementt::map_representation_of_sum(), invariant_sett::modifies(), string_abstractiont::move_lhs_arithmetic(), goto_checkt::nan_check(), negate(), invariant_sett::nnf(), object_descriptor_exprt::object(), address_of_exprt::object(), object_descriptor_exprt::object_descriptor_exprt(), pointer_logict::object_rec(), simplify_exprt::objects_equal(), simplify_exprt::objects_equal_address_of(), objects_read(), with_exprt::old(), update_exprt::old(), byte_extract_exprt::op(), byte_update_exprt::op(), unary_exprt::op(), typecast_exprt::op(), floatbv_typecast_exprt::op(), shift_exprt::op(), not_exprt::op(), cpp_typecheckt::operator_is_overloaded(), or_exprt::or_exprt(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), dereference_exprt::pointer(), goto_checkt::pointer_rel_check(), goto_checkt::pointer_validity_check(), string_constraintt::premise(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), printf_formattert::process_format(), remove_asmt::process_instruction(), acceleration_utilst::push_nondet(), Parser::rDeclarationStatement(), pointer_arithmetict::read(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), complex_exprt::real(), arrayst::record_array_equality(), record_function_outputs(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_cpp_delete(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), remove_vector(), goto_symex_statet::rename(), goto_symext::replace_array_equal(), constant_propagator_ait::replace_array_symbol(), goto_inlinet::replace_return(), string_abstractiont::replace_string_macros(), goto_symext::return_assignment(), code_returnt::return_value(), goto_symext::rewrite_quantifiers(), Parser::rGCCAsmStatement(), Parser::rIfStatement(), object_descriptor_exprt::root_object(), Parser::rStatement(), Parser::rTypedefStatement(), goto_program2codet::scan_for_varargs(), set_class_identifier(), dynamic_object_exprt::set_instance(), cvc_convt::set_to(), dplib_convt::set_to(), smt1_convt::set_to(), prop_conv_solvert::set_to(), smt2_convt::set_to(), sign_of_expr(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_good_pointer(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_invalid_pointer(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_member(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_unary_plus(), simplify_exprt::simplify_with(), c_sizeoft::sizeof_rec(), extractbit_exprt::src(), extractbits_exprt::src(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), string_from_ns(), member_exprt::struct_op(), code_declt::symbol(), code_deadt::symbol(), let_exprt::symbol(), forall_exprt::symbol(), exists_exprt::symbol(), goto_symext::symex_assign(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_assign_typecast(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_goto(), goto_symext::symex_input(), goto_symext::symex_macro(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), goto_symext::symex_output(), path_symext::symex_va_arg_next(), thread_exit_instrumentation(), replication_exprt::times(), ansi_c_languaget::to_expr(), to_update_expr(), trace_value_binary(), custom_bitvector_domaint::transform(), code_try_catcht::try_code(), constant_propagator_domaint::two_way_propagate_rec(), c_typecheck_baset::typecheck_asm(), jsil_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_assign(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), cpp_typecheckt::typecheck_expr_throw(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_num(), jsil_typecheckt::typecheck_expr_unary_string(), c_typecheck_baset::typecheck_expression(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_function_expr(), c_typecheck_baset::typecheck_gcc_computed_goto(), c_typecheck_baset::typecheck_gcc_switch_case_range(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), cpp_typecheckt::typecheck_switch(), cpp_typecheckt::typecheck_try_catch(), c_typecheck_baset::typecheck_typeof_type(), string_not_contains_constraintt::univ_lower_bound(), string_refinementt::update_index_set(), cpp_typecheckt::user_defined_conversion_sequence(), code_switcht::value(), array_of_exprt::what(), xml(), and cpp_typecheckt::zero_initializer().

§ op0() [2/2]

const exprt& exprt::op0 ( ) const
inline

Definition at line 96 of file expr.h.

References operands().

§ op1() [1/2]

exprt& exprt::op1 ( )
inline

Definition at line 87 of file expr.h.

References operands().

Referenced by bv_refinementt::add_approximation(), arrayst::add_array_Ackermann_constraints(), string_constraint_generatort::add_axioms_from_char_array(), string_abstractiont::add_dummy_symbol_and_value(), pointer_arithmetict::add_to_offset(), adjust_float_expressions(), and_exprt::and_exprt(), ansi_c_entry_point(), invariant_sett::apply_code(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), side_effect_expr_function_callt::arguments(), function_application_exprt::arguments(), bv_refinementt::arrays_overapproximated(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), acceleration_utilst::assign_array(), constant_propagator_domaint::assign_rec(), interval_domaint::assume_rec(), string_constraintt::body(), code_switcht::body(), code_whilet::body(), code_dowhilet::body(), goto_checkt::bounds_check(), cpp_typecheck_fargst::build(), string_abstractiont::build(), satcheck_smvsat_interpolatort::build_aig(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), c_nondet_symbol_factory(), mm2cppt::check_acyclic(), goto_checkt::check_rec(), check_renaming(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), goto_program2codet::cleanup_code(), dump_ct::cleanup_decl(), code_switch_caset::code(), code_ifthenelset::code_ifthenelset(), collect_comma_expression(), complex_member(), preconditiont::compute_address_of(), compute_pointer_offset(), code_fort::cond(), string_exprt::content(), float_bvt::convert(), cpp_typecheckt::convert(), goto_convertt::convert(), dplib_convt::convert_address_of_rec(), cvc_convt::convert_address_of_rec(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), goto_convertt::convert_assign(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), goto_convertt::convert_bp_enforce(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), smt1_convt::convert_byte_update(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), jsil_convertt::convert_code(), expr2ct::convert_code_asm(), expr2ct::convert_code_decl(), expr2ct::convert_code_for(), expr2ct::convert_comma(), cvc_convt::convert_comparison_expr(), expr2ct::convert_complex(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), bv_refinementt::convert_div(), smt1_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_div(), goto_convertt::convert_dowhile(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_equality_expr(), cvc_convt::convert_expr(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), expr2cppt::convert_extractbit(), expr2ct::convert_extractbit(), expr2cppt::convert_extractbits(), expr2ct::convert_extractbits(), boolbvt::convert_extractbits(), convert_float_literal(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), expr2ct::convert_Hoare(), boolbvt::convert_ieee_float_rel(), goto_convertt::convert_ifthenelse(), expr2ct::convert_index(), boolbvt::convert_index(), convert_integer_literal(), expr2javat::convert_java_instanceof(), boolbvt::convert_lambda(), smt1_convt::convert_minus(), smt2_convt::convert_minus(), cvc_convt::convert_minus_expr(), bv_refinementt::convert_mod(), smt1_convt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_finally(), smt1_convt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_object_descriptor(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cvc_convt::convert_plus_expr(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_quantifier(), smt1_convt::convert_relation(), smt2_convt::convert_relation(), boolbvt::convert_replication(), dplib_convt::convert_rest(), boolbvt::convert_rest(), boolbvt::convert_shift(), expr2ct::convert_update(), boolbvt::convert_update(), bv_cbmct::convert_waitfor(), smt1_convt::convert_with(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), dereferencet::dereference_plus(), goto_program_dereferencet::dereference_rec(), cpp_static_assertt::description(), update_exprt::designator(), shift_exprt::distance(), goto_checkt::div_by_zero_check(), goto_convertt::do_function_call_symbol(), goto_convertt::do_java_new_array(), acceleration_utilst::do_nonrecursive(), goto_convertt::do_scanf(), dynamic_object_exprt::dynamic_object_exprt(), custom_bitvector_domaint::eval(), interpretert::evaluate(), interpretert::evaluate_address(), cpp_typecheckt::explicit_typecast_ambiguity(), smt1_convt::find_symbols(), overflow_instrumentert::fix_types(), fix_types(), flatten_byte_update(), goto_checkt::float_overflow_check(), polynomialt::from_expr(), bdd_exprt::from_expr_rec(), code_function_callt::function(), remove_asmt::gcc_asm_function_call(), goto_inlinet::get_call(), goto_convertt::get_constant(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_string_argument_rec(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), simplify_exprt::get_values(), guardt::guard_expr(), has_and_or(), complex_exprt::imag(), invariant_sett::implies_rec(), index_exprt::index(), extractbit_exprt::index(), transt::init(), string_refinementt::initial_index_set(), instantiate_quantifier(), path_symex_statet::instantiate_rec_address(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), goto_checkt::integer_overflow_check(), constant_propagator_domaint::valuest::is_array_constant(), inv_object_storet::is_constant_address_rec(), is_empty(), postconditiont::is_used_address_of(), java_record_outputs(), remove_instanceoft::lower_instanceof(), value_sett::make_member(), string_refinementt::map_representation_of_sum(), goto_checkt::mod_by_zero_check(), invariant_sett::modifies(), string_abstractiont::move_lhs_arithmetic(), goto_checkt::nan_check(), cpp_typecheckt::new_temporary(), invariant_sett::nnf(), object_descriptor_exprt::object_descriptor_exprt(), objects_written(), byte_extract_exprt::offset(), byte_update_exprt::offset(), object_descriptor_exprt::offset(), replication_exprt::op(), operator-=(), operator|=(), or_exprt::or_exprt(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), goto_checkt::pointer_rel_check(), acceleration_utilst::push_nondet(), pointer_arithmetict::read(), _rw_set_loct::read_write_rec(), arrayst::record_array_equality(), record_function_outputs(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), remove_vector(), goto_symext::replace_array_equal(), constant_propagator_ait::replace_array_symbol(), goto_symext::rewrite_quantifiers(), code_assignt::rhs(), binary_relation_exprt::rhs(), ieee_float_op_exprt::rhs(), Parser::rIfStatement(), floatbv_typecast_exprt::rounding_mode(), Parser::rStatement(), cvc_convt::set_to(), dplib_convt::set_to(), prop_conv_solvert::set_to(), bv_refinementt::set_to(), side_effect_expr_function_callt::side_effect_expr_function_callt(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_extractbit(), qdimacs_coret::simplify_extractbits(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_member(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_with(), c_sizeoft::sizeof_rec(), symex_slice_by_tracet::slice_SSA_steps(), invariant_sett::strengthen_rec(), goto_symext::symex_assign_rec(), goto_symext::symex_macro(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), code_ifthenelset::then_case(), thread_exit_instrumentation(), to_update_expr(), if_exprt::true_case(), constant_propagator_domaint::two_way_propagate_rec(), jsil_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_assign(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), jsil_typecheckt::typecheck_expr_delete(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), jsil_typecheckt::typecheck_expr_subtype(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_gcc_switch_case_range(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), c_typecheck_baset::typecheck_side_effect_statement_expression(), unary_predicate_exprt::unary_predicate_exprt(), string_not_contains_constraintt::univ_upper_bound(), update_exprt::update_exprt(), string_refinementt::update_index_set(), extractbits_exprt::upper(), dynamic_object_exprt::valid(), let_exprt::value(), with_exprt::where(), forall_exprt::where(), and exists_exprt::where().

§ op1() [2/2]

const exprt& exprt::op1 ( ) const
inline

Definition at line 99 of file expr.h.

References operands().

§ op2() [1/2]

exprt& exprt::op2 ( )
inline

Definition at line 90 of file expr.h.

References operands().

Referenced by bv_refinementt::add_approximation(), string_abstractiont::add_dummy_symbol_and_value(), c_typecheck_baset::add_rounding_mode(), adjust_float_expressions(), and_exprt::and_exprt(), code_function_callt::arguments(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), binary_exprt::binary_exprt(), string_abstractiont::build_symbol_constant(), goto_checkt::check_rec(), bv_refinementt::check_SAT(), code_function_callt::code_function_callt(), code_ifthenelset::code_ifthenelset(), float_bvt::convert(), smt1_convt::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), smt1_convt::convert_byte_update(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), expr2ct::convert_code_asm(), expr2ct::convert_code_for(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_expr(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), expr2cppt::convert_extractbits(), expr2ct::convert_extractbits(), boolbvt::convert_extractbits(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), goto_convertt::convert_for(), goto_convertt::convert_gcc_switch_case_range(), expr2ct::convert_update(), boolbvt::convert_update(), bv_cbmct::convert_waitfor(), smt1_convt::convert_with(), smt2_convt::convert_with(), goto_program_dereferencet::dereference_instruction(), goto_program_dereferencet::dereference_rec(), code_ifthenelset::else_case(), interpretert::evaluate(), if_exprt::false_case(), flatten_byte_update(), remove_asmt::gcc_asm_function_call(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), code_ifthenelset::has_else_case(), is_empty(), code_fort::iter(), extractbits_exprt::lower(), value_sett::make_member(), invariant_sett::modifies(), with_exprt::new_value(), update_exprt::new_value(), objects_written(), operator-=(), operator|=(), or_exprt::or_exprt(), parse_lhs_read(), string_not_contains_constraintt::premise(), _rw_set_loct::read_write_rec(), Parser::rIfStatement(), ieee_float_op_exprt::rounding_mode(), Parser::rStatement(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_with(), goto_symext::symex_macro(), to_update_expr(), transt::trans(), c_typecheck_baset::typecheck_code(), jsil_typecheckt::typecheck_expr_ref(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_for(), c_typecheck_baset::typecheck_gcc_switch_case_range(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), unary_predicate_exprt::unary_predicate_exprt(), string_constraintt::univ_var(), byte_update_exprt::value(), and let_exprt::where().

§ op2() [2/2]

const exprt& exprt::op2 ( ) const
inline

Definition at line 102 of file expr.h.

References operands().

§ op3() [1/2]

§ op3() [2/2]

const exprt& exprt::op3 ( ) const
inline

Definition at line 105 of file expr.h.

References operands().

§ operands() [1/2]

operandst& exprt::operands ( )
inline

Definition at line 70 of file expr.h.

References irept::add(), and irept::get_sub().

Referenced by guardt::add(), bv_refinementt::add_approximation(), arrayst::add_array_constraints(), code_try_catcht::add_catch(), string_abstractiont::add_dummy_symbol_and_value(), pointer_logict::add_object(), c_typecheck_baset::add_rounding_mode(), goto_symext::add_to_lhs(), adjust_float_expressions(), c_typecheck_baset::adjust_float_rel(), aliasing(), and_exprt::and_exprt(), ansi_c_entry_point(), code_blockt::append(), invariant_sett::apply_code(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), code_function_callt::arguments(), side_effect_expr_function_callt::arguments(), function_application_exprt::arguments(), functionst::arguments_equal(), array_name(), bv_refinementt::arrays_overapproximated(), as_vcd_binary(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), interval_domaint::assume_rec(), base_type_eqt::base_type_eq_rec(), smt1_convt::binary2struct(), binary_exprt::binary_exprt(), boolean_negate(), cpp_typecheck_fargst::build(), string_abstractiont::build(), satcheck_smvsat_interpolatort::build_aig(), build_full_lhs_rec(), inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), boolbvt::bv_get_unbounded_array(), byte_extract_exprt::byte_extract_exprt(), byte_update_exprt::byte_update_exprt(), c_nondet_symbol_factory(), goto_convertt::case_guard(), smt1_convt::ce_value(), mm2cppt::check_acyclic(), goto_checkt::check_rec(), bv_refinementt::check_SAT(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_block(), dump_ct::cleanup_decl(), dump_ct::cleanup_expr(), code_assertt::code_assertt(), code_assignt::code_assignt(), code_assumet::code_assumet(), code_blockt::code_blockt(), code_deadt::code_deadt(), code_declt::code_declt(), code_dowhilet::code_dowhilet(), code_expressiont::code_expressiont(), code_fort::code_fort(), code_function_callt::code_function_callt(), code_ifthenelset::code_ifthenelset(), code_labelt::code_labelt(), code_returnt::code_returnt(), code_switch_caset::code_switch_caset(), code_switcht::code_switcht(), code_try_catcht::code_try_catcht(), code_whilet::code_whilet(), arrayst::collect_arrays(), smt2_convt::collect_bindings(), collect_comma_expression(), collect_conditions_rec(), collect_decisions_rec(), collect_deref_expr(), collect_operands(), complex_member(), preconditiont::compute_address_of(), compute_address_taken_functions(), compute_pointer_offset(), preconditiont::compute_rec(), symex_slice_by_tracet::compute_ts_back(), conjunction(), goto_symex_statet::constant_propagation_reference(), goto_checkt::conversion_check(), show_goto_functions_jsont::convert(), goto_convertt::convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), 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(), boolbvt::convert_array(), expr2ct::convert_array(), expr2ct::convert_array_list(), expr2ct::convert_array_member_value(), expr2ct::convert_array_of(), goto_convertt::convert_assign(), graphml_witnesst::convert_assign_rec(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), expr2ct::convert_binary(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), boolbvt::convert_byte_extract(), smt1_convt::convert_byte_update(), boolbvt::convert_byte_update(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), boolbvt::convert_case(), expr2ct::convert_code_array_copy(), expr2ct::convert_code_array_replace(), expr2ct::convert_code_array_set(), expr2ct::convert_code_asm(), expr2ct::convert_code_assert(), expr2ct::convert_code_assume(), expr2cppt::convert_code_cpp_delete(), expr2ct::convert_code_dead(), expr2ct::convert_code_decl(), expr2ct::convert_code_dowhile(), expr2ct::convert_code_expression(), expr2ct::convert_code_for(), expr2ct::convert_code_free(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), expr2ct::convert_code_ifthenelse(), expr2ct::convert_code_input(), expr2javat::convert_code_java_delete(), expr2ct::convert_code_lock(), expr2ct::convert_code_output(), expr2ct::convert_code_printf(), expr2ct::convert_code_return(), expr2ct::convert_code_switch(), expr2ct::convert_code_unlock(), expr2ct::convert_code_while(), expr2ct::convert_comma(), cvc_convt::convert_comparison_expr(), boolbvt::convert_complex(), expr2ct::convert_complex(), boolbvt::convert_complex_imag(), boolbvt::convert_complex_real(), boolbvt::convert_concatenation(), expr2ct::convert_cond(), boolbvt::convert_cond(), boolbvt::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), boolbvt::convert_constraint_select_one(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), expr2ct::convert_designated_initializer(), bv_refinementt::convert_div(), smt1_convt::convert_div(), smt2_convt::convert_div(), goto_convertt::convert_dowhile(), dplib_convt::convert_dplib_expr(), goto_convertt::convert_end_thread(), cvc_convt::convert_equality_expr(), cvc_convt::convert_expr(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), goto_convertt::convert_expression(), expr2cppt::convert_extractbit(), boolbvt::convert_extractbit(), expr2ct::convert_extractbit(), expr2cppt::convert_extractbits(), expr2ct::convert_extractbits(), boolbvt::convert_extractbits(), convert_float_literal(), smt2_convt::convert_floatbv(), smt1_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_div(), smt1_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_minus(), smt1_convt::convert_floatbv_mult(), smt2_convt::convert_floatbv_mult(), bv_refinementt::convert_floatbv_op(), boolbvt::convert_floatbv_op(), smt1_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_plus(), expr2ct::convert_function(), goto_convertt::convert_gcc_switch_case_range(), goto_program2codet::convert_goto_switch(), goto_program2codet::convert_goto_while(), expr2ct::convert_Hoare(), boolbvt::convert_ieee_float_rel(), goto_convertt::convert_ifthenelse(), smt1_convt::convert_index(), expr2ct::convert_index(), boolbvt::convert_index(), smt2_convt::convert_index(), expr2ct::convert_index_designator(), goto_convertt::convert_init(), expr2ct::convert_initializer_list(), goto_program2codet::convert_instruction(), java_bytecode_convert_methodt::convert_instructions(), convert_integer_literal(), smt1_convt::convert_is_dynamic_object(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), goto_convertt::convert_java_try_catch(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), boolbvt::convert_lambda(), expr2ct::convert_malloc(), expr2ct::convert_member(), smt1_convt::convert_member(), smt2_convt::convert_member(), expr2ct::convert_member_designator(), smt1_convt::convert_minus(), smt2_convt::convert_minus(), cvc_convt::convert_minus_expr(), bv_refinementt::convert_mod(), smt1_convt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), bv_refinementt::convert_mult(), smt1_convt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), smt1_convt::convert_nary(), cpp_typecheckt::convert_non_template_declaration(), expr2ct::convert_nondet(), expr2ct::convert_object_descriptor(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cvc_convt::convert_plus_expr(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), expr2ct::convert_pointer_object_has_type(), bv_pointerst::convert_pointer_type(), expr2ct::convert_prob_coin(), expr2ct::convert_prob_uniform(), expr2ct::convert_quantifier(), smt1_convt::convert_relation(), smt2_convt::convert_relation(), dplib_convt::convert_rest(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), goto_convertt::convert_return(), boolbvt::convert_shift(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), expr2ct::convert_statement_expression(), convert_string_literal(), expr2javat::convert_struct(), expr2cppt::convert_struct(), smt1_convt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), cvc_convt::convert_struct_expr(), expr2ct::convert_struct_member_value(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), expr2ct::convert_symbol(), expr2ct::convert_trinary(), goto_convertt::convert_try_catch(), expr2ct::convert_typecast(), smt1_convt::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), cvc_convt::convert_typecast_expr(), expr2ct::convert_unary(), boolbvt::convert_unary_minus(), expr2ct::convert_unary_post(), smt1_convt::convert_union(), expr2ct::convert_union(), smt1_convt::convert_update(), expr2ct::convert_update(), boolbvt::convert_update(), smt2_convt::convert_update(), boolbvt::convert_update_rec(), boolbvt::convert_vector(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), smt1_convt::convert_with(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), cvc_convt::convert_with_expr(), expr2ct::convert_with_precedence(), copy_array(), copy_member(), copy_parent(), copy_to_operands(), cpp_typecheckt::cpp_constructor(), cpp_static_assertt::cpp_static_assertt(), cpp_declarationt::declarators(), ansi_c_declarationt::declarators(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), dereference_exprt::dereference_exprt(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_sett::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), update_exprt::designator(), disjunction(), goto_convertt::do_array_op(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_input(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), cpp_typecheckt::do_not_typechecked(), goto_convertt::do_output(), goto_convertt::do_printf(), goto_convertt::do_scanf(), c_typecheck_baset::do_special_functions(), cpp_typecheckt::do_virtual_table(), does_remove_constt::does_expr_lose_const(), cpp_typecheckt::dtor(), dynamic_object_exprt::dynamic_object_exprt(), custom_bitvector_domaint::eval(), value_sett::eval_pointer_offset(), interpretert::evaluate(), interpretert::evaluate_address(), exists_exprt::exists_exprt(), string_not_contains_constraintt::exists_upper_bound(), path_symex_statet::expand_structs_and_arrays(), cpp_typecheckt::explicit_typecast_ambiguity(), extractbits_exprt::extractbits_exprt(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get_cnf(), qbf_squolem_coret::f_get_dnf(), find_block_position_rec(), code_blockt::find_last_statement(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), goto_convertt::finish_computed_gotos(), flatten_byte_extract(), flatten_byte_update(), goto_checkt::float_overflow_check(), smt2_convt::floatbv_suffix(), forall_exprt::forall_exprt(), bdd_exprt::from_expr_rec(), cpp_typecheckt::full_member_initialization(), function_application_exprt::function_application_exprt(), goto_convertt::generate_conditional_branch(), string_refinementt::get_array(), goto_convertt::get_array_argument(), java_bytecode_convert_methodt::get_array_bounds_check(), prop_conv_solvert::get_bool(), goto_inlinet::get_call(), code_try_catcht::get_catch_code(), code_try_catcht::get_catch_decl(), remove_const_function_pointerst::get_component_value(), rw_range_sett::get_objects_array(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_string_argument_rec(), goto_convertt::get_string_constant(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), bv_refinementt::get_values(), simplify_exprt::get_values(), value_sett::guard(), has_and_or(), has_operands(), code_returnt::has_return_value(), ieee_float_op_exprt::ieee_float_op_exprt(), if_exprt::if_exprt(), invariant_sett::implies_rec(), index_exprt::index_exprt(), dump_ct::insert_local_static_decls(), dump_ct::insert_local_type_decls(), instantiate_quantifier(), path_symex_statet::instantiate_rec(), path_symex_statet::instantiate_rec_address(), cpp_typecheckt::instantiate_template(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), goto_checkt::integer_overflow_check(), inv_object_storet::is_constant_address(), inv_object_storet::is_constant_address_rec(), is_dereference_integer_object(), is_empty(), postconditiont::is_used(), postconditiont::is_used_address_of(), cpp_linkage_spect::items(), cpp_namespace_spect::items(), java_record_outputs(), json(), codet::last_statement(), let_exprt::let_exprt(), lift_if(), string_constraintt::lower_bound(), make_binary(), c_typecheck_baset::make_designator(), value_sett::make_member(), make_not(), make_va_list(), member_exprt::member_exprt(), invariant_sett::modifies(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), move_to_operands(), goto_checkt::nan_check(), negate(), invariant_sett::nnf(), not_exprt::not_exprt(), object_descriptor_exprt::object_descriptor_exprt(), simplify_exprt::objects_equal(), simplify_exprt::objects_equal_address_of(), objects_read(), objects_written(), op0(), op1(), op2(), op3(), operator-=(), cpp_typecheckt::operator_is_overloaded(), operator|=(), or_exprt::or_exprt(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), smt2_convt::parse_struct(), goto_checkt::pointer_overflow_check(), goto_checkt::pointer_rel_check(), printf_formattert::process_format(), Parser::rAllocateExpr(), Parser::rDeclarationStatement(), pointer_arithmetict::read(), memory_model_baset::read_from(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), record_function_outputs(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_cpp_delete(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), remove_vector(), goto_symex_statet::rename(), goto_symext::replace_array_equal(), remove_const_function_pointerst::replace_const_symbols(), java_bytecode_convert_methodt::replace_goto_target(), string_abstractiont::replace_string_macros(), reserve_operands(), goto_convertt::rewrite_boolean(), goto_symext::rewrite_quantifiers(), Parser::rGCCAsmStatement(), Parser::rIfStatement(), Parser::rMemberInit(), object_descriptor_exprt::root_object(), Parser::rPostfixExpr(), Parser::rPrimaryExpr(), Parser::rStatement(), Parser::rTryStatement(), Parser::rTypedefStatement(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), set_class_identifier(), cvc_convt::set_to(), dplib_convt::set_to(), smt1_convt::set_to(), prop_conv_solvert::set_to(), bv_refinementt::set_to(), smt2_convt::set_to(), side_effect_expr_function_callt::side_effect_expr_function_callt(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitnot(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), qdimacs_coret::simplify_extractbits(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_good_pointer(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_cond(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_invalid_pointer(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_unary_plus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), symex_slice_by_tracet::slice_by_trace(), sort_and_join(), invariant_sett::strengthen_rec(), string_exprt::string_exprt(), string_from_ns(), string_refinementt::string_of_array(), smt2_convt::substitute_let(), goto_symext::symex_assign(), goto_symext::symex_assign_array(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_assign_typecast(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_goto(), goto_symext::symex_input(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), goto_symext::symex_output(), goto_symext::symex_printf(), path_symext::symex_va_arg_next(), to_abs_expr(), to_address_of_expr(), string_constantt::to_array_expr(), to_array_of_expr(), to_binary_expr(), to_binary_relation_expr(), to_byte_extract_big_endian_expr(), to_byte_extract_expr(), to_byte_extract_little_endian_expr(), to_byte_update_big_endian_expr(), to_byte_update_expr(), to_byte_update_little_endian_expr(), to_code_assign(), to_code_dead(), to_code_decl(), to_code_dowhile(), to_code_expression(), to_code_for(), to_code_goto(), to_code_ifthenelse(), to_code_label(), to_code_switch(), to_code_switch_case(), to_code_try_catch(), to_code_while(), to_complex_expr(), to_dereference_expr(), to_div_expr(), to_dynamic_object_expr(), to_equal_expr(), ansi_c_languaget::to_expr(), to_extractbit_expr(), to_extractbits_expr(), to_factorial_expr(), to_factorial_power_expr(), to_floatbv_typecast_expr(), to_function_application_expr(), to_ieee_float_equal_expr(), to_ieee_float_notequal_expr(), to_ieee_float_op_expr(), to_if_expr(), to_implies_expr(), to_index_designator(), to_index_expr(), to_isfinite_expr(), to_isinf_expr(), to_isnan_expr(), to_isnormal_expr(), to_let_expr(), to_member_expr(), to_minus_expr(), to_mod_expr(), to_mult_expr(), to_not_expr(), to_notequal_expr(), to_object_descriptor_expr(), to_plus_expr(), to_power_expr(), to_rem_expr(), to_replication_expr(), to_shift_expr(), to_string_constraint(), to_string_expr(), to_string_not_contains_constraint(), to_trans_expr(), to_typecast_expr(), to_unary_expr(), to_unary_minus_expr(), to_union_expr(), to_update_expr(), to_with_expr(), trace_value_binary(), transt::transt(), remove_const_function_pointerst::try_resolve_index_of(), typecast_exprt::typecast_exprt(), c_typecheck_baset::typecheck_asm(), c_typecheck_baset::typecheck_assign(), cpp_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_block(), c_typecheck_baset::typecheck_c_enum_type(), java_bytecode_typecheckt::typecheck_code(), jsil_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), c_typecheck_baset::typecheck_compound_body(), c_typecheck_baset::typecheck_decl(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), c_typecheck_baset::typecheck_dowhile(), jsil_typecheckt::typecheck_exp_binary_equal(), c_typecheck_baset::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), cpp_typecheckt::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), c_typecheck_baset::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), cpp_typecheckt::typecheck_expr_cpp_name(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_new(), java_bytecode_typecheckt::typecheck_expr_java_new_array(), c_typecheck_baset::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_sizeof(), cpp_typecheckt::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_num(), jsil_typecheckt::typecheck_expr_unary_string(), c_typecheck_baset::typecheck_expression(), c_typecheck_baset::typecheck_for(), jsil_typecheckt::typecheck_function_call(), cpp_typecheckt::typecheck_function_expr(), c_typecheck_baset::typecheck_gcc_computed_goto(), c_typecheck_baset::typecheck_gcc_switch_case_range(), c_typecheck_baset::typecheck_ifthenelse(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_start_thread(), c_typecheck_baset::typecheck_switch(), cpp_typecheckt::typecheck_switch(), c_typecheck_baset::typecheck_switch_case(), jsil_typecheckt::typecheck_try_catch(), cpp_typecheckt::typecheck_try_catch(), c_typecheck_baset::typecheck_typeof_type(), c_typecheck_baset::typecheck_while(), unary_exprt::unary_exprt(), unpack_rec(), update_exprt::update_exprt(), with_exprt::with_exprt(), dott::write_dot_subgraph(), xml(), yyansi_cparse(), and zero_initializert::zero_initializer_rec().

§ operands() [2/2]

const operandst& exprt::operands ( ) const
inline

Definition at line 77 of file expr.h.

References irept::find(), and irept::get_sub().

§ reserve_operands()

§ source_location()

const source_locationt& exprt::source_location ( ) const
inline

Definition at line 142 of file expr.h.

References irept::find().

Referenced by string_abstractiont::abstract_assign(), code_contractst::add_contract_check(), cpp_typecheckt::add_implicit_dereference(), adjust_float_expressions(), code_contractst::apply_contract(), build_function_environment(), template_mapt::build_unassigned(), mm2cppt::check_acyclic(), check_apply_invariants(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), cpp_declarator_convertert::combine_types(), cpp_typecheckt::convert(), goto_convertt::convert(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), goto_convertt::convert_assert(), goto_convertt::convert_assume(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_break(), cpp_typecheckt::convert_class_template_specialization(), jsil_convertt::convert_code(), expr2ct::convert_code(), goto_convertt::convert_continue(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_throw(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_decl(), goto_convertt::convert_dowhile(), goto_convertt::convert_expression(), goto_convertt::convert_for(), goto_convertt::convert_gcc_computed_goto(), goto_convertt::convert_goto(), goto_convertt::convert_ifthenelse(), cpp_typecheckt::convert_initializer(), goto_convertt::convert_java_try_catch(), goto_convertt::convert_label(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_finally(), cpp_typecheckt::convert_parameter(), cpp_typecheckt::convert_pmop(), goto_convertt::convert_return(), goto_convertt::convert_skip(), goto_convertt::convert_specc_notify(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), goto_convertt::convert_switch(), cpp_typecheckt::convert_template_declaration(), cpp_typecheckt::convert_template_function_or_member_specialization(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_convertt::copy(), cpp_typecheckt::default_assignop_value(), goto_symext::dereference_rec(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), cpp_typecheckt::explicit_typecast_ambiguity(), find_source_location(), remove_function_pointerst::fix_return_type(), shared_bufferst::flush_read(), remove_asmt::gcc_asm_function_call(), goto_convertt::generate_conditional_branch(), goto_checkt::goto_check(), has_and_or(), cpp_typecheckt::instantiate_template(), interrupt(), shared_bufferst::is_buffered_in_general(), is_empty(), is_not_zero(), remove_instanceoft::lower_instanceof(), mm_io(), cpp_typecheckt::new_temporary(), cpp_typecheckt::operator_is_overloaded(), remove_asmt::process_instruction(), cpp_typecheckt::put_compound_into_scope(), race_check(), cpp_typecheckt::reference_binding(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_cpp_delete(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_malloc(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_side_effect(), goto_symext::replace_nondet(), cpp_typecheck_resolvet::resolve(), rewrite_index(), Parser::rExprStatement(), Parser::rStatement(), simplify_exprt::simplify_typecast(), stack_depth(), cpp_typecheckt::static_typecast(), goto_symext::symex_function_call_code(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_va_arg_next(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), cpp_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_declarator(), c_typecheck_baset::typecheck_custom_type(), c_typecheck_baset::typecheck_decl(), c_typecheck_baset::typecheck_dowhile(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), cpp_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_expr_function_identifier(), java_bytecode_typecheckt::typecheck_expr_java_string_literal(), c_typecheck_baset::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), c_typecheck_baset::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_for(), cpp_typecheckt::typecheck_function_expr(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_goto(), c_typecheck_baset::typecheck_ifthenelse(), c_typecheck_baset::typecheck_label(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), c_typecheck_baset::typecheck_return(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), cpp_typecheckt::typecheck_template_parameters(), c_typecheck_baset::typecheck_while(), cpp_typecheckt::user_defined_conversion_sequence(), and ansi_c_convert_typet::write().

§ subtract()

§ sum()

§ type() [1/2]

typet& exprt::type ( )
inline

Definition at line 60 of file expr.h.

References irept::add().

Referenced by float_bvt::abs(), acceleration_utilst::abstract_arrays(), string_abstractiont::abstract_assign(), string_abstractiont::abstract_char_assign(), string_abstractiont::abstract_pointer_assign(), disjunctive_polynomial_accelerationt::accelerate(), polynomial_acceleratort::accelerate(), guardt::add(), bv_refinementt::add_approximation(), c_typecheck_baset::add_argc_argv(), arrayst::add_array_Ackermann_constraints(), arrayst::add_array_constraints(), arrayst::add_array_constraints_array_of(), arrayst::add_array_constraints_equality(), arrayst::add_array_constraints_if(), arrayst::add_array_constraints_update(), arrayst::add_array_constraints_with(), uninitializedt::add_assertions(), string_constraint_generatort::add_axioms_for_char_at(), string_constraint_generatort::add_axioms_for_char_set(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_code_point_at(), string_constraint_generatort::add_axioms_for_code_point_before(), string_constraint_generatort::add_axioms_for_code_point_count(), string_constraint_generatort::add_axioms_for_compare_to(), string_constraint_generatort::add_axioms_for_concat(), string_constraint_generatort::add_axioms_for_concat_bool(), string_constraint_generatort::add_axioms_for_concat_char(), string_constraint_generatort::add_axioms_for_concat_code_point(), string_constraint_generatort::add_axioms_for_concat_int(), string_constraint_generatort::add_axioms_for_concat_long(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_delete_char_at(), string_constraint_generatort::add_axioms_for_empty_string(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_hash_code(), string_constraint_generatort::add_axioms_for_if(), string_constraint_generatort::add_axioms_for_index_of(), string_constraint_generatort::add_axioms_for_index_of_string(), string_constraint_generatort::add_axioms_for_insert(), string_constraint_generatort::add_axioms_for_insert_bool(), string_constraint_generatort::add_axioms_for_insert_char(), string_constraint_generatort::add_axioms_for_insert_int(), string_constraint_generatort::add_axioms_for_insert_long(), string_constraint_generatort::add_axioms_for_intern(), string_constraint_generatort::add_axioms_for_is_empty(), string_constraint_generatort::add_axioms_for_is_prefix(), string_constraint_generatort::add_axioms_for_is_suffix(), string_constraint_generatort::add_axioms_for_java_char_array(), string_constraint_generatort::add_axioms_for_last_index_of(), string_constraint_generatort::add_axioms_for_last_index_of_string(), string_constraint_generatort::add_axioms_for_offset_by_code_point(), string_constraint_generatort::add_axioms_for_parse_int(), string_constraint_generatort::add_axioms_for_replace(), string_constraint_generatort::add_axioms_for_set_length(), string_constraint_generatort::add_axioms_for_string_expr(), string_constraint_generatort::add_axioms_for_substring(), string_constraint_generatort::add_axioms_for_to_lower_case(), string_constraint_generatort::add_axioms_for_to_upper_case(), string_constraint_generatort::add_axioms_for_trim(), string_constraint_generatort::add_axioms_for_value_of(), string_constraint_generatort::add_axioms_from_bool(), string_constraint_generatort::add_axioms_from_char(), string_constraint_generatort::add_axioms_from_char_array(), string_constraint_generatort::add_axioms_from_float(), string_constraint_generatort::add_axioms_from_int(), string_constraint_generatort::add_axioms_from_int_hex(), string_constraint_generatort::add_axioms_from_literal(), string_constraint_generatort::add_axioms_from_long(), ansi_c_parsert::add_declarator(), cpp_typecheckt::add_implicit_dereference(), bv_minimizet::add_objective(), add_padding(), c_typecheck_baset::add_rounding_mode(), java_bytecode_convert_classt::add_string_type(), float_bvt::add_sub(), cpp_typecheckt::add_this_to_method_type(), pointer_arithmetict::add_to_offset(), invariant_sett::add_type_bounds(), java_bytecode_vtable_factoryt::add_vtable_entry(), add_vtable_pointer_member(), goto_symext::address_arithmetic(), adjust_float_expressions(), c_typecheck_baset::adjust_float_rel(), aliasing(), java_object_factoryt::allocate_nondet_length_array(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), ansi_c_entry_point(), template_mapt::apply(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), cpp_typecheck_resolvet::apply_template_args(), functionst::arguments_equal(), smt1_convt::array_index(), path_symex_statet::array_theory(), as_vcd_binary(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), acceleration_utilst::assign_array(), local_may_aliast::assign_lhs(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), value_sett::assign_rec(), value_set_fit::assign_rec(), goto_symex_statet::assignment(), interval_domaint::assume_rec(), string_exprt::axiom_for_has_length(), string_constraint_generatort::axiom_for_is_positive_index(), string_exprt::axiom_for_is_shorter_than(), string_exprt::axiom_for_is_strictly_longer_than(), base_type(), base_type_eqt::base_type_eq_rec(), float_bvt::bias(), simplify_exprt::bits2expr(), string_refinementt::boolbv_set_equality_to_true(), boolbvt::boolbv_set_equality_to_true(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), ansi_c_declaratort::build(), string_abstractiont::build(), object_descriptor_exprt::build(), build_class_identifier(), build_function_environment(), build_havoc_code(), havoc_loopst::build_havoc_code(), string_abstractiont::build_if(), build_object_descriptor_rec(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), acceleratet::build_state_machine(), inv_object_storet::build_string(), string_abstractiont::build_symbol(), template_mapt::build_template_args(), template_mapt::build_unassigned(), string_abstractiont::build_wrap(), boolbvt::bv_get_cache(), boolbvt::bv_get_unbounded_array(), check_c_implicit_typecast(), acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), goto_checkt::check_rec(), check_renaming(), check_renaming_l1(), bv_refinementt::check_SAT(), bv_refinementt::check_UNSAT(), clean_deref(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), arrayst::collect_arrays(), smt2_convt::collect_bindings(), collect_decisions_rec(), arrayst::collect_indices(), cpp_declarator_convertert::combine_types(), compare_components(), complex_member(), struct_union_typet::component_type(), compute_address_taken_functions(), compute_functions(), compute_pointer_offset(), cpp_typecheckt::const_typecast(), float_bvt::conversion(), goto_checkt::conversion_check(), boolbvt::conversion_failed(), cvc_convt::convert(), float_bvt::convert(), cpp_declarator_convertert::convert(), smt1_convt::convert(), java_bytecode_convert_classt::convert(), smt2_convt::convert(), java_bytecode_convert_methodt::convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), 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(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), boolbvt::convert_array(), expr2ct::convert_array(), dplib_convt::convert_array_index(), cvc_convt::convert_array_index(), boolbvt::convert_array_of(), dplib_convt::convert_as_bv(), cvc_convt::convert_as_bv(), goto_convertt::convert_assign(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), cvc_convt::convert_binary_expr(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), string_refinementt::convert_bool_bv(), boolbvt::convert_bv_literals(), boolbvt::convert_bv_reduction(), boolbvt::convert_bv_rel(), boolbvt::convert_bv_typecast(), expr2ct::convert_byte_extract(), boolbvt::convert_byte_extract(), smt2_convt::convert_byte_extract(), smt1_convt::convert_byte_update(), boolbvt::convert_byte_update(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), boolbvt::convert_case(), character_refine_preprocesst::convert_char_function(), cpp_typecheckt::convert_class_template_specialization(), expr2ct::convert_code_decl(), expr2javat::convert_code_function_call(), character_refine_preprocesst::convert_compare(), cvc_convt::convert_comparison_expr(), boolbvt::convert_complex(), expr2ct::convert_complex(), boolbvt::convert_complex_imag(), boolbvt::convert_complex_real(), dump_ct::convert_compound(), boolbvt::convert_concatenation(), boolbvt::convert_cond(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt1_convt::convert_constant(), smt2_convt::convert_constant(), boolbvt::convert_constant(), expr2ct::convert_constant(), cvc_convt::convert_constant_expr(), boolbvt::convert_constraint_select_one(), goto_convertt::convert_cpp_delete(), expr2cppt::convert_cpp_new(), goto_program2codet::convert_decl(), character_refine_preprocesst::convert_digit_char(), bv_refinementt::convert_div(), smt1_convt::convert_div(), boolbvt::convert_div(), smt2_convt::convert_div(), dplib_convt::convert_dplib_expr(), boolbvt::convert_equality(), cvc_convt::convert_equality_expr(), cvc_convt::convert_expr(), smt1_convt::convert_expr(), smt2_convt::convert_expr(), boolbvt::convert_extractbit(), boolbvt::convert_extractbits(), convert_float_literal(), smt1_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_div(), smt1_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_minus(), smt1_convt::convert_floatbv_mult(), smt2_convt::convert_floatbv_mult(), bv_refinementt::convert_floatbv_op(), boolbvt::convert_floatbv_op(), smt1_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), character_refine_preprocesst::convert_for_digit(), cpp_typecheckt::convert_function(), boolbvt::convert_function_application(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheck_resolvet::convert_identifiers(), boolbvt::convert_ieee_float_rel(), boolbvt::convert_if(), smt1_convt::convert_index(), boolbvt::convert_index(), smt2_convt::convert_index(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), symex_target_equationt::convert_io(), smt1_convt::convert_is_dynamic_object(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), expr2javat::convert_java_new(), boolbvt::convert_lambda(), expr2ct::convert_malloc(), expr2ct::convert_member(), smt1_convt::convert_member(), boolbvt::convert_member(), smt2_convt::convert_member(), smt1_convt::convert_minus(), smt2_convt::convert_minus(), cvc_convt::convert_minus_expr(), bv_refinementt::convert_mod(), smt1_convt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), bv_refinementt::convert_mult(), smt1_convt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), cpp_declarator_convertert::convert_new_symbol(), cpp_typecheckt::convert_non_template_declaration(), expr2ct::convert_nondet(), boolbvt::convert_not(), expr2ct::convert_object_descriptor(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), cpp_typecheckt::convert_parameter(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cvc_convt::convert_plus_expr(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_prob_uniform(), expr2ct::convert_quantifier(), expr2cppt::convert_rec(), smt1_convt::convert_relation(), smt2_convt::convert_relation(), boolbvt::convert_replication(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), goto_convertt::convert_return(), smt2_convt::convert_rounding_mode_FPA(), boolbvt::convert_shift(), convert_string_literal(), expr2javat::convert_struct(), expr2cppt::convert_struct(), smt1_convt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), cvc_convt::convert_struct_expr(), string_refinementt::convert_symbol(), boolbvt::convert_symbol(), expr2ct::convert_symbol(), cpp_typecheckt::convert_template_declaration(), cpp_typecheckt::convert_template_function_or_member_specialization(), cpp_typecheck_resolvet::convert_template_parameter(), character_refine_preprocesst::convert_to_code_point(), smt2_convt::convert_type(), expr2ct::convert_typecast(), smt1_convt::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), cvc_convt::convert_typecast_expr(), boolbvt::convert_unary_minus(), smt1_convt::convert_union(), smt2_convt::convert_union(), boolbvt::convert_union(), boolbvt::convert_update(), boolbvt::convert_update_rec(), boolbvt::convert_vector(), expr2ct::convert_vector(), boolbvt::convert_verilog_case_equality(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), smt1_convt::convert_with(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), cvc_convt::convert_with_expr(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), copy_parent(), count_slots(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), goto_convertt::cpp_new_initializer(), create_initialize(), string_refinementt::dec_solve(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), smt2_convt::define_object_size(), float_bvt::denormalization_shift(), value_set_dereferencet::dereference(), dereferencet::dereference_if(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_sett::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), dereferencet::dereference_typecast(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), float_bvt::div(), goto_checkt::div_by_zero_check(), goto_convertt::do_array_equal(), acceleration_utilst::do_arrays(), acceleration_utilst::do_assumptions(), cpp_typecheck_resolvet::do_builtin(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), value_sett::do_end_function(), value_set_fit::do_end_function(), value_set_fivrnst::do_end_function(), value_set_fivrt::do_end_function(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), value_sett::do_free(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), string_instrumentationt::do_fscanf(), flow_insensitive_analysis_baset::do_function_call(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), remove_returnst::do_function_calls(), c_typecheck_baset::do_initializer(), c_typecheck_baset::do_initializer_list(), c_typecheck_baset::do_initializer_rec(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), acceleration_utilst::do_nonrecursive(), bv_pointerst::do_postponed(), goto_convertt::do_printf(), goto_convertt::do_prob_coin(), goto_convertt::do_prob_uniform(), string_instrumentationt::do_snprintf(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_sprintf(), string_instrumentationt::do_strerror(), c_typecastt::do_typecast(), cpp_typecheckt::do_virtual_table(), does_remove_constt::does_expr_lose_const(), cpp_typecheckt::dtor(), dynamic_object_upper_bound(), cpp_typecheckt::dynamic_typecast(), simplify_exprt::eliminate_common_addends(), equalityt::equality2(), value_sett::eval_pointer_offset(), interpretert::evaluate(), interpretert::evaluate_address(), interpretert::execute_assign(), interpretert::execute_function_call(), path_symex_statet::expand_structs_and_arrays(), cpp_typecheckt::explicit_typecast_ambiguity(), float_bvt::exponent_all_ones(), float_bvt::exponent_all_zeros(), simplify_exprt::expr2bits(), character_refine_preprocesst::expr_of_is_bmp_code_point(), character_refine_preprocesst::expr_of_is_defined(), character_refine_preprocesst::expr_of_is_supplementary_code_point(), character_refine_preprocesst::expr_of_is_valid_code_point(), cpp_typecheck_resolvet::filter_for_named_scopes(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), string_constraint_generatort::find_or_add_string_of_symbol(), find_superclass_with_type(), dplib_convt::find_symbols(), cvc_convt::find_symbols(), find_symbols(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), smt2_convt::find_symbols_rec(), goto_convertt::finish_computed_gotos(), polynomial_acceleratort::fit_const(), polynomial_acceleratort::fit_polynomial_sliced(), remove_function_pointerst::fix_argument_types(), remove_function_pointerst::fix_return_type(), overflow_instrumentert::fix_types(), scratch_programt::fix_types(), fix_types(), smt2_convt::flatten2bv(), smt1_convt::flatten_array(), smt2_convt::flatten_array(), flatten_byte_extract(), flatten_byte_update(), value_set_fit::flatten_rec(), value_set_fivrt::flatten_rec(), goto_checkt::float_overflow_check(), smt2_convt::floatbv_suffix(), float_bvt::fraction_all_zeros(), float_bvt::fraction_rounding_decision(), string_constantt::from_array_expr(), fixedbvt::from_expr(), bv_arithmetict::from_expr(), ieee_floatt::from_expr(), bdd_exprt::from_expr_rec(), from_rational(), float_bvt::from_signed_integer(), float_bvt::from_unsigned_integer(), cpp_typecheckt::full_member_initialization(), ansi_c_declarationt::full_type(), path_symext::function_call_rec(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_pointer_target_init(), smt1_convt::get(), prop_conv_solvert::get(), smt2_convt::get(), float_bvt::rounding_mode_bitst::get(), string_refinementt::get_array(), goto_convertt::get_array_argument(), prop_conv_solvert::get_bool(), invariant_sett::get_bounds(), get_class_identifier_field(), cpp_typecheckt::get_component(), get_component_rec(), remove_const_function_pointerst::get_component_value(), invariant_sett::get_constant(), refined_string_typet::get_index_type(), get_isr(), rw_range_sett::get_objects_array(), rw_range_sett::get_objects_byte_extract(), rw_range_sett::get_objects_complex(), rw_range_sett::get_objects_index(), rw_range_sett::get_objects_member(), invariant_propagationt::get_objects_rec(), rw_range_sett::get_objects_rec(), rw_range_sett::get_objects_shift(), rw_range_sett::get_objects_struct(), rw_range_sett::get_objects_typecast(), goto_symex_statet::get_original_name(), get_quantifier_var_max(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), get_ref(), value_set_fit::get_reference_set(), value_set_fivrt::get_reference_set(), value_sett::get_reference_set_rec(), value_set_fivrnst::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), float_bvt::get_spec(), get_subexpression_at_offset(), symex_slicet::get_symbols(), value_sett::get_value_set(), value_set_fit::get_value_set(), value_set_fivrnst::get_value_set(), value_set_fivrt::get_value_set(), value_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), get_virtual_method_targets(), good_pointer_def(), goto_checkt::goto_check(), goto_rw(), value_sett::guard(), cpp_typecheck_resolvet::guess_function_template_args(), cpp_typecheck_resolvet::guess_template_args(), cpp_declarator_convertert::handle_initializer(), has_and_or(), have_to_adjust_float_expressions(), have_to_remove_complex(), have_to_remove_vector(), rename_symbolt::have_to_rename(), replace_symbolt::have_to_replace(), have_to_rewrite_union(), interval_domaint::havoc_rec(), cpp_typecheckt::implicit_conversion_sequence(), c_typecastt::implicit_typecast(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), c_typecastt::implicit_typecast_arithmetic(), c_typecastt::implicit_typecast_followed(), invariant_sett::implies_rec(), character_refine_preprocesst::in_interval_expr(), character_refine_preprocesst::in_list_expr(), string_refinementt::initial_index_set(), goto_symext::initialize_auto_object(), acceleratet::insert_automaton(), escape_analysist::insert_cleanup(), goto_inlinet::insert_function_nobody(), dump_ct::insert_local_type_decls(), string_refinementt::instantiate(), string_refinementt::instantiate_not_contains(), path_symex_statet::instantiate_rec(), cpp_typecheckt::instantiate_template(), remove_exceptionst::instrument_exception_handler(), remove_exceptionst::instrument_throw(), string_constraint_generatort::int_of_hex_char(), integer_address(), goto_checkt::integer_overflow_check(), string_instrumentationt::invalidate_buffer(), constant_propagator_domaint::valuest::is_array_constant(), is_boolean(), cpp_declarationt::is_class_template(), is_condition(), remove_const_function_pointerst::is_const_expression(), cpp_declarationt::is_constructor(), cpp_declarationt::is_destructor(), pointer_logict::is_dynamic_object(), is_empty(), cpp_declarationt::is_empty(), is_false(), string_constraint_generatort::is_high_surrogate(), string_constraint_generatort::is_low_surrogate(), is_not_zero(), is_one(), is_skip(), path_symex_statet::is_symbol_member_index(), is_true(), refined_string_typet::is_unrefined_string(), float_bvt::is_zero(), is_zero(), java_build_arguments(), java_bytecode_convert_method_lazy(), java_bytecode_promotion(), java_root_class(), java_type_from_string(), json(), lift_if(), float_bvt::limit_distance(), boolbvt::literal(), prop_conv_solvert::literal(), look_through_casts(), template_mapt::lookup(), remove_instanceoft::lower_instanceof(), make_binary(), make_clean_pointer_cast(), goto_convertt::make_compound_literal(), cpp_typecheck_resolvet::make_constructors(), interval_domaint::make_expression(), value_sett::make_member(), make_member_expr(), make_not(), cpp_typecheckt::make_ptr_typecast(), goto_convertt::make_temp_symbol(), printf_formattert::make_type(), string_abstractiont::make_type(), string_instrumentationt::make_type(), jsil_typecheckt::make_type_compatible(), string_abstractiont::make_val_or_dummy_rec(), make_vtable_function(), string_abstractiont::member(), member_offset_expr(), value_set_dereferencet::memory_model(), value_set_dereferencet::memory_model_bytes(), value_set_dereferencet::memory_model_conversion(), cpp_declaratort::merge_type(), mm_io(), goto_checkt::mod_by_zero_check(), string_abstractiont::move_lhs_arithmetic(), mul(), mutex_init_instrumentation(), cpp_declarationt::name_anon_struct_union(), goto_checkt::nan_check(), negate(), float_bvt::negation(), cpp_typecheckt::new_temporary(), invariant_sett::nnf(), nondet_static(), nondet_volatile_rhs(), float_bvt::normalization_shift(), null_object(), null_pointer(), object_lower_bound(), pointer_logict::object_rec(), object_upper_bound(), bv_pointerst::offset_arithmetic(), format_constantt::operator()(), does_remove_constt::operator()(), dereferencet::operator()(), string_exprt::operator[](), cpp_typecheckt::operator_is_overloaded(), cpp_declaratort::output(), cpp_declarationt::output(), value_sett::output(), ansi_c_declarationt::output(), value_set_fit::output(), value_set_fivrt::output(), value_set_fivrnst::output_entry(), overflow_instrumentert::overflow_expr(), float_bvt::pack(), goto_inlinet::parameter_assignments(), goto_symext::parameter_assignments(), smt2_convt::parse_array(), smt2_convt::parse_struct(), smt2_convt::parse_union(), pointer_offset_sum(), goto_checkt::pointer_rel_check(), goto_checkt::pointer_validity_check(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), const_function_pointer_propagationt::propagate(), acceleration_utilst::push_nondet(), cpp_typecheckt::put_compound_into_scope(), Parser::rAllocateExpr(), Parser::rArgDeclaration(), Parser::rCastExpr(), java_bytecode_parsert::rClassFile(), Parser::rConstructorDecl(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), pointer_arithmetict::read(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), path_symex_statet::read_symbol_member_index(), cpp_convert_typet::read_template(), arrayst::record_array_equality(), value_set_fivrt::recursive_find(), cpp_typecheckt::reference_binding(), cpp_typecheckt::reference_compatible(), cpp_typecheckt::reference_related(), cpp_typecheckt::reinterpret_typecast(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_cpp_new(), goto_convertt::remove_function_call(), remove_function_pointerst::remove_function_pointer(), goto_convertt::remove_gcc_conditional_expression(), goto_convertt::remove_malloc(), goto_convertt::remove_post(), goto_convertt::remove_pre(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), remove_vector(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbol_extt::replace(), replace_symbolt::replace(), goto_symext::replace_array_equal(), constant_propagator_ait::replace_array_symbol(), goto_symext::replace_nondet(), goto_inlinet::replace_return(), remove_returnst::replace_returns(), constant_propagator_ait::replace_types_rec(), cpp_typecheck_resolvet::resolve(), goto_symext::return_assignment(), rewrite_assignment(), rewrite_index(), rewrite_union(), Parser::rIntegralDeclaration(), Parser::rIntegralDeclStatement(), java_bytecode_parsert::rmethod_attribute(), Parser::rOtherDeclaration(), Parser::rOtherDeclStatement(), float_bvt::round_exponent(), float_bvt::round_fraction(), Parser::rPrimaryExpr(), Parser::rSimpleDeclaration(), Parser::rTempArgDeclaration(), Parser::rTemplateArgs(), Parser::rTypedef(), Parser::rTypedefUsing(), Parser::rTypeName(), goto_program2codet::scan_for_varargs(), template_mapt::set(), set_class_identifier(), cvc_convt::set_to(), dplib_convt::set_to(), boolbvt::set_to(), smt1_convt::set_to(), prop_conv_solvert::set_to(), bv_refinementt::set_to(), smt2_convt::set_to(), string_constantt::set_value(), java_bytecode_vtable_factoryt::set_vtable_value(), cpp_typecheck_resolvet::show_identifiers(), float_bvt::sign_bit(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_address_of(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_bitnot(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_bswap(), simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_dereference(), simplify_exprt::simplify_div(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_implies(), simplify_exprt::simplify_if_recursive(), simplify_exprt::simplify_index(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_member(), simplify_exprt::simplify_minus(), simplify_exprt::simplify_mod(), simplify_exprt::simplify_mult(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_object_size(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_pointer_object(), simplify_exprt::simplify_pointer_offset(), simplify_exprt::simplify_popcount(), simplify_exprt::simplify_power(), simplify_exprt::simplify_shifts(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), size_of_expr(), c_sizeoft::sizeof_rec(), sort_and_join(), stack_depth(), cpp_typecheckt::standard_conversion_array_to_pointer(), cpp_typecheckt::standard_conversion_boolean(), cpp_typecheckt::standard_conversion_floating_integral_conversion(), cpp_typecheckt::standard_conversion_floating_point_conversion(), cpp_typecheckt::standard_conversion_floating_point_promotion(), cpp_typecheckt::standard_conversion_integral_conversion(), cpp_typecheckt::standard_conversion_integral_promotion(), cpp_typecheckt::standard_conversion_lvalue_to_rvalue(), cpp_typecheckt::standard_conversion_pointer(), cpp_typecheckt::standard_conversion_pointer_to_member(), cpp_typecheckt::standard_conversion_qualification(), cpp_typecheckt::standard_conversion_sequence(), cpp_typecheckt::static_typecast(), float_bvt::sticky_right_shift(), postconditiont::strengthen(), invariant_sett::strengthen_rec(), smt1_dect::string_to_expr_z3(), substitute_rec(), subtract(), float_bvt::subtract_exponents(), sum(), goto_symext::symex_assign_array(), goto_symext::symex_assign_byte_extract(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_assign_symbol(), goto_symext::symex_assign_typecast(), goto_symext::symex_cpp_new(), goto_symext::symex_dead(), goto_symext::symex_decl(), goto_symext::symex_function_call_code(), goto_symext::symex_gcc_builtin_va_arg_next(), path_symext::symex_malloc(), goto_symext::symex_malloc(), goto_symext::symex_other(), path_symext::symex_va_arg_next(), template_parametert::template_parametert(), cpp_typecheckt::template_suffix(), cpp_typecheckt::this_struct_type(), string_constantt::to_array_expr(), ansi_c_languaget::to_expr(), value_sett::to_expr(), value_set_fit::to_expr(), value_set_fivrt::to_expr(), value_set_fivrnst::to_expr(), to_integer(), float_bvt::to_integer(), to_member(), jsil_declarationt::to_symbol(), to_update_expr(), trace_value_binary(), custom_bitvector_domaint::transform(), c_typecheck_baset::typecheck_arithmetic_pointer(), c_typecheck_baset::typecheck_array_type(), jsil_typecheckt::typecheck_assign(), c_typecheck_baset::typecheck_assign(), c_typecheck_baset::typecheck_c_enum_type(), cpp_typecheckt::typecheck_cast_expr(), cpp_typecheckt::typecheck_class_template(), java_bytecode_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code(), cpp_typecheckt::typecheck_code(), c_typecheck_baset::typecheck_code_type(), cpp_typecheckt::typecheck_compound_bases(), c_typecheck_baset::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_compound_declarator(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_declaration(), cpp_typecheckt::typecheck_enum_body(), jsil_typecheckt::typecheck_exp_binary_equal(), java_bytecode_typecheckt::typecheck_expr(), cpp_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_address_of(), cpp_typecheckt::typecheck_expr_address_of(), c_typecheck_baset::typecheck_expr_alignof(), jsil_typecheckt::typecheck_expr_base(), jsil_typecheckt::typecheck_expr_binary_arith(), c_typecheck_baset::typecheck_expr_binary_arithmetic(), jsil_typecheckt::typecheck_expr_binary_boolean(), c_typecheck_baset::typecheck_expr_binary_boolean(), jsil_typecheckt::typecheck_expr_binary_compare(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), c_typecheck_baset::typecheck_expr_builtin_va_arg(), c_typecheck_baset::typecheck_expr_comma(), cpp_typecheckt::typecheck_expr_comma(), jsil_typecheckt::typecheck_expr_concatenation(), jsil_typecheckt::typecheck_expr_constant(), cpp_typecheckt::typecheck_expr_cpp_name(), c_typecheck_baset::typecheck_expr_cw_va_arg_typeof(), jsil_typecheckt::typecheck_expr_delete(), cpp_typecheckt::typecheck_expr_delete(), c_typecheck_baset::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_dereference(), cpp_typecheckt::typecheck_expr_explicit_constructor_call(), cpp_typecheckt::typecheck_expr_explicit_typecast(), jsil_typecheckt::typecheck_expr_field(), c_typecheck_baset::typecheck_expr_function_identifier(), jsil_typecheckt::typecheck_expr_has_field(), jsil_typecheckt::typecheck_expr_index(), c_typecheck_baset::typecheck_expr_index(), java_bytecode_typecheckt::typecheck_expr_java_new(), java_bytecode_typecheckt::typecheck_expr_java_new_array(), jsil_typecheckt::typecheck_expr_main(), c_typecheck_baset::typecheck_expr_main(), cpp_typecheckt::typecheck_expr_main(), java_bytecode_typecheckt::typecheck_expr_member(), c_typecheck_baset::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_member(), cpp_typecheckt::typecheck_expr_new(), c_typecheck_baset::typecheck_expr_pointer_arithmetic(), jsil_typecheckt::typecheck_expr_proto_field(), jsil_typecheckt::typecheck_expr_proto_obj(), c_typecheck_baset::typecheck_expr_ptrmember(), cpp_typecheckt::typecheck_expr_ptrmember(), jsil_typecheckt::typecheck_expr_ref(), c_typecheck_baset::typecheck_expr_rel(), c_typecheck_baset::typecheck_expr_rel_vector(), c_typecheck_baset::typecheck_expr_shifts(), c_typecheck_baset::typecheck_expr_side_effect(), c_typecheck_baset::typecheck_expr_sizeof(), jsil_typecheckt::typecheck_expr_subtype(), java_bytecode_typecheckt::typecheck_expr_symbol(), c_typecheck_baset::typecheck_expr_symbol(), cpp_typecheckt::typecheck_expr_this(), cpp_typecheckt::typecheck_expr_throw(), c_typecheck_baset::typecheck_expr_trinary(), cpp_typecheckt::typecheck_expr_trinary(), c_typecheck_baset::typecheck_expr_typecast(), c_typecheck_baset::typecheck_expr_unary_arithmetic(), jsil_typecheckt::typecheck_expr_unary_boolean(), c_typecheck_baset::typecheck_expr_unary_boolean(), jsil_typecheckt::typecheck_expr_unary_string(), cpp_typecheckt::typecheck_friend_declaration(), c_typecheck_baset::typecheck_function_body(), c_typecheck_baset::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_call_arguments(), cpp_typecheckt::typecheck_function_expr(), cpp_typecheckt::typecheck_function_template(), c_typecheck_baset::typecheck_gcc_computed_goto(), cpp_typecheckt::typecheck_member_function(), cpp_typecheckt::typecheck_member_initializer(), cpp_typecheckt::typecheck_method_application(), c_typecheck_baset::typecheck_return(), c_typecheck_baset::typecheck_side_effect_assignment(), cpp_typecheckt::typecheck_side_effect_assignment(), c_typecheck_baset::typecheck_side_effect_function_call(), cpp_typecheckt::typecheck_side_effect_function_call(), c_typecheck_baset::typecheck_side_effect_gcc_conditional_expression(), cpp_typecheckt::typecheck_side_effect_inc_dec(), c_typecheck_baset::typecheck_side_effect_statement_expression(), c_typecheck_baset::typecheck_switch(), jsil_typecheckt::typecheck_symbol_expr(), cpp_typecheckt::typecheck_template_args(), cpp_typecheckt::typecheck_template_parameters(), cpp_typecheckt::typecheck_try_catch(), cpp_typecheckt::typecheck_type(), c_typecheck_baset::typecheck_typeof_type(), goto_checkt::undefined_shift_check(), remove_returnst::undo_function_calls(), unpack_rec(), jsil_typecheckt::update_expr_type(), string_refinementt::update_index_set(), ssa_exprt::update_type(), smt2_convt::use_array_theory(), cpp_typecheckt::user_defined_conversion_sequence(), string_abstractiont::value_assignments(), java_bytecode_convert_methodt::variable(), postconditiont::weaken(), wp_decl(), shared_bufferst::write(), xml(), yyansi_cparse(), yyjsilparse(), cpp_typecheckt::zero_initializer(), and zero_initializert::zero_initializer_rec().

§ type() [2/2]

const typet& exprt::type ( ) const
inline

Definition at line 61 of file expr.h.

References irept::find().

§ visit() [1/2]

void exprt::visit ( class expr_visitort visitor)

Definition at line 483 of file expr.cpp.

References Forall_operands, and stack.

Referenced by find_expr(), find_index(), find_qvar(), and slice_global_inits().

§ visit() [2/2]

void exprt::visit ( class const_expr_visitort visitor) const

Definition at line 501 of file expr.cpp.

References forall_operands, and stack.


The documentation for this class was generated from the following files: