26 if(dest.
id()==ID_side_effect)
31 if(statement==ID_nondet)
40 if(dest.
id()==ID_side_effect &&
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)
146 const if_exprt if_expr(alias_cond, by, dest, dest.
type());
161 if(lhs.
id()==ID_member)
169 new_rhs.
old()=new_lhs;
170 new_rhs.
where().
id(ID_member_name);
171 new_rhs.
where().
set(ID_component_name, component_name);
179 else if(lhs.
id()==ID_index)
186 new_rhs.
old()=new_lhs;
246 if(statement==ID_assign)
248 else if(statement==ID_assume)
250 else if(statement==ID_skip)
252 else if(statement==ID_decl)
254 else if(statement==ID_assert)
256 else if(statement==ID_expression)
258 else if(statement==ID_printf)
260 else if(statement==ID_free)
262 else if(statement==ID_asm)
264 else if(statement==ID_fence)
267 throw "sorry, wp("+
id2string(statement)+
"...) not implemented";
const irep_idt & get_statement() const
const code_declt & to_code_decl(const codet &code)
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 ...
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 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.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
A side effect that returns a non-deterministically chosen value.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
An assumption, which must hold in subsequent code.
void rewrite_assignment(exprt &lhs, exprt &rhs)
Base class for all expressions.
const exprt & struct_op() const
const exprt & assumption() const
Operator to update elements in structs and arrays.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_statement() const