cprover
|
Deprecated expression utility functions. More...
Go to the source code of this file.
Functions | |
bool | is_lvalue (const exprt &expr) |
Returns true iff the argument is (syntactically) an lvalue. More... | |
exprt | make_binary (const exprt &) |
splits an expression with >=3 operands into nested binary expressions More... | |
with_exprt | make_with_expr (const update_exprt &) |
converts an update expr into a (possibly nested) with expression More... | |
exprt | is_not_zero (const exprt &, const namespacet &ns) |
converts a scalar/float expression to C/C++ Booleans More... | |
exprt | boolean_negate (const exprt &) |
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More... | |
bool | has_subexpr (const exprt &, const std::function< bool(const exprt &)> &pred) |
returns true if the expression has a subexpression that satisfies pred More... | |
bool | has_subexpr (const exprt &, const irep_idt &) |
returns true if the expression has a subexpression with given ID More... | |
bool | has_subtype (const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns) |
returns true if any of the contained types satisfies pred More... | |
bool | has_subtype (const typet &, const irep_idt &id, const namespacet &) |
returns true if any of the contained types is id More... | |
if_exprt | lift_if (const exprt &, std::size_t operand_number) |
lift up an if_exprt one level More... | |
const exprt & | skip_typecast (const exprt &expr) |
find the expression nested inside typecasts, if any More... | |
Deprecated expression utility functions.
Definition in file expr_util.h.
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition at line 126 of file expr_util.cpp.
References irept::id(), exprt::is_false(), exprt::is_true(), exprt::op0(), and exprt::operands().
Referenced by goto_convertt::convert_while(), qbf_bdd_certificatet::f_get(), qbf_squolem_coret::f_get(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), and goto_convertt::optimize_guarded_gotos().
returns true if the expression has a subexpression that satisfies pred
Definition at line 138 of file expr_util.cpp.
References exprt::depth_begin(), and exprt::depth_end().
Referenced by goto_program_dereferencet::dereference_rec(), rw_range_set_value_sett::get_objects_dereference(), has_char_array_subexpr(), has_subexpr(), and goto_checkt::invalidate().
returns true if the expression has a subexpression with given ID
Definition at line 146 of file expr_util.cpp.
References has_subexpr(), and irept::id().
bool has_subtype | ( | const typet & | type, |
const std::function< bool(const typet &)> & | pred, | ||
const namespacet & | ns | ||
) |
returns true if any of the contained types satisfies pred
type | a type |
pred | a predicate |
ns | namespace for symbol type lookups |
type
satisfies predicate pred
. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... For instance in the type t
defined by { int a; char[] b; double * c; { bool d} e}
, int
, char
, double
and bool
are subtypes of t
. Definition at line 152 of file expr_util.cpp.
References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), stack, typet::subtypes(), to_c_enum_tag_type(), and to_struct_union_type().
Referenced by add_string_equation_to_symbol_resolution(), has_char_pointer_subtype(), has_subtype(), and string_identifiers_resolution_from_equations().
bool has_subtype | ( | const typet & | , |
const irep_idt & | id, | ||
const namespacet & | |||
) |
returns true if any of the contained types is id
Definition at line 192 of file expr_util.cpp.
References has_subtype(), and irept::id().
bool is_lvalue | ( | const exprt & | expr | ) |
Returns true iff the argument is (syntactically) an lvalue.
Definition at line 22 of file expr_util.cpp.
References index_exprt::array(), member_exprt::compound(), irept::id(), is_lvalue(), to_index_expr(), and to_member_expr().
Referenced by goto_convertt::do_function_call_symbol(), is_lvalue(), and make_va_list().
exprt is_not_zero | ( | const exprt & | , |
const namespacet & | ns | ||
) |
converts a scalar/float expression to C/C++ Booleans
Definition at line 97 of file expr_util.cpp.
References CHECK_RETURN, namespace_baset::follow(), namespace_baset::follow_tag(), from_integer(), irept::id(), irept::is_not_nil(), exprt::source_location(), to_c_enum_tag_type(), and exprt::type().
Referenced by c_typecastt::do_typecast(), goto_convertt::remove_assignment(), goto_convertt::remove_post(), and goto_convertt::remove_pre().
lift up an if_exprt one level
Definition at line 198 of file expr_util.cpp.
References if_exprt::cond(), if_exprt::false_case(), exprt::operands(), PRECONDITION, to_if_expr(), if_exprt::true_case(), and exprt::type().
Referenced by simplify_exprt::simplify_byte_extract(), simplify_exprt::simplify_dynamic_object(), simplify_exprt::simplify_inequality(), simplify_exprt::simplify_inequality_constant(), and simplify_exprt::simplify_pointer_offset().
splits an expression with >=3 operands into nested binary expressions
Definition at line 35 of file expr_util.cpp.
References exprt::operands(), PRECONDITION, irept::swap(), and exprt::type().
Referenced by adjust_float_expressions(), bv_refinementt::convert_mult(), smt2_convt::convert_plus(), goto_checkt::float_overflow_check(), bdd_exprt::from_expr_rec(), and goto_checkt::nan_check().
with_exprt make_with_expr | ( | const update_exprt & | ) |
converts an update expr into a (possibly nested) with expression
Definition at line 66 of file expr_util.cpp.
References update_exprt::designator(), forall_expr, index_designatort::index(), with_exprt::new_value(), PRECONDITION, to_index_designator(), to_with_expr(), UNREACHABLE, and with_exprt::where().
find the expression nested inside typecasts, if any
Definition at line 218 of file expr_util.cpp.
References irept::id(), skip_typecast(), and to_typecast_expr().
Referenced by goto_program2codet::convert_assign_varargs(), goto_program2codet::convert_goto_switch(), goto_program2codet::get_cases(), get_null_checked_expr(), and skip_typecast().