25 if(expr.
id()==ID_symbol)
26 expr.
id(ID_next_symbol);
33 if(operands.size()<=2)
39 exprt previous=operands.front();
42 for(exprt::operandst::const_iterator
43 it=++operands.begin();
51 tmp.operands().resize(2);
52 tmp.op0().swap(previous);
72 if(it->id()==ID_index_designator)
76 else if(it->id()==ID_member_designator)
100 const typet &src_type=
101 src.
type().
id()==ID_c_enum_tag?
105 if(src_type.
id()==ID_bool)
109 src_type.
id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
122 if(src.
id()==ID_not && src.
operands().size()==1)
150 const exprt true_case=if_expr.true_case();
151 const exprt false_case=if_expr.false_case();
154 result.
cond()=if_expr.cond();
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
The type of an expression.
const typet & follow(const typet &src) const
Operator to update elements in structs and arrays.
Deprecated expression utility functions.
#define forall_expr(it, expr)
exprt::operandst & designator()
The trinary if-then-else operator.
#define CHECK_RETURN(CONDITION)
const typet & follow_tag(const union_tag_typet &src) const
const irep_idt & id() const
The boolean constant true.
void make_next_state(exprt &expr)
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
A generic base class for binary expressions.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
API to expression classes.
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
#define PRECONDITION(CONDITION)
#define forall_operands(it, expr)
const exprt & index() const
The boolean constant false.
bool has_subexpr(const exprt &src, const irep_idt &id)
returns true if the expression has a subexpression with given ID
std::vector< exprt > operandst
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Base class for all expressions.
Operator to update elements in structs and arrays.
const source_locationt & source_location() const
#define Forall_operands(it, expr)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions