cprover
|
Base class for all expressions. More...
#include <expr.h>
Public Types | |
typedef std::vector< exprt > | operandst |
![]() | |
typedef std::vector< irept > | subt |
typedef std::map< irep_namet, irept > | named_subt |
Public Member Functions | |
exprt () | |
exprt (const irep_idt &_id) | |
exprt (const irep_idt &_id, const typet &_type) | |
typet & | type () |
const typet & | type () const |
bool | has_operands () const |
operandst & | operands () |
const operandst & | operands () const |
exprt & | op0 () |
exprt & | op1 () |
exprt & | op2 () |
exprt & | op3 () |
const exprt & | op0 () const |
const exprt & | op1 () const |
const exprt & | op2 () const |
const exprt & | op3 () 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) |
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_locationt & | find_source_location () const |
const source_locationt & | source_location () const |
source_locationt & | add_source_location () |
exprt & | add_expr (const irep_idt &name) |
const exprt & | find_expr (const irep_idt &name) const |
void | visit (class expr_visitort &visitor) |
void | visit (class const_expr_visitort &visitor) const |
depth_iteratort | depth_begin () |
depth_iteratort | depth_end () |
const_depth_iteratort | depth_begin () const |
const_depth_iteratort | depth_end () const |
const_depth_iteratort | depth_cbegin () const |
const_depth_iteratort | depth_cend () const |
depth_iteratort | depth_begin (std::function< exprt &()> mutate_root) const |
const_unique_depth_iteratort | unique_depth_begin () const |
const_unique_depth_iteratort | unique_depth_end () const |
const_unique_depth_iteratort | unique_depth_cbegin () const |
const_unique_depth_iteratort | unique_depth_cend () const |
![]() | |
bool | is_nil () const |
bool | is_not_nil () const |
irept (const irep_idt &_id) | |
irept () | |
irept (const irept &irep) | |
irept (irept &&irep) | |
irept & | operator= (const irept &irep) |
irept & | operator= (irept &&irep) |
~irept () | |
const irep_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_namet &name) const |
irept & | add (const irep_namet &name) |
irept & | add (const irep_namet &name, const irept &irep) |
const std::string & | get_string (const irep_namet &name) const |
const irep_idt & | get (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 () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_named_sub () const |
named_subt & | get_comments () |
const named_subt & | get_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 dt & | read () const |
dt & | write () |
Additional Inherited Members | |
![]() | |
void | detach () |
![]() | |
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... | |
![]() | |
dt * | data |
![]() | |
static dt | empty_d |
typedef std::vector<exprt> exprt::operandst |
|
inline |
Definition at line 48 of file expr.h.
Referenced by make_bool(), make_false(), make_not(), and make_true().
Definition at line 50 of file expr.h.
References irept::add().
Definition at line 135 of file expr.h.
References irept::add().
Referenced by code_typet::parametert::default_value().
|
inline |
Definition at line 130 of file expr.h.
References irept::add().
Referenced by string_abstractiont::abstract_pointer_assign(), code_blockt::add(), cpp_typecheckt::add_implicit_dereference(), adjust_float_expressions(), allocate_dynamic_object(), allocate_dynamic_object_with_decl(), java_object_factoryt::allocate_nondet_length_array(), symbol_factoryt::allocate_object(), cpp_typecheck_resolvet::apply_template_args(), ansi_c_declaratort::build(), c_nondet_symbol_factory(), goto_checkt::check_rec(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), cpp_declarator_convertert::combine_types(), cpp_typecheckt::convert_anon_struct_union_member(), java_bytecode_convert_methodt::convert_astore(), java_bytecode_convert_methodt::convert_athrow(), java_bytecode_convert_methodt::convert_checkcast(), 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(), java_bytecode_convert_methodt::convert_if(), java_bytecode_convert_methodt::convert_if_cmp(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), goto_convertt::convert_ifthenelse(), java_bytecode_convert_methodt::convert_iinc(), java_bytecode_convert_methodt::convert_invoke(), goto_program2codet::convert_labels(), goto_convertt::convert_msc_leave(), java_bytecode_convert_methodt::convert_new(), java_bytecode_convert_methodt::convert_putstatic(), java_bytecode_convert_methodt::convert_ret(), goto_program2codet::convert_start_thread(), java_bytecode_convert_methodt::convert_switch(), cpp_typecheck_resolvet::convert_template_parameter(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), cpp_declaratort::cpp_declaratort(), cpp_typecheckt::cpp_destructor(), create_fatal_assertion(), java_simple_method_stubst::create_method_stub(), declare_created_symbols(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), goto_convertt::do_array_op(), goto_convertt::do_cpp_new(), c_typecheck_baset::do_designated_initializer(), goto_convertt::do_function_call_other(), goto_convertt::do_function_call_symbol(), 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(), c_typecheck_baset::do_special_functions(), cpp_typecheckt::dtor(), cpp_typecheckt::explicit_typecast_ambiguity(), expr_initializert< nondet >::expr_initializer_rec(), goto_convertt::finish_gotos(), 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(), generate_ansi_c_start_function(), generate_java_start_function(), cpp_typecheckt::get_component(), java_object_factoryt::get_null_assignment(), get_thread_safe_clinit_wrapper_body(), escape_analysist::insert_cleanup(), dump_ct::insert_local_type_decls(), instrument_end_thread(), instrument_get_current_thread_id(), interrupt(), java_bytecode_instrument_uncaught_exceptions(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), remove_java_newt::lower_java_new_array(), linker_script_merget::ls_data2instructions(), goto_convertt::make_compound_literal(), goto_convertt::make_temp_symbol(), merge_source_location_rec(), cpp_typecheckt::new_temporary(), goto_convertt::new_tmp_symbol(), 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_delete(), 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(), java_bytecode_convert_methodt::replace_call_to_cprover_assume(), linker_script_merget::replace_expr(), replace_location(), goto_symext::replace_nondet(), cpp_typecheck_resolvet::resolve(), rewrite_index(), Parser::rExprStatement(), Parser::rStatement(), Parser::rTemplateArgs(), parsert::set_source_location(), side_effect_exprt::side_effect_exprt(), simplify_exprt::simplify_typecast(), static_lifetime_init(), java_bytecode_instrumentt::throw_exception(), c_typecheck_baset::typecheck_array_type(), 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_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(), and cpp_typecheckt::zero_initializer().
void exprt::copy_to_operands | ( | const exprt & | expr | ) |
Definition at line 55 of file expr.cpp.
References operands().
Referenced by guardt::add(), code_blockt::add(), code_try_catcht::add_catch(), pointer_arithmetict::add_to_offset(), allocate_dynamic_object(), java_object_factoryt::allocate_nondet_length_array(), java_object_factoryt::allocate_object(), already_typechecked(), and_exprt::and_exprt(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), binary_exprt::binary_exprt(), bitand_exprt::bitand_exprt(), bitor_exprt::bitor_exprt(), buffer_size(), byte_update_exprt::byte_update_exprt(), code_asmt::code_asmt(), code_assertt::code_assertt(), java_string_library_preprocesst::code_assign_components_to_java_string(), code_assignt::code_assignt(), code_assumet::code_assumet(), code_deadt::code_deadt(), code_declt::code_declt(), code_expressiont::code_expressiont(), code_landingpadt::code_landingpadt(), 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(), goto_program2codet::convert_assign_rec(), java_bytecode_convert_methodt::convert_athrow(), goto_program2codet::convert_decl(), cpp_typecheckt::convert_function(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_if(), cpp_typecheck_resolvet::convert_identifier(), java_bytecode_convert_methodt::convert_iinc(), goto_program2codet::convert_instruction(), java_bytecode_convert_methodt::convert_instructions(), goto_program2codet::convert_labels(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_newarray(), java_bytecode_convert_methodt::convert_putfield(), java_bytecode_convert_methodt::convert_putstatic(), goto_program2codet::convert_return(), copy_array(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), create_fatal_assertion(), java_simple_method_stubst::create_method_stub(), java_bytecode_convert_methodt::create_stack_tmp_var(), cpp_typecheckt::default_cpctor(), goto_convertt::do_array_op(), acceleration_utilst::do_arrays(), c_typecheck_baset::do_designated_initializer(), goto_convertt::do_function_call_symbol(), dynamic_object(), expr_initializert< nondet >::expr_initializer_rec(), character_refine_preprocesst::expr_of_to_chars(), extractbits_exprt::extractbits_exprt(), flatten_byte_extract(), floatbv_mult(), 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(), generate_java_start_function(), get_or_create_string_literal_symbol(), ieee_float_op_exprt::ieee_float_op_exprt(), if_exprt::if_exprt(), index_designatort::index_designatort(), java_bytecode_instrumentt::instrument_code(), instrument_start_thread(), instrument_synchronized_code(), is_digit_with_radix(), is_zero_string(), java_static_lifetime_init(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), make_allocate_code(), java_string_library_preprocesst::make_argument_for_format(), multi_ary_exprt::multi_ary_exprt(), cpp_typecheckt::operator_is_overloaded(), or_exprt::or_exprt(), predicate_exprt::predicate_exprt(), java_bytecode_instrumentt::prepend_instrumentation(), cpp_typecheckt::reference_binding(), refined_string_exprt::refined_string_exprt(), float_bvt::relation(), goto_convertt::remove_assignment(), goto_convertt::remove_post(), goto_convertt::remove_pre(), simplify_exprt::simplify_index(), simplify_exprt::simplify_plus(), cpp_typecheckt::static_and_dynamic_initialization(), cpp_typecheckt::static_typecast(), string_not_contains_constraintt::string_not_contains_constraintt(), goto_symext::symex_assign_byte_extract(), goto_symext::symex_macro(), java_bytecode_instrumentt::throw_exception(), cpp_typecheckt::typecheck_class_template_member(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_expr_dereference(), 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(), and zero_string_length().
Definition at line 60 of file expr.cpp.
References operands().
Definition at line 70 of file expr.cpp.
References operands().
depth_iteratort exprt::depth_begin | ( | ) |
Definition at line 299 of file expr.cpp.
Referenced by string_refinementt::add_lemma(), convert_threadblock(), extract_strings(), find_indexes(), string_constraintt::gather_indices(), require_goto_statements::get_all_statements(), has_subexpr(), initial_index_set(), string_constraintt::is_linear_arithmetic_expr(), references_class_model(), rename_symbolt::rename(), replace_expr(), and string_constraintt::universal_only_in_index().
const_depth_iteratort exprt::depth_begin | ( | ) | const |
depth_iteratort exprt::depth_begin | ( | std::function< exprt &()> | mutate_root | ) | const |
const_depth_iteratort exprt::depth_cbegin | ( | ) | const |
Definition at line 307 of file expr.cpp.
Referenced by notify_static_method_calls().
const_depth_iteratort exprt::depth_cend | ( | ) | const |
Definition at line 309 of file expr.cpp.
Referenced by notify_static_method_calls().
depth_iteratort exprt::depth_end | ( | ) |
Definition at line 301 of file expr.cpp.
Referenced by string_refinementt::add_lemma(), convert_threadblock(), extract_strings(), find_indexes(), string_constraintt::gather_indices(), require_goto_statements::get_all_statements(), has_subexpr(), initial_index_set(), string_constraintt::is_linear_arithmetic_expr(), references_class_model(), rename_symbolt::rename(), replace_expr(), and string_constraintt::universal_only_in_index().
const_depth_iteratort exprt::depth_end | ( | ) | const |
Definition at line 140 of file expr.h.
References irept::find().
Referenced by code_typet::parametert::default_value().
const source_locationt & exprt::find_source_location | ( | ) | const |
Definition at line 246 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_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(), goto_convertt::convert_return(), boolbvt::convert_struct(), bv_cbmct::convert_waitfor(), 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(), linkingt::duplicate_object_symbol(), typecheckt::err_location(), goto_convertt::finish_gotos(), goto_checkt::float_overflow_check(), goto_convertt::get_array_argument(), goto_convertt::get_string_constant(), c_typecheck_baset::implicit_typecast(), cpp_typecheckt::implicit_typecast(), goto_checkt::integer_overflow_check(), 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(), does_remove_constt::operator()(), 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_cpp_new(), 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(), goto_convertt::rewrite_boolean(), c_typecheck_baset::typecheck_array_type(), 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().
|
inline |
Definition at line 63 of file expr.h.
References operands().
Referenced by bracket_subexpression(), goto_program2codet::cleanup_code(), boolbvt::convert_array(), cpp_typecheckt::convert_function(), goto_program2codet::convert_goto_while(), cpp_typecheckt::convert_non_template_declaration(), expr2ct::convert_sizeof(), interpretert::evaluate(), fallback_format_rec(), find_block_position_rec(), codet::first_statement(), format_rec(), uncaught_exceptions_domaint::get_exception_symbol(), cpp_declarationt::is_empty(), codet::last_statement(), move_label_ifthenelse(), simplify_exprt::simplify_bitnot(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_if_cond(), simplify_exprt::simplify_node(), simplify_exprt::simplify_node_preorder(), sort_and_join(), to_literal_expr(), to_member_designator(), to_nondet_symbol_expr(), smt2_convt::to_smt2_symbol(), to_ssa_expr(), to_symbol_expr(), uncaught_exceptions_domaint::transform(), and cpp_typecheckt::typecheck_member_function().
bool exprt::is_boolean | ( | ) | const |
Definition at line 156 of file expr.cpp.
References irept::id(), and type().
Referenced by goto_checkt::check_rec(), goto_convertt::clean_expr(), goto_program_dereferencet::dereference_rec(), and goto_convertt::rewrite_boolean().
bool exprt::is_constant | ( | ) | const |
Definition at line 119 of file expr.cpp.
References irept::id().
Referenced by constant_propagator_domaint::assign_rec(), 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(), 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(), eval_string(), bv_arithmetict::from_expr(), bdd_exprt::from_expr_rec(), invariant_sett::get_constant(), value_set_fit::get_value_set_rec(), value_sett::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(), format_constantt::operator()(), smt2_convt::parse_struct(), replace_symbolt::replace(), 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_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(), substitute_array_lists(), goto_symext::symex_allocate(), to_integer(), custom_bitvector_domaint::transform(), c_typecheck_baset::typecheck_array_type(), c_typecheck_baset::typecheck_expr_trinary(), and c_typecheck_baset::typecheck_redefinition_non_type().
bool exprt::is_false | ( | ) | const |
Definition at line 131 of file expr.cpp.
References irept::id(), is_constant(), and type().
Referenced by guardt::add(), boolean_negate(), custom_bitvector_analysist::check(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_code_ifthenelse(), cfg_baset< cfg_nodet >::compute_edges(), symex_slice_by_tracet::compute_ts_back(), smt2_convt::convert(), cpp_typecheckt::convert(), prop_conv_solvert::convert_bool(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt2_convt::convert_constant(), format_rec(), 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(), goto_programt::get_successors(), guardt::guard_expr(), instantiate_quantifier(), string_constraintt::is_valid_string_constraint(), 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(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_not(), simplify_exprt::simplify_typecast(), static_verifier(), invariant_sett::strengthen_rec(), goto_symext::symex_allocate(), 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(), symex_bmct::symex_step(), goto_symext::symex_step(), cpp_typecheckt::template_suffix(), constant_propagator_domaint::transform(), custom_bitvector_domaint::transform(), and c_typecheck_baset::typecheck_c_enum_type().
bool exprt::is_one | ( | ) | const |
Definition at line 205 of file expr.cpp.
References binary2integer(), CHECK_RETURN, irept::get_string(), irept::id_string(), is_constant(), rationalt::is_one(), string2integer(), to_constant_expr(), to_rational(), and type().
Referenced by simplify_exprt::simplify_div(), and simplify_exprt::simplify_floatbv_op().
bool exprt::is_true | ( | ) | const |
Definition at line 124 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(), as_string(), boolean_negate(), local_cfgt::build(), sat_path_enumeratort::build_path(), disjunctive_polynomial_accelerationt::build_path(), custom_bitvector_analysist::check(), goto_convertt::clean_expr(), goto_program2codet::cleanup_code_ifthenelse(), goto_program2codet::cleanup_expr(), cfg_baset< cfg_nodet >::compute_edges_goto(), show_goto_functions_jsont::convert(), smt2_convt::convert(), cpp_typecheckt::convert(), prop_conv_solvert::convert_bool(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt2_convt::convert_constant(), expr2ct::convert_constant(), goto_program2codet::convert_goto_break_continue(), goto_program2codet::convert_goto_while(), goto_program_dereferencet::dereference_failure(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::do_free(), eval_string(), interpretert::evaluate(), format_rec(), prop_conv_solvert::get_bool(), rw_range_sett::get_objects_if(), rw_guarded_range_set_value_sett::get_objects_if(), goto_programt::get_successors(), guardt::guard_expr(), goto_symext::havoc_rec(), invariant_sett::implies_rec(), instantiate_quantifier(), instrument_intervals(), json(), goto_symex_statet::l2_thread_read_encoding(), goto_symext::loop_bound_exceeded(), make_not(), invariant_sett::nnf(), taint_analysist::operator()(), operator|=(), goto_programt::output_instruction(), sat_path_enumeratort::record_path(), disjunctive_polynomial_accelerationt::record_path(), simplify_exprt::simplify_address_of_arg(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_not(), simplify_exprt::simplify_typecast(), symex_slice_by_tracet::slice_SSA_steps(), static_verifier(), 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_numeric_value(), c_typecheck_baset::typecheck_c_enum_type(), goto_symext::vcc(), and xml().
bool exprt::is_zero | ( | ) | const |
Definition at line 161 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(), smt2_convt::convert_address_of_rec(), expr2ct::convert_complex(), expr2javat::convert_constant(), expr2ct::convert_with_precedence(), dereferencet::dereference_typecast(), c_typecheck_baset::do_designated_initializer(), simplify_exprt::eliminate_common_addends(), format_rec(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_set_fivrnst::get_reference_set_rec(), value_sett::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(), goto_symext::process_array_expr(), pointer_arithmetict::read(), dereferencet::read_object(), cpp_typecheckt::reinterpret_typecast(), 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(), goto_symext::symex_allocate(), c_typecheck_baset::typecheck_expr_rel(), and cpp_typecheckt::typecheck_method_bodies().
void exprt::make_bool | ( | bool | value | ) |
Definition at line 138 of file expr.cpp.
References exprt().
Referenced by simplify_exprt::simplify_boolean(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_extractbit(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_address_of(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_isinf(), simplify_exprt::simplify_isnan(), simplify_exprt::simplify_isnormal(), simplify_exprt::simplify_sign(), simplify_exprt::simplify_typecast(), and c_typecheck_baset::typecheck_expr_main().
void exprt::make_false | ( | ) |
Definition at line 150 of file expr.cpp.
References exprt().
Referenced by get_quantifier_var_max(), get_quantifier_var_min(), memory_model_tsot::program_order(), goto_symext::symex_goto(), and goto_unwindt::unwind().
void exprt::make_not | ( | ) |
Definition at line 91 of file expr.cpp.
References exprt(), is_false(), is_true(), move_to_operands(), operands(), irept::swap(), and type().
Referenced by symex_slice_by_tracet::compute_ts_back(), goto_convertt::convert_for(), bv_cbmct::convert_waitfor(), goto_program_dereferencet::dereference_failure(), goto_program_dereferencet::dereference_rec(), eval_expr(), flow_insensitive_abstract_domain_baset::get_guard(), static_analysis_baset::get_guard(), guardt::guard_expr(), symex_slice_by_tracet::implies_false(), value_set_dereferencet::memory_model_conversion(), goto_checkt::nan_check(), invariant_sett::nnf(), operator|=(), sign_of_expr(), simplify_exprt::simplify_boolean(), simplify_exprt::simplify_ieee_float_relation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_inequality_not_constant(), simplify_exprt::simplify_not(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), goto_symext::symex_goto(), goto_symext::symex_step_goto(), custom_bitvector_domaint::transform(), and invariant_set_domaint::transform().
void exprt::make_true | ( | ) |
Definition at line 144 of file expr.cpp.
References exprt().
Referenced by interval_domaint::ai_simplify(), symex_slice_by_tracet::assign_merges(), rw_guarded_range_set_value_sett::get_objects_rec(), guardt::guardt(), operator|=(), and symex_slice_by_tracet::slice_by_trace().
void exprt::make_typecast | ( | const typet & | _type | ) |
Definition at line 84 of file expr.cpp.
References irept::swap().
Referenced by pointer_arithmetict::add_to_offset(), functionst::arguments_equal(), goto_checkt::bounds_check(), value_set_dereferencet::build_reference_to(), build_sizeof_expr(), java_bytecode_instrumentt::check_class_cast(), goto_program2codet::cleanup_expr(), cpp_typecheckt::convert(), goto_convertt::convert(), goto_convertt::convert_assign(), boolbvt::convert_byte_extract(), java_bytecode_convert_methodt::convert_iinc(), java_bytecode_convert_methodt::convert_switch(), java_bytecode_convert_methodt::convert_ushr(), dereferencet::dereference_plus(), goto_convertt::do_cpp_new(), goto_convertt::do_function_call_symbol(), parameter_assignmentst::do_function_calls(), c_typecastt::do_typecast(), dynamic_object_upper_bound(), flatten_byte_update(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), goto_checkt::goto_check(), cpp_typecheck_resolvet::guess_template_args(), escape_analysist::insert_cleanup(), lower_popcount(), linker_script_merget::ls_data2instructions(), 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(), pointer_offset_sum(), goto_symext::process_array_expr(), 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(), java_bytecode_convert_methodt::replace_call_to_cprover_assume(), goto_inlinet::replace_return(), 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_allocate(), goto_symext::symex_assign_typecast(), goto_symext::symex_gcc_builtin_va_arg_next(), goto_symext::symex_other(), 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(), and c_typecheck_baset::typecheck_side_effect_assignment().
void exprt::move_to_operands | ( | exprt & | expr | ) |
Definition at line 22 of file expr.cpp.
References get_nil_irep(), and operands().
Referenced by java_bytecode_instrumentt::add_expr_instrumentation(), goto_checkt::add_guarded_claim(), java_object_factoryt::allocate_nondet_length_array(), simplify_exprt::bits2expr(), goto_convertt::case_guard(), goto_program2codet::cleanup_code_ifthenelse(), dump_ct::cleanup_expr(), clinit_wrapper_do_recursive_calls(), symex_slice_by_tracet::compute_ts_back(), cpp_typecheckt::convert_anonymous_union(), goto_program2codet::convert_assign_varargs(), java_bytecode_convert_methodt::convert_athrow(), 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(), java_bytecode_convert_methodt::convert_invoke(), goto_program2codet::convert_labels(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), java_bytecode_convert_methodt::convert_newarray(), java_bytecode_convert_methodt::convert_putstatic(), java_bytecode_convert_methodt::convert_ret(), goto_program2codet::convert_start_thread(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), cpp_typecheckt::default_cpctor(), cpp_typecheckt::default_ctor(), cpp_typecheckt::default_dtor(), java_bytecode_convert_methodt::do_exception_handling(), 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(), generate_ansi_c_start_function(), generate_java_start_function(), get_clinit_wrapper_body(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), get_or_create_string_literal_symbol(), instrument_synchronized_code(), java_bytecode_instrument_uncaught_exceptions(), java_record_outputs(), java_static_lifetime_init(), jsil_entry_point(), codet::make_block(), make_not(), monitor_exits(), code_blockt::move(), 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(), Parser::rEqualityExpr(), 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(), symex_slice_by_tracet::slice_by_trace(), cpp_typecheckt::static_and_dynamic_initialization(), static_lifetime_init(), goto_symext::symex_cpp_new(), java_bytecode_instrumentt::throw_exception(), c_typecheck_baset::typecheck_block(), cpp_typecheckt::typecheck_compound_body(), cpp_typecheckt::typecheck_decl(), c_typecheck_baset::typecheck_dowhile(), cpp_typecheckt::typecheck_expr_explicit_typecast(), c_typecheck_baset::typecheck_expr_index(), cpp_typecheckt::typecheck_expr_new(), cpp_typecheckt::typecheck_expr_ptrmember(), 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().
Definition at line 29 of file expr.cpp.
References get_nil_irep(), and operands().
Definition at line 41 of file expr.cpp.
References get_nil_irep(), and operands().
|
inline |
Definition at line 72 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_with(), 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(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), index_exprt::array(), array_name(), bv_refinementt::arrays_overapproximated(), as_vcd_binary(), code_assertt::assertion(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), acceleration_utilst::assign_array(), value_set_fit::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), code_assumet::assumption(), boolean_negate(), goto_checkt::bounds_check(), value_set_dereferencet::bounds_check(), string_abstractiont::build(), build_full_lhs_rec(), inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), c_nondet_symbol_factory(), ssa_exprt::can_build_identifier(), goto_convertt::case_guard(), code_switch_caset::case_op(), code_landingpadt::catch_expr(), 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(), preconditiont::compute_rec(), symex_slice_by_tracet::compute_ts_back(), 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_add_sub(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), expr2ct::convert_array_member_value(), expr2ct::convert_array_of(), boolbvt::convert_array_of(), goto_convertt::convert_assign(), expr2ct::convert_binary(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), expr2ct::convert_byte_update(), boolbvt::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(), expr2ct::convert_complex(), boolbvt::convert_complex_imag(), boolbvt::convert_complex_real(), expr2ct::convert_constant(), 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(), smt2_convt::convert_div(), boolbvt::convert_div(), goto_convertt::convert_dowhile(), smt2_convt::convert_expr(), goto_convertt::convert_expression(), expr2cppt::convert_extractbit(), expr2ct::convert_extractbit(), 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(), boolbvt::convert_floatbv_typecast(), cpp_typecheckt::convert_function(), goto_convertt::convert_gcc_switch_case_range(), 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(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), goto_convertt::convert_label(), boolbvt::convert_lambda(), expr2ct::convert_let(), expr2ct::convert_member(), smt2_convt::convert_minus(), boolbvt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), boolbvt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_object_descriptor(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_prob_coin(), expr2ct::convert_prob_uniform(), expr2ct::convert_quantifier(), smt2_convt::convert_relation(), boolbvt::convert_replication(), boolbvt::convert_rest(), boolbvt::convert_shift(), expr2ct::convert_statement_expression(), smt2_convt::convert_struct(), expr2ct::convert_struct_member_value(), expr2ct::convert_symbol(), expr2ct::convert_trinary(), goto_convertt::convert_try_catch(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), expr2ct::convert_unary(), boolbvt::convert_unary_minus(), expr2ct::convert_unary_post(), boolbvt::convert_union(), expr2ct::convert_union(), expr2ct::convert_update(), boolbvt::convert_update_rec(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), 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(), goto_program_dereferencet::dereference_instruction(), dereferencet::dereference_plus(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), value_sett::dereference_rec(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), 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(), 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(), 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(), require_goto_statements::find_struct_component_assignments(), smt2_convt::find_symbols(), require_goto_statements::find_this_component_assignment(), 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(), format_rec(), polynomialt::from_expr(), bdd_exprt::from_expr_rec(), side_effect_expr_function_callt::function(), function_application_exprt::function(), function_application_exprt::function_application_exprt(), acceleration_utilst::gather_array_accesses(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_pointer_target_init(), generate_ansi_c_start_function(), goto_convertt::generate_conditional_branch(), goto_convertt::get_array_argument(), prop_conv_solvert::get_bool(), goto_convertt::get_constant(), uncaught_exceptions_domaint::get_exception_symbol(), dynamic_object_exprt::get_instance(), get_null_checked_expr(), 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_set_fivrnst::get_reference_set_rec(), value_sett::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_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), goto_checkt::goto_check(), value_sett::guard(), guardt::guard_expr(), cpp_typecheckt::implicit_typecast(), invariant_sett::implies_rec(), index_designatort::index(), code_fort::init(), initial_index_set(), instantiate_quantifier(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), instrument_end_thread(), java_bytecode_instrumentt::instrument_expr(), instrument_start_thread(), goto_checkt::integer_overflow_check(), transt::invar(), inv_object_storet::is_constant_address(), inv_object_storet::is_constant_address_rec(), is_dereference_integer_object(), is_index_member_symbol(), local_safe_pointerst::is_non_null_at_program_point(), local_safe_pointerst::is_safe_dereference(), postconditiont::is_used(), postconditiont::is_used_address_of(), java_record_outputs(), json(), refined_string_exprt::length(), let_exprt::let_exprt(), code_assignt::lhs(), binary_relation_exprt::lhs(), code_function_callt::lhs(), ieee_float_op_exprt::lhs(), linker_script_merget::linker_script_merget(), boolbvt::literal(), look_through_casts(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), array_poolt::make_char_array_for_char_pointer(), make_clean_pointer_cast(), c_typecheck_baset::make_designator(), value_sett::make_member(), make_va_list(), map_representation_of_sum(), invariant_sett::modifies(), string_abstractiont::move_lhs_arithmetic(), goto_checkt::nan_check(), invariant_sett::nnf(), object_descriptor_exprt::object(), address_of_exprt::object(), object_descriptor_exprt::object_descriptor_exprt(), 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(), floatbv_typecast_exprt::op(), shift_exprt::op(), cpp_typecheckt::operator_is_overloaded(), or_exprt::or_exprt(), goto_programt::output_instruction(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), dereference_exprt::pointer(), goto_checkt::pointer_rel_check(), goto_symext::process_array_expr(), printf_formattert::process_format(), remove_asmt::process_instruction_gcc(), remove_asmt::process_instruction_msc(), acceleration_utilst::push_nondet(), smt2_parsert::quantifier_expression(), quantifier_exprt::quantifier_exprt(), Parser::rDeclarationStatement(), pointer_arithmetict::read(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), complex_exprt::real(), 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_inlinet::replace_return(), remove_returnst::replace_returns(), 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_checkt::rw_ok_check(), set_class_identifier(), dynamic_object_exprt::set_instance(), 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_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_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_json_expr(), 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_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(), extractbit_exprt::src(), extractbits_exprt::src(), cpp_typecheckt::static_typecast(), invariant_sett::strengthen_rec(), string_from_ns(), member_exprt::struct_op(), sum_overflows(), code_declt::symbol(), code_deadt::symbol(), member_exprt::symbol(), let_exprt::symbol(), quantifier_exprt::symbol(), goto_symext::symex_allocate(), 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(), goto_symext::symex_other(), goto_symext::symex_output(), thread_exit_instrumentation(), replication_exprt::times(), to_bswap_expr(), ansi_c_languaget::to_expr(), trace_numeric_value(), 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(), 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(), update_index_set(), cpp_typecheckt::user_defined_conversion_sequence(), code_switcht::value(), array_of_exprt::what(), xml(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 84 of file expr.h.
References operands().
|
inline |
Definition at line 75 of file expr.h.
References operands().
Referenced by bv_refinementt::add_approximation(), arrayst::add_array_Ackermann_constraints(), string_abstractiont::add_dummy_symbol_and_value(), pointer_arithmetict::add_to_offset(), adjust_float_expressions(), and_exprt::and_exprt(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), 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(), interval_domaint::assume_rec(), code_switcht::body(), code_whilet::body(), code_dowhilet::body(), goto_checkt::bounds_check(), cpp_typecheck_fargst::build(), string_abstractiont::build_symbol_constant(), 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(), code_fort::cond(), refined_string_exprt::content(), float_bvt::convert(), cpp_typecheckt::convert(), goto_convertt::convert(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), goto_convertt::convert_assign(), expr2ct::convert_binary(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), 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(), expr2ct::convert_complex(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), bv_refinementt::convert_div(), smt2_convt::convert_div(), boolbvt::convert_div(), goto_convertt::convert_dowhile(), smt2_convt::convert_expr(), expr2cppt::convert_extractbit(), expr2ct::convert_extractbit(), 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(), smt2_convt::convert_floatbv_typecast(), goto_convertt::convert_gcc_switch_case_range(), expr2ct::convert_Hoare(), boolbvt::convert_ieee_float_rel(), goto_convertt::convert_ifthenelse(), expr2ct::convert_index(), convert_integer_literal(), expr2javat::convert_java_instanceof(), boolbvt::convert_lambda(), smt2_convt::convert_minus(), bv_refinementt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_finally(), smt2_convt::convert_mult(), expr2ct::convert_object_descriptor(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_quantifier(), smt2_convt::convert_relation(), boolbvt::convert_replication(), boolbvt::convert_rest(), boolbvt::convert_shift(), expr2ct::convert_trinary(), expr2ct::convert_update(), boolbvt::convert_update(), bv_cbmct::convert_waitfor(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), copy_array(), copy_member(), copy_parent(), cpp_typecheckt::cpp_constructor(), goto_program_dereferencet::dereference_instruction(), 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(), 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(), 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(), generate_ansi_c_start_function(), goto_convertt::get_constant(), get_null_checked_expr(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_set_fivrnst::get_reference_set_rec(), value_sett::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_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), simplify_exprt::get_values(), guardt::guard_expr(), complex_exprt::imag(), invariant_sett::implies_rec(), index_exprt::index(), extractbit_exprt::index(), transt::init(), initial_index_set(), instantiate_quantifier(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), java_bytecode_instrumentt::instrument_expr(), goto_checkt::integer_overflow_check(), inv_object_storet::is_constant_address_rec(), postconditiont::is_used_address_of(), java_record_outputs(), linker_script_merget::linker_script_merget(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new_array(), value_sett::make_member(), map_representation_of_sum(), mmio(), 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(), or_exprt::or_exprt(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), pointer_offset_sum(), goto_checkt::pointer_rel_check(), acceleration_utilst::push_nondet(), smt2_parsert::quantifier_expression(), pointer_arithmetict::read(), _rw_set_loct::read_write_rec(), record_function_outputs(), goto_convertt::remove_assignment(), remove_complex(), goto_convertt::remove_function_call(), goto_convertt::remove_gcc_conditional_expression(), remove_vector(), 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(), goto_checkt::rw_ok_check(), prop_conv_solvert::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_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(), symex_slice_by_tracet::slice_SSA_steps(), invariant_sett::strengthen_rec(), sum_overflows(), goto_symext::symex_allocate(), goto_symext::symex_assign_rec(), goto_symext::symex_assign_struct_member(), goto_symext::symex_macro(), goto_symext::symex_other(), code_ifthenelset::then_case(), thread_exit_instrumentation(), custom_bitvector_domaint::transform(), 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(), string_not_contains_constraintt::univ_upper_bound(), update_exprt::update_exprt(), update_index_set(), extractbits_exprt::upper(), dynamic_object_exprt::valid(), let_exprt::value(), shared_bufferst::cfg_visitort::weak_memory(), with_exprt::where(), quantifier_exprt::where(), and shared_bufferst::write().
|
inline |
Definition at line 87 of file expr.h.
References operands().
|
inline |
Definition at line 78 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_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), 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(), smt2_convt::convert_address_of_rec(), expr2ct::convert_byte_update(), smt2_convt::convert_byte_update(), expr2ct::convert_code_asm(), expr2ct::convert_code_for(), 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_trinary(), expr2ct::convert_update(), boolbvt::convert_update(), bv_cbmct::convert_waitfor(), smt2_convt::convert_with(), goto_program_dereferencet::dereference_instruction(), goto_program_dereferencet::dereference_rec(), code_ifthenelset::else_case(), interpretert::evaluate(), interpretert::evaluate_address(), if_exprt::false_case(), flatten_byte_update(), remove_asmt::gcc_asm_function_call(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), code_ifthenelset::has_else_case(), code_fort::iter(), extractbits_exprt::lower(), value_sett::make_member(), invariant_sett::modifies(), with_exprt::new_value(), update_exprt::new_value(), objects_written(), 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_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_index(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_with(), goto_symext::symex_macro(), goto_symext::symex_other(), 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(), byte_update_exprt::value(), and let_exprt::where().
|
inline |
Definition at line 90 of file expr.h.
References operands().
|
inline |
Definition at line 81 of file expr.h.
References operands().
Referenced by and_exprt::and_exprt(), code_fort::body(), expr2ct::convert_code_asm(), bv_cbmct::convert_waitfor(), string_not_contains_constraintt::exists_lower_bound(), or_exprt::or_exprt(), goto_symext::symex_macro(), and c_typecheck_baset::typecheck_for().
|
inline |
Definition at line 93 of file expr.h.
References operands().
|
inline |
Definition at line 66 of file expr.h.
References 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(), allocate_dynamic_object_with_decl(), and_exprt::and_exprt(), code_blockt::append(), invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), 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_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), value_set_fit::assign_rec(), value_sett::assign_rec(), interval_domaint::assume_rec(), base_type_eqt::base_type_eq_rec(), binary_exprt::binary_exprt(), boolean_negate(), cpp_typecheck_fargst::build(), string_abstractiont::build(), build_full_lhs_rec(), inv_object_storet::build_string(), string_abstractiont::build_symbol_constant(), boolbvt::bv_get_rec(), byte_update_exprt::byte_update_exprt(), c_nondet_symbol_factory(), goto_convertt::case_guard(), 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_landingpadt::code_landingpadt(), 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(), preconditiont::compute_rec(), symex_slice_by_tracet::compute_ts_back(), conjunction(), goto_symex_statet::constant_propagation_reference(), contains_instanceof(), goto_checkt::conversion_check(), show_goto_functions_jsont::convert(), goto_convertt::convert(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), 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(), boolbvt::convert_bv_rel(), expr2ct::convert_byte_extract(), expr2ct::convert_byte_update(), boolbvt::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(), 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(), 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(), smt2_convt::convert_div(), goto_convertt::convert_dowhile(), goto_convertt::convert_end_thread(), 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(), smt2_convt::convert_floatbv(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), bv_refinementt::convert_floatbv_op(), boolbvt::convert_floatbv_op(), 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(), 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(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), goto_convertt::convert_label(), goto_program2codet::convert_labels(), boolbvt::convert_lambda(), expr2ct::convert_let(), expr2ct::convert_member(), smt2_convt::convert_member(), expr2ct::convert_member_designator(), smt2_convt::convert_minus(), bv_refinementt::convert_mod(), smt2_convt::convert_mod(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), bv_refinementt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), expr2ct::convert_multi_ary(), cpp_typecheckt::convert_non_template_declaration(), expr2ct::convert_nondet(), expr2ct::convert_object_descriptor(), expr2ct::convert_overflow(), boolbvt::convert_overflow(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), expr2ct::convert_prob_coin(), expr2ct::convert_prob_uniform(), expr2ct::convert_quantifier(), smt2_convt::convert_relation(), bv_pointerst::convert_rest(), boolbvt::convert_rest(), goto_convertt::convert_return(), expr2ct::convert_statement_expression(), convert_string_literal(), expr2javat::convert_struct(), expr2cppt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), expr2ct::convert_struct_member_value(), expr2ct::convert_symbol(), expr2ct::convert_trinary(), goto_convertt::convert_try_catch(), expr2ct::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), expr2ct::convert_unary(), boolbvt::convert_unary_minus(), expr2ct::convert_unary_post(), expr2ct::convert_union(), 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(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), expr2ct::convert_with_precedence(), copy_array(), copy_member(), copy_parent(), copy_to_operands(), cpp_typecheckt::cpp_constructor(), cpp_static_assertt::cpp_static_assertt(), create_fatal_assertion(), java_simple_method_stubst::create_method_stub_at(), cpp_declarationt::declarators(), ansi_c_declarationt::declarators(), cpp_typecheckt::default_assignop(), cpp_typecheckt::default_assignop_value(), cpp_typecheckt::default_cpctor(), smt2_solvert::define_constants(), goto_program_dereferencet::dereference_instruction(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), value_sett::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_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(), custom_bitvector_domaint::eval(), value_sett::eval_pointer_offset(), eval_string(), interpretert::evaluate(), interpretert::evaluate_address(), string_not_contains_constraintt::exists_upper_bound(), smt2_solvert::expand_function_applications(), cpp_typecheckt::explicit_typecast_ambiguity(), expr_initializert< nondet >::expr_initializer_rec(), extractbits_exprt::extractbits_exprt(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get_cnf(), qbf_squolem_coret::f_get_dnf(), fallback_format_rec(), find_block_position_rec(), code_blockt::find_last_statement(), smt2_convt::find_symbols(), goto_convertt::finish_computed_gotos(), flatten_byte_extract(), flatten_byte_update(), goto_checkt::float_overflow_check(), smt2_convt::floatbv_suffix(), format_rec(), bdd_exprt::from_expr_rec(), cpp_typecheckt::full_member_initialization(), ci_lazy_methodst::gather_virtual_callsites(), generate_ansi_c_start_function(), goto_convertt::generate_conditional_branch(), prop_conv_solvert::get(), goto_convertt::get_array_argument(), prop_conv_solvert::get_bool(), code_try_catcht::get_catch_code(), code_try_catcht::get_catch_decl(), get_component_in_struct(), remove_const_function_pointerst::get_component_value(), rw_range_sett::get_objects_array(), java_bytecode_convert_methodt::get_or_create_block_for_pcrange(), get_or_create_string_literal_symbol(), get_quantifier_var_max(), get_quantifier_var_min(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_set_fivrnst::get_reference_set_rec(), value_sett::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(), get_sub_arrays(), value_set_fit::get_value_set_rec(), value_sett::get_value_set_rec(), bv_refinementt::get_values(), simplify_exprt::get_values(), goto_checkt::goto_check(), value_sett::guard(), has_operands(), code_returnt::has_return_value(), ieee_float_op_exprt::ieee_float_op_exprt(), if_exprt::if_exprt(), cpp_typecheckt::implicit_typecast(), invariant_sett::implies_rec(), initial_index_set(), initialize_nondet_string_fields(), dump_ct::insert_local_static_decls(), dump_ct::insert_local_type_decls(), insert_nondet_init_code(), instantiate_quantifier(), cpp_typecheckt::instantiate_template(), mm2cppt::instruction2cpp(), taint_analysist::instrument(), java_bytecode_instrumentt::instrument_code(), goto_checkt::integer_overflow_check(), interval_sparse_arrayt::interval_sparse_arrayt(), inv_object_storet::is_constant_address(), inv_object_storet::is_constant_address_rec(), is_dereference_integer_object(), is_typecast_with_id(), postconditiont::is_used(), postconditiont::is_used_address_of(), cpp_linkage_spect::items(), cpp_namespace_spect::items(), java_record_outputs(), java_root_class_init(), json(), codet::last_statement(), let_exprt::let_exprt(), lift_if(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), make_binary(), c_typecheck_baset::make_designator(), value_sett::make_member(), make_not(), make_string(), make_va_list(), map_representation_of_sum(), merge_source_location_rec(), invariant_sett::modifies(), move_label_ifthenelse(), cpp_typecheckt::move_member_initializers(), move_to_operands(), depth_iterator_baset< const_depth_iteratort >::mutate(), goto_checkt::nan_check(), invariant_sett::nnf(), 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(), goto_programt::output_instruction(), overflow_instrumentert::overflow_expr(), parse_lhs_read(), goto_checkt::pointer_overflow_check(), goto_checkt::pointer_rel_check(), linker_script_merget::pointerize_subexprs_of(), printf_formattert::process_format(), depth_iterator_baset< const_depth_iteratort >::push_expr(), 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(), refined_string_exprt::refined_string_exprt(), 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(), 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(), goto_checkt::rw_ok_check(), string_not_contains_constraintt::s0(), string_not_contains_constraintt::s1(), java_bytecode_convert_methodt::save_stack_entries(), set_class_identifier(), prop_conv_solvert::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_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_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_json_expr(), 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_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_from_ns(), substitute_array_access_in_place(), substitute_array_lists(), smt2_convt::substitute_let(), sum_overflows(), linker_script_merget::symbols_to_pointerize(), goto_symext::symex_allocate(), 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(), goto_symext::symex_other(), goto_symext::symex_output(), goto_symext::symex_printf(), to_abs_expr(), to_address_of_expr(), string_constantt::to_array_expr(), to_array_of_expr(), to_binary_expr(), to_binary_relation_expr(), to_bswap_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_popcount_expr(), to_power_expr(), to_quantifier_expr(), to_rem_expr(), to_replication_expr(), to_shift_expr(), 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_numeric_value(), custom_bitvector_domaint::transform(), transt::transt(), remove_const_function_pointerst::try_resolve_index_of(), c_typecheck_baset::typecheck_asm(), c_typecheck_baset::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(), utf16_constant_array_to_java(), validate_expr(), validate_operands(), with_exprt::with_exprt(), dott::write_dot_subgraph(), xml(), and yyansi_cparse().
|
inline |
Definition at line 69 of file expr.h.
References irept::get_sub().
|
inline |
Definition at line 96 of file expr.h.
References operands().
Referenced by simplify_exprt::bits2expr(), boolbvt::bv_get_rec(), goto_convertt::case_guard(), code_blockt::code_blockt(), cpp_typecheckt::convert_anonymous_union(), goto_program2codet::operator()(), float_bvt::relation(), Parser::rForStatement(), goto_symext::symex_fkt(), cpp_typecheckt::typecheck_decl(), and c_typecheck_baset::typecheck_for().
|
inline |
Definition at line 125 of file expr.h.
References irept::find().
Referenced by string_abstractiont::abstract_assign(), polynomial_acceleratort::accelerate(), code_contractst::add_contract_check(), cpp_typecheckt::add_implicit_dereference(), adjust_float_expressions(), acceleration_utilst::assign_array(), build_function_environment(), template_mapt::build_unassigned(), mm2cppt::check_acyclic(), check_apply_invariants(), goto_checkt::check_rec(), goto_convertt::clean_expr(), goto_program2codet::cleanup_expr(), cpp_declarator_convertert::combine_types(), show_goto_functions_jsont::convert(), show_goto_functions_xmlt::convert(), 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_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(), java_bytecode_convert_methodt::convert_instructions(), 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_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(), value_set_dereferencet::dereference(), 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(), c_typecheck_baset::do_special_functions(), string_instrumentationt::do_strerror(), cpp_typecheckt::explicit_typecast_ambiguity(), expr_initializert< nondet >::expr_initializer_rec(), find_source_location(), remove_function_pointerst::fix_return_type(), shared_bufferst::flush_read(), remove_asmt::gcc_asm_function_call(), java_object_factoryt::gen_nondet_pointer_init(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_thread_block(), get_or_create_string_literal_symbol(), havoc_generate_function_bodiest::havoc_expr_rec(), goto_symext::initialize_auto_object(), cpp_typecheckt::instantiate_template(), java_bytecode_instrumentt::instrument_code(), instrument_end_thread(), java_bytecode_instrumentt::instrument_expr(), instrument_get_current_thread_id(), instrument_intervals(), instrument_start_thread(), interrupt(), shared_bufferst::is_buffered_in_general(), is_not_zero(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), make_allocate_code(), mm_io(), remove_asmt::msc_asm_function_call(), cpp_typecheckt::new_temporary(), nondet_volatile_rhs(), cpp_typecheckt::operator_is_overloaded(), remove_asmt::process_instruction_gcc(), remove_asmt::process_instruction_msc(), acceleration_utilst::push_nondet(), cpp_typecheckt::put_compound_into_scope(), race_check(), Parser::rAttribute(), 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(), linker_script_merget::replace_expr(), goto_symext::replace_nondet(), cpp_typecheck_resolvet::resolve(), rewrite_index(), rewrite_union(), Parser::rExprStatement(), Parser::rStatement(), simplify_exprt::simplify_typecast(), stack_depth(), cpp_typecheckt::static_typecast(), goto_symext::symex_allocate(), goto_symext::symex_function_call_code(), goto_symext::symex_gcc_builtin_va_arg_next(), jsil_declarationt::to_symbol(), ansi_c_declarationt::to_symbol(), 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(), 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_sizeof(), 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().
|
inline |
Definition at line 56 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(), actuals_replace_map(), 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_characters_in_integer_string(), 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_char(), string_constraint_generatort::add_axioms_for_concat_substr(), string_constraint_generatort::add_axioms_for_constant(), string_constraint_generatort::add_axioms_for_constrain_characters(), string_constraint_generatort::add_axioms_for_contains(), string_constraint_generatort::add_axioms_for_copy(), string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_delete(), string_constraint_generatort::add_axioms_for_equals(), string_constraint_generatort::add_axioms_for_equals_ignore_case(), string_constraint_generatort::add_axioms_for_format(), string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_hash_code(), 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_is_prefix(), 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_char(), string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_for_string_of_int(), string_constraint_generatort::add_axioms_for_string_of_int_with_radix(), 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_from_float_scientific_notation(), add_character_set_constraint(), string_constraint_generatort::add_constraint_on_characters(), ansi_c_parsert::add_declarator(), add_dependency_to_string_subexprs(), cpp_typecheckt::add_implicit_dereference(), bv_minimizet::add_objective(), add_padding(), add_pointer_to_array_association(), c_typecheck_baset::add_rounding_mode(), add_string_equation_to_symbol_resolution(), float_bvt::add_sub(), cpp_typecheckt::add_this_to_method_type(), pointer_arithmetict::add_to_offset(), invariant_sett::add_type_bounds(), goto_symext::address_arithmetic(), goto_checkt::address_check(), adjust_float_expressions(), c_typecheck_baset::adjust_float_rel(), custom_bitvector_analysist::aliases(), aliasing(), allocate_dynamic_object(), allocate_dynamic_object_with_decl(), java_object_factoryt::allocate_nondet_length_array(), symbol_factoryt::allocate_object(), java_object_factoryt::allocate_object(), template_mapt::apply(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), cpp_typecheck_resolvet::apply_template_args(), functionst::arguments_equal(), as_vcd_binary(), disjunctive_polynomial_accelerationt::assert_for_values(), polynomial_acceleratort::assert_for_values(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), acceleration_utilst::assign_array(), local_may_aliast::assign_lhs(), constant_propagator_domaint::assign_rec(), value_set_fit::assign_rec(), value_sett::assign_rec(), custom_bitvector_domaint::assign_struct_rec(), goto_symex_statet::assignment(), string_constraint_generatort::associate_array_to_pointer(), string_constraint_generatort::associate_length_to_array(), interval_domaint::assume_rec(), string_exprt< array_string_exprt >::axiom_for_has_length(), string_constraint_generatort::axiom_for_is_positive_index(), string_exprt< array_string_exprt >::axiom_for_length_ge(), string_exprt< array_string_exprt >::axiom_for_length_gt(), string_exprt< array_string_exprt >::axiom_for_length_le(), string_exprt< array_string_exprt >::axiom_for_length_lt(), base_type(), base_type_eqt::base_type_eq_rec(), float_bvt::bias(), simplify_exprt::bits2expr(), 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(), cannot_be_neg(), smt2_parsert::cast_bv_to_unsigned(), java_bytecode_instrumentt::check_arithmetic_exception(), check_axioms(), check_c_implicit_typecast(), java_bytecode_instrumentt::check_class_cast(), acceleration_utilst::check_inductive(), polynomial_acceleratort::check_inductive(), java_bytecode_instrumentt::check_null_dereference(), 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(), java_string_library_preprocesst::code_assign_components_to_java_string(), code_assign_function_application(), java_string_library_preprocesst::code_assign_java_string_to_string_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(), struct_union_typet::componentt::componentt(), compute_address_taken_functions(), compute_functions(), compute_inverse_function(), compute_pointer_offset(), interval_sparse_arrayt::concretize(), typecast_exprt::conditional_cast(), cpp_typecheckt::const_typecast(), float_bvt::conversion(), goto_checkt::conversion_check(), boolbvt::conversion_failed(), float_bvt::convert(), cpp_declarator_convertert::convert(), smt2_convt::convert(), java_bytecode_convert_classt::convert(), boolbvt::convert_abs(), boolbvt::convert_add_sub(), bv_pointerst::convert_address_of_rec(), smt2_convt::convert_address_of_rec(), expr2ct::convert_allocate(), java_bytecode_convert_methodt::convert_aload(), cpp_typecheckt::convert_anon_struct_union_member(), cpp_typecheckt::convert_anonymous_union(), boolbvt::convert_array(), expr2ct::convert_array(), boolbvt::convert_array_of(), goto_convertt::convert_assign(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), java_bytecode_convert_methodt::convert_astore(), bv_pointerst::convert_bitvector(), boolbvt::convert_bitvector(), boolbvt::convert_bitwise(), prop_conv_solvert::convert_bool(), boolbvt::convert_bswap(), 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(), expr2ct::convert_byte_update(), boolbvt::convert_byte_update(), smt2_convt::convert_byte_update(), boolbvt::convert_case(), cpp_typecheckt::convert_class_template_specialization(), expr2ct::convert_code_decl(), expr2javat::convert_code_function_call(), boolbvt::convert_complex(), expr2ct::convert_complex(), boolbvt::convert_complex_imag(), boolbvt::convert_complex_real(), dump_ct::convert_compound(), boolbvt::convert_concatenation(), boolbvt::convert_cond(), java_bytecode_convert_methodt::convert_const(), expr2javat::convert_constant(), expr2cppt::convert_constant(), smt2_convt::convert_constant(), boolbvt::convert_constant(), expr2ct::convert_constant(), 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(), smt2_convt::convert_div(), boolbvt::convert_div(), boolbvt::convert_equality(), smt2_convt::convert_expr(), java_string_library_preprocesst::convert_exprt_to_string_exprt(), boolbvt::convert_extractbits(), convert_float_literal(), smt2_convt::convert_floatbv_div(), smt2_convt::convert_floatbv_minus(), smt2_convt::convert_floatbv_mult(), bv_refinementt::convert_floatbv_op(), boolbvt::convert_floatbv_op(), smt2_convt::convert_floatbv_plus(), smt2_convt::convert_floatbv_typecast(), boolbvt::convert_floatbv_typecast(), cpp_typecheckt::convert_function(), boolbvt::convert_function_application(), goto_convertt::convert_gcc_switch_case_range(), java_bytecode_convert_methodt::convert_getstatic(), cpp_typecheck_resolvet::convert_identifier(), cpp_typecheck_resolvet::convert_identifiers(), boolbvt::convert_ieee_float_rel(), boolbvt::convert_if(), java_bytecode_convert_methodt::convert_ifnonull(), java_bytecode_convert_methodt::convert_ifnull(), java_bytecode_convert_methodt::convert_iinc(), boolbvt::convert_index(), smt2_convt::convert_index(), cpp_typecheckt::convert_initializer(), java_bytecode_convert_methodt::convert_instructions(), java_bytecode_convert_methodt::convert_invoke(), java_bytecode_convert_methodt::convert_invoke_dynamic(), symex_target_equationt::convert_io(), smt2_convt::convert_is_dynamic_object(), expr2javat::convert_java_instanceof(), expr2javat::convert_java_new(), boolbvt::convert_lambda(), boolbvt::convert_let(), expr2ct::convert_member(), boolbvt::convert_member(), smt2_convt::convert_member(), smt2_convt::convert_minus(), bv_refinementt::convert_mod(), boolbvt::convert_mod(), smt2_convt::convert_mod(), bv_refinementt::convert_mult(), boolbvt::convert_mult(), smt2_convt::convert_mult(), java_bytecode_convert_methodt::convert_multianewarray(), java_bytecode_convert_methodt::convert_new(), cpp_declarator_convertert::convert_new_symbol(), java_bytecode_convert_methodt::convert_newarray(), 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(), smt2_convt::convert_plus(), cpp_typecheckt::convert_pmop(), expr2ct::convert_pointer_arithmetic(), expr2ct::convert_pointer_difference(), bv_pointerst::convert_pointer_type(), boolbvt::convert_power(), expr2ct::convert_prob_uniform(), java_bytecode_convert_methodt::convert_putstatic(), expr2ct::convert_quantifier(), expr2cppt::convert_rec(), 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(), java_bytecode_convert_methodt::convert_store(), convert_string_literal(), expr2javat::convert_struct(), expr2cppt::convert_struct(), boolbvt::convert_struct(), smt2_convt::convert_struct(), expr2ct::convert_struct(), java_bytecode_convert_methodt::convert_switch(), 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(), smt2_convt::convert_type(), expr2ct::convert_typecast(), boolbvt::convert_typecast(), smt2_convt::convert_typecast(), boolbvt::convert_unary_minus(), smt2_convt::convert_union(), boolbvt::convert_union(), boolbvt::convert_update(), boolbvt::convert_update_rec(), java_bytecode_convert_methodt::convert_ushr(), boolbvt::convert_vector(), expr2ct::convert_vector(), boolbvt::convert_verilog_case_equality(), bv_cbmct::convert_waitfor(), bv_cbmct::convert_waitfor_symbol(), expr2ct::convert_with(), boolbvt::convert_with(), smt2_convt::convert_with(), boolbvt::convert_with_array(), boolbvt::convert_with_bv(), expr2javat::convert_with_precedence(), expr2cppt::convert_with_precedence(), expr2ct::convert_with_precedence(), boolbvt::convert_with_struct(), boolbvt::convert_with_union(), copy_parent(), cpp_typecheckt::cpp_constructor(), cpp_typecheckt::cpp_destructor(), goto_convertt::cpp_new_initializer(), create_initialize(), create_static_function_call(), 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(), dereference_exprt::dereference_exprt(), dereferencet::dereference_if(), dereferencet::dereference_plus(), dereferencet::dereference_rec(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), value_set_fit::dereference_rec(), value_set_fivrnst::dereference_rec(), value_set_fivrt::dereference_rec(), value_sett::dereference_rec(), dereferencet::dereference_typecast(), linkingt::detailed_conflict_report_rec(), cpp_typecheck_resolvet::disambiguate_functions(), float_bvt::div(), goto_checkt::div_by_zero_check(), 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_set_fit::do_end_function(), value_set_fivrnst::do_end_function(), value_set_fivrt::do_end_function(), value_sett::do_end_function(), string_instrumentationt::do_format_string_read(), string_instrumentationt::do_format_string_write(), value_set_fit::do_free(), value_set_fivrnst::do_free(), value_set_fivrt::do_free(), value_sett::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_rec(), 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(), custom_bitvector_domaint::eval(), string_concat_char_builtin_functiont::eval(), string_set_char_builtin_functiont::eval(), string_to_lower_case_builtin_functiont::eval(), string_to_upper_case_builtin_functiont::eval(), string_insertion_builtin_functiont::eval(), string_of_int_builtin_functiont::eval(), value_sett::eval_pointer_offset(), interpretert::evaluate(), interpretert::evaluate_address(), interpretert::execute_assign(), interpretert::execute_function_call(), cpp_typecheckt::explicit_typecast_ambiguity(), float_bvt::exponent_all_ones(), float_bvt::exponent_all_zeros(), simplify_exprt::expr2bits(), expr_initializert< nondet >::expr_initializer_rec(), 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(), extract_strings_from_lhs(), cpp_typecheck_resolvet::filter_for_named_scopes(), array_poolt::find(), cpp_typecheckt::find_assignop(), cpp_typecheckt::find_cpctor(), require_goto_statements::find_pointer_assignments(), require_goto_statements::find_struct_component_assignments(), find_superclass_with_type(), find_symbols(), smt2_convt::find_symbols(), smt2_convt::find_symbols_rec(), require_goto_statements::find_this_component_assignment(), 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(), 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(), floatbv_mult(), smt2_convt::floatbv_suffix(), format_rec(), 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(), java_bytecode_languaget::from_type(), float_bvt::from_unsigned_integer(), cpp_typecheckt::full_member_initialization(), ansi_c_declarationt::full_type(), smt2_parsert::function_application(), java_object_factoryt::gen_nondet_array_init(), symbol_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_init(), java_object_factoryt::gen_nondet_pointer_init(), java_object_factoryt::gen_nondet_struct_init(), java_object_factoryt::gen_pointer_target_init(), generate_ansi_c_start_function(), havoc_generate_function_bodiest::generate_function_body_impl(), generate_symbol_resolution_from_equations(), string_refinementt::get(), prop_conv_solvert::get(), smt2_convt::get(), float_bvt::rounding_mode_bitst::get(), get_array(), goto_convertt::get_array_argument(), prop_conv_solvert::get_bool(), invariant_sett::get_bounds(), get_char_array_and_concretize(), get_class_identifier_field(), cpp_typecheckt::get_component(), get_component_in_struct(), get_component_rec(), remove_const_function_pointerst::get_component_value(), invariant_sett::get_constant(), get_data(), get_destructor(), get_isr(), get_ldc_result(), array_poolt::get_length(), get_length(), get_null_checked_expr(), java_string_library_preprocesst::get_object_at_index(), 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(), get_or_create_class_literal_symbol(), get_or_create_string_literal_symbol(), goto_symex_statet::get_original_name(), java_string_library_preprocesst::get_primitive_value_of_object(), get_quantifier_var_max(), local_may_aliast::get_rec(), local_bitvector_analysist::get_rec(), value_set_fit::get_reference_set(), value_set_fivrt::get_reference_set(), value_set_fivrnst::get_reference_set_rec(), value_sett::get_reference_set_rec(), value_set_fit::get_reference_set_sharing_rec(), value_set_fivrt::get_reference_set_sharing_rec(), get_significand(), interpretert::get_size(), float_bvt::get_spec(), string_constraint_generatort::get_string_expr(), get_sub_arrays(), get_subexpression_at_offset(), symex_slicet::get_symbols(), value_set_fit::get_value_set(), value_set_fivrnst::get_value_set(), value_set_fivrt::get_value_set(), value_sett::get_value_set(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), value_sett::get_value_set_rec(), 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(), has_char_array_subexpr(), 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(), havoc_generate_function_bodiest::havoc_expr_rec(), interval_domaint::havoc_rec(), goto_symext::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(), infer_opaque_type_fields(), initial_index_set(), goto_symext::initialize_auto_object(), initialize_nondet_string_fields(), array_poolt::insert(), acceleratet::insert_automaton(), escape_analysist::insert_cleanup(), dump_ct::insert_local_type_decls(), cpp_typecheckt::instantiate_template(), java_bytecode_instrumentt::instrument_code(), remove_exceptionst::instrument_exception_handler(), java_bytecode_instrumentt::instrument_expr(), remove_exceptionst::instrument_throw(), string_constraint_generatort::int_of_hex_char(), integer_address(), goto_checkt::integer_overflow_check(), interval_sparse_arrayt::interval_sparse_arrayt(), string_instrumentationt::invalidate_buffer(), is_boolean(), cpp_declarationt::is_class_template(), is_condition(), remove_const_function_pointerst::is_const_expression(), cpp_declarationt::is_constructor(), cpp_declarationt::is_destructor(), is_digit_with_radix(), pointer_logict::is_dynamic_object(), cpp_declarationt::is_empty(), is_false(), string_constraint_generatort::is_high_surrogate(), string_constraint_generatort::is_low_surrogate(), is_lower_case(), is_nondet_pointer(), is_not_zero(), is_one(), is_skip(), is_true(), is_upper_case(), is_valid_java_array(), float_bvt::is_zero(), is_zero(), java_build_arguments(), java_bytecode_convert_method_lazy(), java_bytecode_promotion(), java_root_class(), json(), array_string_exprt::length(), string_set_char_builtin_functiont::length_constraint(), string_of_int_builtin_functiont::length_constraint(), length_constraint_for_concat_substr(), smt2_parsert::let_expression(), lift_if(), float_bvt::limit_distance(), linker_script_merget::linker_script_merget(), boolbvt::literal(), prop_conv_solvert::literal(), look_through_casts(), template_mapt::lookup(), remove_instanceoft::lower_instanceof(), remove_java_newt::lower_java_new(), remove_java_newt::lower_java_new_array(), lower_popcount(), linker_script_merget::ls_data2instructions(), make_allocate_code(), java_string_library_preprocesst::make_argument_for_format(), make_binary(), array_poolt::make_char_array_for_char_pointer(), make_clean_pointer_cast(), goto_convertt::make_compound_literal(), cpp_typecheck_resolvet::make_constructors(), java_string_library_preprocesst::make_copy_string_code(), interval_domaint::make_expression(), value_sett::make_member(), make_member_expr(), make_nondet_infinite_char_array(), java_string_library_preprocesst::make_nondet_string_expr(), make_not(), java_string_library_preprocesst::make_object_get_class_code(), cpp_typecheckt::make_ptr_typecast(), java_string_library_preprocesst::make_string_length_code(), 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(), 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_expr(), mutex_init_instrumentation(), cpp_declarationt::name_anon_struct_union(), goto_checkt::nan_check(), float_bvt::negation(), negation_of_not_contains_constraint(), cpp_typecheckt::new_temporary(), invariant_sett::nnf(), nondet_static(), nondet_volatile_rhs(), float_bvt::normalization_shift(), not_exprt::not_exprt(), 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()(), cpp_typecheckt::operator_is_overloaded(), cpp_declaratort::output(), cpp_declarationt::output(), ansi_c_declarationt::output(), value_set_fit::output(), value_set_fivrt::output(), value_sett::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(), goto_symext::phi_function(), pointer_offset_sum(), goto_checkt::pointer_rel_check(), goto_checkt::pointer_validity_check(), goto_symext::process_array_expr(), java_string_library_preprocesst::process_equals_function_operands(), acceleration_utilst::push_nondet(), cpp_typecheckt::put_compound_into_scope(), Parser::rAllocateExpr(), Parser::rArgDeclaration(), Parser::rCastExpr(), java_bytecode_parsert::rClassFile(), Parser::rConstructorDecl(), Parser::rDeclaration(), Parser::rDeclarator(), Parser::rDeclaratorWithInit(), pointer_arithmetict::read(), cpp_convert_typet::read_function_type(), dereferencet::read_object(), 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_calls_no_bodyt::remove_call_no_body(), 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_side_effect(), goto_convertt::remove_statement_expression(), goto_convertt::remove_temporary_object(), remove_vector(), remove_virtual_functionst::remove_virtual_function(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbolt::replace(), java_bytecode_convert_methodt::replace_call_to_cprover_assume(), java_string_library_preprocesst::replace_char_array(), goto_symext::replace_nondet(), goto_inlinet::replace_return(), constant_propagator_ait::replace_types_rec(), cpp_typecheck_resolvet::resolve(), cpp_typecheck_resolvet::resolve_argument(), goto_symext::return_assignment(), rewrite_assignment(), rewrite_index(), rewrite_union(), java_bytecode_parsert::rexceptions_attribute(), java_bytecode_parsert::rinner_classes_attribute(), Parser::rIntegralDeclaration(), Parser::rIntegralDeclStatement(), 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(), boolbvt::set_to(), string_refinementt::set_to(), prop_conv_solvert::set_to(), smt2_convt::set_to(), string_constantt::set_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_json_expr(), 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_sum(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), simplify_exprt::simplify_update(), simplify_exprt::simplify_with(), size_of_expr(), 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(), string_identifiers_resolution_from_equations(), string_of_array(), string_of_int_builtin_functiont::string_of_int_builtin_functiont(), substitute_array_access(), substitute_rec(), float_bvt::subtract_exponents(), sum_expr(), sum_overflows(), goto_symext::symex_allocate(), 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(), goto_symext::symex_goto(), goto_symext::symex_other(), cpp_typecheckt::template_suffix(), cpp_typecheckt::this_struct_type(), string_constantt::to_array_expr(), to_array_string_expr(), to_bswap_expr(), to_char_pair(), ansi_c_languaget::to_expr(), value_set_fit::to_expr(), value_set_fivrnst::to_expr(), value_set_fivrt::to_expr(), value_sett::to_expr(), sparse_arrayt::to_if_expression(), interval_sparse_arrayt::to_if_expression(), to_integer(), float_bvt::to_integer(), to_member(), jsil_declarationt::to_symbol(), trace_numeric_value(), custom_bitvector_domaint::transform(), uncaught_exceptions_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(), jsil_typecheckt::typecheck_function_call(), 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(), update_index_set(), ssa_exprt::update_type(), smt2_convt::use_array_theory(), cpp_typecheckt::user_defined_conversion_sequence(), validate_expr(), string_abstractiont::value_assignments(), postconditiont::weaken(), wp_decl(), shared_bufferst::write(), xml(), yyansi_cparse(), yyjsilparse(), zero_if_negative(), and cpp_typecheckt::zero_initializer().
|
inline |
Definition at line 57 of file expr.h.
References irept::find().
const_unique_depth_iteratort exprt::unique_depth_begin | ( | ) | const |
const_unique_depth_iteratort exprt::unique_depth_cbegin | ( | ) | const |
const_unique_depth_iteratort exprt::unique_depth_cend | ( | ) | const |
const_unique_depth_iteratort exprt::unique_depth_end | ( | ) | const |
void exprt::visit | ( | class expr_visitort & | visitor | ) |
Definition at line 263 of file expr.cpp.
References Forall_operands, and stack.
Referenced by find_qvar().
void exprt::visit | ( | class const_expr_visitort & | visitor | ) | const |
Definition at line 281 of file expr.cpp.
References forall_operands, and stack.