27 if(expr.
id()==ID_symbol)
33 std::string identifier=
37 if(l0_l1!=std::string::npos)
39 identifier.resize(l0_l1);
57 if(assign.
rhs().
id()==ID_array)
74 else if(assign.
rhs().
id()==ID_struct ||
75 assign.
rhs().
id()==ID_union)
79 if(assign.
lhs().
id()==ID_member &&
87 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
88 assign.
lhs().
id()==ID_byte_extract_big_endian)
101 exprt::operandst::const_iterator it=
103 for(
const auto &comp : components)
105 if(comp.type().id()==ID_code ||
106 comp.get_is_padding() ||
112 it != assign.
rhs().
operands().end(),
"expression must have operands");
124 if(assign.
rhs().
id()==ID_union)
134 if(lhs.find(
'$')!=std::string::npos)
137 result=lhs+
" = "+
from_expr(
ns, identifier, clean_rhs)+
";";
145 const goto_tracet::stepst::const_iterator &prev_it,
146 goto_tracet::stepst::const_iterator &it)
149 (!it->pc->is_assign() ||
154 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
160 if(prev_it!=goto_trace.
steps.end() &&
161 prev_it->pc->source_location==it->pc->source_location)
164 if(it->is_goto() && it->pc->guard.is_true())
169 if(source_location.
is_nil() ||
184 graphml[sink].node_name=
"sink";
186 graphml[sink].is_violation=
false;
187 graphml[sink].has_invariant=
false;
190 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
192 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
193 for(goto_tracet::stepst::const_iterator
194 it=goto_trace.
steps.begin();
195 it!=goto_trace.
steps.end();
200 step_to_node[it->step_nr]=sink;
206 goto_tracet::stepst::const_iterator next=it;
208 if(next!=goto_trace.
steps.end() &&
210 it->full_lhs==next->full_lhs &&
211 it->pc->source_location==next->pc->source_location)
213 step_to_node[it->step_nr]=sink;
227 graphml[node].thread_nr=it->thread_nr;
230 graphml[node].has_invariant=
false;
232 step_to_node[it->step_nr]=node;
236 for(goto_tracet::stepst::const_iterator
237 it=goto_trace.
steps.begin();
238 it!=goto_trace.
steps.end();
241 const std::size_t from=step_to_node[it->step_nr];
249 auto next = std::next(it);
250 for(; next != goto_trace.
steps.end() &&
251 (step_to_node[next->step_nr] == sink ||
257 const std::size_t to=
258 next==goto_trace.
steps.end()?
259 sink:step_to_node[next->step_nr];
282 it->full_lhs_value.is_not_nil() &&
283 it->full_lhs.is_not_nil())
288 from_expr(
ns, it->function, it->full_lhs_value) +
";";
292 val_s.
data=
id2string(it->pc->source_location.get_function());
299 const std::string cond =
from_expr(
ns, it->function, it->cond_expr);
300 const std::string neg_cond =
302 val.
data=
"["+(it->cond_value ? cond : neg_cond)+
"]";
319 val2.
data=
"["+(it->cond_value ? neg_cond : cond)+
"]";
361 graphml[sink].node_name=
"sink";
363 graphml[sink].is_violation=
false;
364 graphml[sink].has_invariant=
false;
367 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
369 std::size_t step_nr=1;
370 for(symex_target_equationt::SSA_stepst::const_iterator
378 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
379 (it->is_goto() && it->source.pc->guard.is_true()) ||
380 source_location.
is_nil() ||
384 step_to_node[step_nr]=sink;
390 symex_target_equationt::SSA_stepst::const_iterator next=it;
393 next->is_assignment() &&
394 it->ssa_full_lhs==next->ssa_full_lhs &&
395 it->source.pc->source_location==next->source.pc->source_location)
397 step_to_node[step_nr]=sink;
408 graphml[node].thread_nr=it->source.thread_nr;
409 graphml[node].is_violation=
false;
410 graphml[node].has_invariant=
false;
412 step_to_node[step_nr]=node;
417 for(symex_target_equationt::SSA_stepst::const_iterator
422 const std::size_t from=step_to_node[step_nr];
431 symex_target_equationt::SSA_stepst::const_iterator next=it;
432 std::size_t next_step_nr=step_nr;
433 for(++next, ++next_step_nr;
435 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
436 ++next, ++next_step_nr)
440 const std::size_t to=
442 sink:step_to_node[next_step_nr];
464 if((it->is_assignment() ||
466 it->ssa_rhs.is_not_nil() &&
467 it->ssa_full_lhs.is_not_nil())
469 irep_idt identifier=it->ssa_lhs.get_object_name();
471 graphml[to].has_invariant=
true;
475 id2string(it->source.pc->source_location.get_function());
477 else if(it->is_goto() &&
478 it->source.pc->is_goto())
482 const std::string cond =
484 val.
data=
"["+cond+
"]";
513 step_nr=next_step_nr;
const std::string & id2string(const irep_idt &d)
std::string convert_assign_rec(const irep_idt &identifier, const code_assignt &assign)
static bool is_built_in(const std::string &s)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
const componentst & components() const
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
Extract member of struct or union.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Expression classes for byte-level operators.
const irep_idt & get_line() const
void remove_l0_l1(exprt &expr)
const edgest & out(node_indext n) const
void set_attribute(const std::string &attribute, unsigned value)
const irep_idt & get(const irep_namet &name) const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
nodet::node_indext node_indext
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
Functor to check whether iterators from different collections point at the same object.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const irep_idt & get_file() const
Base type for structs and unions.
xmlt & new_element(const std::string &key)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const exprt & get_original_expr() const
bool is_ssa_expr(const exprt &expr)
void set_identifier(const irep_idt &identifier)
const edgest & in(node_indext n) const
#define Forall_operands(it, expr)
void operator()(const goto_tracet &goto_trace)
counterexample witness
static bool filter_out(const goto_tracet &goto_trace, const goto_tracet::stepst::const_iterator &prev_it, goto_tracet::stepst::const_iterator &it)
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
A codet representing an assignment in the program.
Witnesses for Traces and Proofs.