cprover
expr.h File Reference
#include "type.h"
Include dependency graph for expr.h:

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 OPERANDS_IN_GETSUB
 
#define forall_operands(it, expr)
 
#define Forall_operands(it, expr)
 
#define forall_expr(it, expr)
 
#define Forall_expr(it, expr)
 
#define forall_expr_list(it, expr)
 
#define Forall_expr_list(it, expr)
 

Typedefs

typedef std::list< exprtexpr_listt
 

Macro Definition Documentation

◆ forall_expr

◆ Forall_expr

#define Forall_expr (   it,
  expr 
)

◆ forall_expr_list

#define forall_expr_list (   it,
  expr 
)

◆ Forall_expr_list

#define Forall_expr_list (   it,
  expr 
)
Value:
for(expr_listt::iterator it=(expr).begin(); \
it!=(expr).end(); ++it)

Definition at line 40 of file expr.h.

◆ forall_operands

#define forall_operands (   it,
  expr 
)
Value:
if((expr).has_operands()) /* NOLINT(readability/braces) */ \
for(exprt::operandst::const_iterator it=(expr).operands().begin(), \
it##_end=(expr).operands().end(); \
it!=it##_end; ++it)

Definition at line 17 of file expr.h.

Referenced by invariant_sett::apply_code(), value_sett::apply_code(), value_set_fit::apply_code(), value_set_fivrnst::apply_code(), value_set_fivrt::apply_code(), as_vcd_binary(), value_sett::assign(), value_set_fit::assign(), value_set_fivrnst::assign(), value_set_fivrt::assign(), path_symext::assign_rec(), constant_propagator_domaint::assign_rec(), 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(), remove_instanceoft::contains_instanceof(), goto_convertt::convert(), expr2ct::convert_array(), expr2ct::convert_array_list(), graphml_witnesst::convert_assign_rec(), goto_program2codet::convert_assign_rec(), expr2ct::convert_binary(), 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(), cvc_convt::convert_constant_expr(), boolbvt::convert_constraint_select_one(), dplib_convt::convert_dplib_expr(), cvc_convt::convert_expr(), 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_overflow(), smt1_convt::convert_plus(), smt2_convt::convert_plus(), cvc_convt::convert_plus_expr(), bv_pointerst::convert_pointer_type(), goto_convertt::convert_specc_event(), goto_convertt::convert_specc_notify(), goto_convertt::convert_switch(), expr2ct::convert_update(), expr2ct::convert_vector(), interpretert::evaluate(), simplify_exprt::expr2bits(), dirtyt::find_dirty(), find_macros(), exprt::find_source_location(), find_symbols(), dplib_convt::find_symbols(), cvc_convt::find_symbols(), smt1_convt::find_symbols(), smt2_convt::find_symbols(), string_constantt::from_array_expr(), acceleration_utilst::gather_array_accesses(), gather_needed_globals(), cone_of_influencet::gather_rvalues(), acceleration_utilst::gather_rvalues(), gather_symbol_live_ranges(), gather_virtual_callsites(), 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_sett::get_value_set_rec(), value_set_fit::get_value_set_rec(), value_set_fivrnst::get_value_set_rec(), value_set_fivrt::get_value_set_rec(), 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_subexpr(), 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(), string_refinementt::initial_index_set(), mm2cppt::instruction2cpp(), 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(), path_symext::propagate(), pointer_arithmetict::read(), c_storage_spect::read(), ansi_c_convert_typet::read_rec(), _rw_set_loct::read_write_rec(), cvc_convt::set_to(), dplib_convt::set_to(), smt1_convt::set_to(), prop_conv_solvert::set_to(), bv_refinementt::set_to(), smt2_convt::set_to(), smt1_convt::set_value(), simplify_exprt::simplify_bitwise(), simplify_exprt::simplify_boolean(), qdimacs_coret::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(), string_refinementt::update_index_set(), exprt::visit(), xml(), yyansi_cparse(), and yyjsilparse().

◆ Forall_operands

#define Forall_operands (   it,
  expr 
)
Value:
if((expr).has_operands()) /* NOLINT(readability/braces) */ \
for(exprt::operandst::iterator it=(expr).operands().begin(); \
it!=(expr).operands().end(); ++it)

Definition at line 23 of file expr.h.

Referenced by acceleration_utilst::abstract_arrays(), 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(), smt2_convt::collect_bindings(), preconditiont::compute_rec(), goto_convertt::convert_assign(), jsil_convertt::convert_code(), smt1_convt::convert_plus(), goto_program_dereferencet::dereference_instruction(), goto_program_dereferencet::dereference_rec(), goto_symext::dereference_rec(), path_symex_statet::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(), prop_conv_solvert::get(), goto_symex_statet::get_l1_name(), goto_symex_statet::get_original_name(), symex_slice_by_tracet::implied_guards(), insert_at_label(), path_symex_statet::instantiate_rec(), remove_instanceoft::lower_instanceof(), make_next_state(), invariant_sett::nnf(), nondet_volatile_rhs(), goto_symex_statet::propagationt::operator()(), goto_symext::process_array_expr(), goto_symext::process_array_expr_rec(), acceleration_utilst::push_nondet(), path_symex_statet::read_symbol_member_index(), remove_complex(), graphml_witnesst::remove_l0_l1(), remove_vector(), rename(), rename_symbolt::rename(), goto_symex_statet::rename(), goto_symex_statet::rename_address(), replace_symbol_extt::replace(), replace_symbolt::replace(), goto_symext::replace_array_equal(), constant_propagator_ait::replace_array_symbol(), replace_expr(), 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().

◆ OPERANDS_IN_GETSUB

#define OPERANDS_IN_GETSUB

Definition at line 13 of file expr.h.

Typedef Documentation

◆ expr_listt

typedef std::list<exprt> expr_listt

Definition at line 166 of file expr.h.