Go to the documentation of this file.
27 if(dest.
id()==ID_side_effect)
32 if(statement==ID_nondet)
41 if(dest.
id()==ID_side_effect &&
46 dest.
id(ID_nondet_symbol);
56 static unsigned count=0;
69 e1.
id() == ID_dereference &&
77 e2.
id() == ID_dereference &&
93 if(e1.
id()==ID_symbol && e2.
id()==ID_symbol)
105 if(e1.
id()==ID_index || e1.
id()==ID_struct)
106 if(e2.
id()!=ID_dereference && e1.
id()!=e2.
id())
109 if(e2.
id()==ID_index || e2.
id()==ID_struct)
110 if(e2.
id()!=ID_dereference && e1.
id()!=e2.
id())
126 if(dest.
id()!=ID_address_of)
131 if(dest.
id()==ID_member ||
132 dest.
id()==ID_index ||
133 dest.
id()==ID_dereference ||
134 dest.
id()==ID_symbol)
151 const if_exprt if_expr(alias_cond, by, dest, dest.
type());
166 if(lhs.
id()==ID_member)
173 new_rhs.
where().
set(ID_component_name, component_name);
180 else if(lhs.
id()==ID_index)
243 if(statement==ID_assign)
245 else if(statement==ID_assume)
247 else if(statement==ID_skip)
249 else if(statement==ID_decl)
251 else if(statement==ID_assert)
253 else if(statement==ID_expression)
255 else if(statement==ID_printf)
257 else if(statement==ID_asm)
259 else if(statement==ID_fence)
262 false,
"sorry, wp(",
id2string(statement),
"...) is not implemented");
Operator to update elements in structs and arrays.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void substitute_rec(exprt &dest, const exprt &what, const exprt &by, const namespacet &ns)
replace 'what' by 'by' in 'dest', considering possible aliasing
#define Forall_operands(it, expr)
const code_declt & to_code_decl(const codet &code)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
The trinary if-then-else operator.
A codet representing the declaration of a local variable.
const exprt & assumption() const
Base class for all expressions.
bool has_nondet(const exprt &dest)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void approximate_nondet(exprt &dest)
Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.
aliasingt
consider possible aliasing
side_effect_exprt & to_side_effect_expr(exprt &expr)
exprt wp_decl(const code_declt &code, const exprt &post, const namespacet &ns)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
void approximate_nondet_rec(exprt &dest, unsigned &count)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
const code_assumet & to_code_assume(const codet &code)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
const exprt & struct_op() const
aliasingt aliasing(const exprt &e1, const exprt &e2, const namespacet &ns)
exprt wp_assign(const code_assignt &code, const exprt &post, const namespacet &ns)
An assumption, which must hold in subsequent code.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const irep_idt & get_statement() const
A side_effect_exprt that returns a non-deterministically chosen value.
Extract member of struct or union.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
void rewrite_assignment(exprt &lhs, exprt &rhs)
const code_assignt & to_code_assign(const codet &code)
void set(const irep_namet &name, const irep_idt &value)
exprt wp_assume(const code_assumet &code, const exprt &post, const namespacet &)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
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.
Operator to return the address of an object.
A codet representing an assignment in the program.
const irep_idt & get_statement() const
API to expression classes.
An expression containing a side effect.
Data structure for representing an arbitrary statement in a program.