cprover
|
#include "expr_util.h"
#include <unordered_set>
#include "expr.h"
#include "expr_iterator.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "std_expr.h"
#include "symbol.h"
#include "namespace.h"
#include "arith_tools.h"
Go to the source code of this file.
Functions | |
exprt | make_binary (const exprt &expr) |
splits an expression with >=3 operands into nested binary expressions More... | |
with_exprt | make_with_expr (const update_exprt &src) |
converts an update expr into a (possibly nested) with expression More... | |
exprt | is_not_zero (const exprt &src, const namespacet &ns) |
converts a scalar/float expression to C/C++ Booleans More... | |
exprt | boolean_negate (const exprt &src) |
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More... | |
bool | has_subexpr (const exprt &expr, const std::function< bool(const exprt &)> &pred) |
returns true if the expression has a subexpression that satisfies pred More... | |
bool | has_subexpr (const exprt &src, const irep_idt &id) |
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 &type, const irep_idt &id, const namespacet &ns) |
returns true if any of the contained types is id More... | |
if_exprt | lift_if (const exprt &src, std::size_t operand_number) |
lift up an if_exprt one level More... | |
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition at line 113 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 125 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(), goto_checkt::invalidate(), and c_typecheck_baset::typecheck_side_effect_function_call().
returns true if the expression has a subexpression with given ID
Definition at line 133 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 139 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 & | type, |
const irep_idt & | id, | ||
const namespacet & | ns | ||
) |
returns true if any of the contained types is id
Definition at line 179 of file expr_util.cpp.
References has_subtype(), and irept::id().
exprt is_not_zero | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
converts a scalar/float expression to C/C++ Booleans
Definition at line 84 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 185 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 22 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 & | src | ) |
converts an update expr into a (possibly nested) with expression
Definition at line 53 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().