19 error() <<
"waitfor expected to have four operands" <<
eom;
35 error() <<
"waitfor bound must be a constant" <<
eom;
54 bound_plus1.copy_to_operands(bound);
55 bound_plus1.move_to_operands(one);
66 exprt old_cycle_plus_i(ID_plus, old_cycle.
type());
67 old_cycle_plus_i.
operands().resize(2);
68 old_cycle_plus_i.op0()=old_cycle;
71 exprt tmp_predicate=predicate;
72 replace_expr(cycle_var, old_cycle_plus_i, tmp_predicate);
84 cycle_le_bound.
op0()=old_cycle_plus_i;
85 cycle_le_bound.
op1()=bound;
88 cycle_lt_new_cycle.
operands().resize(2);
89 cycle_lt_new_cycle.
op0()=old_cycle_plus_i;
90 cycle_lt_new_cycle.
op1()=new_cycle;
94 and_expr.
op0().
swap(cycle_le_bound);
95 and_expr.
op1().
swap(cycle_lt_new_cycle);
108 cycle_le_bound.
operands().resize(2);
109 cycle_le_bound.
op0()=old_cycle_plus_i;
110 cycle_le_bound.
op1()=bound;
113 cycle_eq_new_cycle.
operands().resize(2);
114 cycle_eq_new_cycle.
op0()=old_cycle_plus_i;
115 cycle_eq_new_cycle.
op1()=new_cycle;
119 and_expr.
op0().
swap(cycle_le_bound);
120 and_expr.
op1().
swap(cycle_eq_new_cycle);
140 error() <<
"waitfor_symbol expected to have one operand" <<
eom;
152 rel_expr.copy_to_operands(
result, bound);
160 if(expr.
id()==
"waitfor")
163 if(expr.
id()==
"waitfor_symbol")
void copy_to_operands(const exprt &expr)
bvt convert_bitvector(const exprt &expr) override
void move_to_operands(exprt &expr)
static mstreamt & eom(mstreamt &m)
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bvt convert_waitfor_symbol(const exprt &expr)
const source_locationt & find_source_location() const
source_locationt source_location
virtual void make_free_bv_expr(const typet &type, exprt &dest)
virtual bvt convert_bitvector(const exprt &expr)
Base class for all expressions.
void set_to_true(const exprt &expr)
virtual bvt convert_waitfor(const exprt &expr)
std::vector< literalt > bvt
void reserve_operands(operandst::size_type n)