cprover
|
Go to the source code of this file.
Classes | |
class | exprt |
Base class for all expressions. More... | |
class | expr_visitort |
class | const_expr_visitort |
Macros | |
#define | forall_operands(it, expr) |
#define | Forall_operands(it, expr) |
#define | forall_expr(it, expr) |
#define | Forall_expr(it, expr) |
#define forall_expr | ( | it, | |
expr | |||
) |
Definition at line 28 of file expr.h.
Referenced by goto_convertt::case_guard(), boolbvt::convert_array(), prop_conv_solvert::convert_bool(), expr2javat::convert_code_function_call(), expr2ct::convert_code_function_call(), boolbvt::convert_complex(), boolbvt::convert_concatenation(), expr2ct::convert_function_application(), boolbvt::convert_index(), expr2ct::convert_side_effect_expr_function_call(), boolbvt::convert_vector(), goto_convertt::do_function_call_symbol(), expressions_read(), goto_rw(), cpp_typecheckt::instantiate_template(), make_with_expr(), remove_function_pointerst::remove_function_pointer(), cpp_typecheckt::show_instantiation_stack(), and sort_operands().
#define Forall_expr | ( | it, | |
expr | |||
) |
Definition at line 32 of file expr.h.
Referenced by goto_program2codet::cleanup_code(), dump_ct::cleanup_expr(), goto_program2codet::cleanup_function_call(), goto_convertt::do_function_call(), find_block_position_rec(), concurrency_instrumentationt::instrument(), simplify_exprt::simplify_plus(), and goto_symext::symex_step().
#define forall_operands | ( | it, | |
expr | |||
) |
Definition at line 17 of file expr.h.
Referenced by invariant_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), value_sett::apply_code_rec(), as_vcd_binary(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), value_sett::assign(), interval_domaint::assume_rec(), c_sizeof_type_rec(), goto_checkt::check_rec(), check_renaming(), check_renaming_l1(), goto_program2codet::cleanup_code_block(), arrayst::collect_indices(), goto_convertt::collect_operands(), compute_address_taken_functions(), compute_functions(), goto_symex_statet::constant_propagation(), goto_convertt::convert(), expr2ct::convert_array(), expr2ct::convert_array_list(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), boolbvt::convert_bitwise(), goto_convertt::convert_block(), prop_conv_solvert::convert_bool(), 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_block(), expr2ct::convert_code_decl_block(), expr2ct::convert_code_input(), expr2ct::convert_code_output(), expr2ct::convert_code_printf(), expr2ct::convert_code_switch(), expr2ct::convert_complex(), expr2ct::convert_cond(), boolbvt::convert_cond(), boolbvt::convert_constant(), boolbvt::convert_constraint_select_one(), smt2_convt::convert_expr(), smt2_convt::convert_floatbv(), expr2ct::convert_function(), expr2ct::convert_initializer_list(), java_bytecode_convert_methodt::convert_instructions(), smt2_convt::convert_minus(), smt2_convt::convert_mult(), expr2ct::convert_multi_ary(), expr2ct::convert_overflow(), smt2_convt::convert_plus(), bv_pointerst::convert_pointer_type(), expr2ct::convert_update(), expr2ct::convert_vector(), interpretert::evaluate(), simplify_exprt::expr2bits(), dirtyt::find_dirty(), find_macros(), exprt::find_source_location(), find_symbols(), smt2_convt::find_symbols(), string_constantt::from_array_expr(), acceleration_utilst::gather_array_accesses(), ci_lazy_methodst::gather_needed_globals(), cone_of_influencet::gather_rvalues(), acceleration_utilst::gather_rvalues(), gather_symbol_live_ranges(), remove_asmt::gcc_asm_function_call(), prop_conv_solvert::get_bool(), get_destructor(), rw_range_sett::get_objects_array(), get_objects_rec(), rw_range_sett::get_objects_rec(), rw_range_sett::get_objects_struct(), goto_convertt::get_string_constant(), symex_slicet::get_symbols(), 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(), goto_checkt::goto_check(), value_sett::guard(), has_and_or(), has_byte_operator(), goto_convertt::has_function_call(), custom_bitvector_domaint::has_get_must_or_may(), has_labels(), has_nondet(), string_abstractiont::has_string_macros(), has_symbol(), 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(), invariant_sett::implies_rec(), mm2cppt::instruction2cpp(), java_bytecode_instrumentt::instrument_expr(), constant_propagator_domaint::valuest::is_constant(), postconditiont::is_used(), json(), c_typecheck_baset::make_designator(), goto_convertt::needs_cleaning(), objects_read(), cpp_typecheckt::operator_is_overloaded(), overflow_instrumentert::overflow_expr(), cpp_typecheckt::overloadable(), pointer_arithmetict::read(), c_storage_spect::read(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), set_internal_dynamic_object(), prop_conv_solvert::set_to(), smt2_convt::set_to(), simplify_exprt::simplify_bitwise(), qdimacs_coret::simplify_extractbits(), simplify_exprt::simplify_extractbits(), simplify_exprt::simplify_if_conj(), simplify_exprt::simplify_if_disj(), simplify_exprt::simplify_if_preorder(), simplify_exprt::simplify_inequality_pointer_object(), simplify_exprt::simplify_plus(), sort_and_join(), invariant_sett::strengthen_rec(), trace_value_binary(), goto_symext::trigger_auto_object(), constant_propagator_domaint::two_way_propagate_rec(), c_typecheck_baset::typecheck_expr_builtin_offsetof(), cpp_typecheckt::typecheck_member_initializer(), update_index_set(), exprt::visit(), xml(), yyansi_cparse(), and yyjsilparse().
#define Forall_operands | ( | it, | |
expr | |||
) |
Definition at line 23 of file expr.h.
Referenced by acceleration_utilst::abstract_arrays(), adjust_byte_extract_rec(), adjust_float_expressions(), template_mapt::apply(), approximate_nondet_rec(), base_type(), goto_convertt::clean_expr(), goto_convertt::clean_expr_address_of(), goto_program2codet::cleanup_code(), goto_program2codet::cleanup_expr(), dump_ct::cleanup_expr(), dump_ct::cleanup_harness(), smt2_convt::collect_bindings(), preconditiont::compute_rec(), goto_convertt::convert_assign(), jsil_convertt::convert_code(), goto_program_dereferencet::dereference_instruction(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), c_typecheck_baset::do_initializer_rec(), simplify_exprt::eliminate_common_addends(), custom_bitvector_domaint::eval(), value_sett::eval_pointer_offset(), fix_types(), flatten_byte_operators(), namespace_baset::follow_macros(), goto_symex_statet::get_l1_name(), goto_symex_statet::get_original_name(), symex_slice_by_tracet::implied_guards(), insert_at_label(), java_bytecode_instrumentt::instrument_code(), remove_instanceoft::lower_instanceof(), invariant_sett::nnf(), nondet_volatile_rhs(), goto_symex_statet::propagationt::operator()(), acceleration_utilst::push_nondet(), remove_complex(), graphml_witnesst::remove_l0_l1(), remove_vector(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbolt::replace(), replace_location(), goto_convertt::replace_new_object(), goto_symext::replace_nondet(), string_abstractiont::replace_string_macros(), constant_propagator_ait::replace_types_rec(), rewrite_union(), Parser::rPostfixExpr(), invariant_sett::simplify(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_byte_update(), simplify_exprt::simplify_concatenation(), simplify_exprt::simplify_if(), simplify_exprt::simplify_if_conj(), simplify_exprt::simplify_if_disj(), simplify_exprt::simplify_if_recursive(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_node_preorder(), simplify_exprt::simplify_not(), simplify_exprt::simplify_object(), simplify_exprt::simplify_plus(), simplify_exprt::simplify_typecast(), symex_slice_by_tracet::slice_SSA_steps(), smt2_convt::substitute_let(), substitute_rec(), goto_symext::symex_fkt(), c_typecheck_baset::typecheck_asm(), jsil_typecheckt::typecheck_block(), c_typecheck_baset::typecheck_block(), java_bytecode_typecheckt::typecheck_code(), cpp_typecheckt::typecheck_compound_body(), java_bytecode_typecheckt::typecheck_expr(), c_typecheck_baset::typecheck_expr_main(), jsil_typecheckt::typecheck_expr_operands(), c_typecheck_baset::typecheck_expr_operands(), cpp_typecheckt::typecheck_member_initializer(), exprt::visit(), and postconditiont::weaken().