19 error() <<
"waitfor expected to have four operands" <<
eom;
33 error() <<
"waitfor bound must be a constant" <<
eom;
58 exprt tmp_predicate=predicate;
59 replace_expr(cycle_var, old_cycle_plus_i, tmp_predicate);
70 old_cycle_plus_i, ID_le, bound);
72 old_cycle_plus_i, ID_lt, new_cycle);
73 const and_exprt and_expr(cycle_le_bound, cycle_lt_new_cycle);
83 old_cycle_plus_i, ID_le, bound);
84 const equal_exprt cycle_eq_new_cycle(old_cycle_plus_i, new_cycle);
85 const and_exprt and_expr(cycle_le_bound, cycle_eq_new_cycle);
111 if(expr.
id()==
"waitfor")
114 if(expr.
id()==
"waitfor_symbol")
A generic base class for relations, i.e., binary predicates.
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
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 bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
#define PRECONDITION(CONDITION)
virtual exprt make_free_bv_expr(const typet &type)
mstreamt & result() const
Base class for all expressions.
void set_to_true(const exprt &expr)
virtual bvt convert_waitfor(const exprt &expr)
std::vector< literalt > bvt