cprover
|
#include "expr_util.h"
#include "expr.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 | |
void | make_next_state (exprt &expr) |
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 &src, const irep_idt &id) |
returns true if the expression has a subexpression with given 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 120 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(), goto_convertt::generate_conditional_branch(), and goto_convertt::generate_ifthenelse().
returns true if the expression has a subexpression with given ID
Definition at line 132 of file expr_util.cpp.
References forall_operands, has_subexpr(), and irept::id().
Referenced by value_set_dereferencet::has_dereference(), goto_checkt::has_dereference(), and has_subexpr().
exprt is_not_zero | ( | const exprt & | src, |
const namespacet & | ns | ||
) |
converts a scalar/float expression to C/C++ Booleans
Definition at line 91 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 144 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 29 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().
void make_next_state | ( | exprt & | ) |
Use functions from util/std_expr.h instead.
Definition at line 20 of file expr_util.cpp.
References Forall_operands, irept::id(), and make_next_state().
Referenced by goto_convertt::convert_bp_enforce(), and make_next_state().
with_exprt make_with_expr | ( | const update_exprt & | src | ) |
converts an update expr into a (possibly nested) with expression
Definition at line 60 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().