26 if(dest.
id()==ID_side_effect)
31 if(statement==ID_nondet)
40 if(dest.
id()==ID_side_effect &&
44 dest.
set(ID_identifier,
"wp::nondet::"+std::to_string(count));
45 dest.
id(ID_nondet_symbol);
55 static unsigned count=0;
67 if(e1.
id()==ID_dereference &&
69 e1.
op0().
id()==ID_address_of &&
73 if(e2.
id()==ID_dereference &&
75 e2.
op0().
id()==ID_address_of &&
88 if(e1.
id()==ID_symbol && e2.
id()==ID_symbol)
100 if(e1.
id()==ID_index || e1.
id()==ID_struct)
101 if(e2.
id()!=ID_dereference && e1.
id()!=e2.
id())
104 if(e2.
id()==ID_index || e2.
id()==ID_struct)
105 if(e2.
id()!=ID_dereference && e1.
id()!=e2.
id())
121 if(dest.
id()!=ID_address_of)
126 if(dest.
id()==ID_member ||
127 dest.
id()==ID_index ||
128 dest.
id()==ID_dereference ||
129 dest.
id()==ID_symbol)
148 if_expr.
cond()=alias_cond;
166 if(lhs.
id()==ID_member)
174 new_rhs.
old()=new_lhs;
175 new_rhs.
where().
id(ID_member_name);
176 new_rhs.
where().
set(ID_component_name, component_name);
184 else if(lhs.
id()==ID_index)
191 new_rhs.
old()=new_lhs;
251 if(statement==ID_assign)
253 else if(statement==ID_assume)
255 else if(statement==ID_skip)
257 else if(statement==ID_decl)
259 else if(statement==ID_assert)
261 else if(statement==ID_expression)
263 else if(statement==ID_printf)
265 else if(statement==ID_free)
267 else if(statement==ID_asm)
269 else if(statement==ID_fence)
272 throw "sorry, wp("+
id2string(statement)+
"...) not implemented";
const irep_idt & get_statement() const
const code_declt & to_code_decl(const codet &code)
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &ns)
exprt wp(const codet &code, const exprt &post, const namespacet &ns)
Compute the weakest precondition of the given program piece code with respect to the expression post...
const std::string & id2string(const irep_idt &d)
const code_assumet & to_code_assume(const codet &code)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
bool has_nondet(const exprt &dest)
void approximate_nondet_rec(exprt &dest, unsigned &count)
const irep_idt & get_identifier() const
void approximate_nondet(exprt &dest)
approximate the non-deterministic choice in a way cheaper than by (proper) quantification ...
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
The trinary if-then-else operator.
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
A declaration of a local variable.
API to expression classes.
A side effect that returns a non-deterministically chosen value.
#define forall_operands(it, expr)
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
void substitute_rec(exprt &dest, const exprt &what, const exprt &by, const namespacet &ns)
replace 'what' by 'by' in 'dest', considering possible aliasing
Operator to return the address of an object.
void rewrite_assignment(exprt &lhs, exprt &rhs)
Base class for all expressions.
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const exprt & assumption() const
Operator to update elements in structs and arrays.
irep_idt get_component_name() const
#define Forall_operands(it, expr)
aliasingt
consider possible aliasing
A statement in a programming language.
An expression containing a side effect.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const