23 if(expr.
id()==ID_symbol)
29 std::string identifier=
33 if(l0_l1!=std::string::npos)
35 identifier.resize(l0_l1);
53 if(assign.
rhs().
id()==ID_array)
70 else if(assign.
rhs().
id()==ID_struct ||
71 assign.
rhs().
id()==ID_union)
75 if(assign.
lhs().
id()==ID_member &&
83 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
84 assign.
lhs().
id()==ID_byte_extract_big_endian)
97 exprt::operandst::const_iterator it=
99 for(
const auto &comp : components)
101 if(comp.type().id()==ID_code ||
102 comp.get_is_padding() ||
119 if(assign.
rhs().
id()==ID_union)
129 if(lhs.find(
'$')!=std::string::npos)
132 result=lhs+
" = "+
from_expr(
ns, identifier, clean_rhs)+
";";
140 const goto_tracet::stepst::const_iterator &prev_it,
141 goto_tracet::stepst::const_iterator &it)
144 (!it->is_assignment() ||
149 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
155 if(prev_it!=goto_trace.
steps.end() &&
156 prev_it->pc->source_location==it->pc->source_location)
159 if(it->is_goto() && it->pc->guard.is_true())
164 if(source_location.
is_nil() ||
179 graphml[sink].node_name=
"sink";
181 graphml[sink].is_violation=
false;
182 graphml[sink].has_invariant=
false;
185 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
187 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
188 for(goto_tracet::stepst::const_iterator
189 it=goto_trace.
steps.begin();
190 it!=goto_trace.
steps.end();
195 step_to_node[it->step_nr]=sink;
201 goto_tracet::stepst::const_iterator next=it;
203 if(next!=goto_trace.
steps.end() &&
205 it->full_lhs==next->full_lhs &&
206 it->pc->source_location==next->pc->source_location)
208 step_to_node[it->step_nr]=sink;
219 std::to_string(it->pc->location_number)+
"."+std::to_string(it->step_nr);
222 graphml[node].thread_nr=it->thread_nr;
225 graphml[node].has_invariant=
false;
227 step_to_node[it->step_nr]=node;
231 for(goto_tracet::stepst::const_iterator
232 it=goto_trace.
steps.begin();
233 it!=goto_trace.
steps.end();
236 const std::size_t from=step_to_node[it->step_nr];
244 goto_tracet::stepst::const_iterator next=it;
246 next!=goto_trace.
steps.end() &&
247 (step_to_node[next->step_nr]==sink || it->pc==next->pc);
252 const std::size_t to=
253 next==goto_trace.
steps.end()?
254 sink:step_to_node[next->step_nr];
277 it->lhs_object_value.is_not_nil() &&
278 it->full_lhs.is_not_nil())
280 if(!it->lhs_object_value.is_constant() ||
281 !it->lhs_object_value.has_operands() ||
287 code_assignt assign(it->lhs_object, it->lhs_object_value);
288 irep_idt identifier=it->lhs_object.get_identifier();
293 val_s.
data=
id2string(it->pc->source_location.get_function());
301 const std::string cond=
from_expr(
ns,
"", it->cond_expr);
302 const std::string neg_cond=
304 val.
data=
"["+(it->cond_value ? cond : neg_cond)+
"]";
321 val2.
data=
"["+(it->cond_value ? neg_cond : cond)+
"]";
363 graphml[sink].node_name=
"sink";
365 graphml[sink].is_violation=
false;
366 graphml[sink].has_invariant=
false;
369 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
371 std::size_t step_nr=1;
372 for(symex_target_equationt::SSA_stepst::const_iterator
380 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
381 (it->is_goto() && it->source.pc->guard.is_true()) ||
382 source_location.
is_nil() ||
386 step_to_node[step_nr]=sink;
392 symex_target_equationt::SSA_stepst::const_iterator next=it;
395 next->is_assignment() &&
396 it->ssa_full_lhs==next->ssa_full_lhs &&
397 it->source.pc->source_location==next->source.pc->source_location)
399 step_to_node[step_nr]=sink;
406 std::to_string(it->source.pc->location_number)+
"."+
407 std::to_string(step_nr);
410 graphml[node].thread_nr=it->source.thread_nr;
411 graphml[node].is_violation=
false;
412 graphml[node].has_invariant=
false;
414 step_to_node[step_nr]=node;
419 for(symex_target_equationt::SSA_stepst::const_iterator
424 const std::size_t from=step_to_node[step_nr];
433 symex_target_equationt::SSA_stepst::const_iterator next=it;
434 std::size_t next_step_nr=step_nr;
435 for(++next, ++next_step_nr;
437 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
438 ++next, ++next_step_nr)
442 const std::size_t to=
444 sink:step_to_node[next_step_nr];
466 if((it->is_assignment() ||
468 it->ssa_rhs.is_not_nil() &&
469 it->ssa_full_lhs.is_not_nil())
471 irep_idt identifier=it->ssa_lhs.get_object_name();
473 graphml[to].has_invariant=
true;
477 id2string(it->source.pc->source_location.get_function());
479 else if(it->is_goto() &&
480 it->source.pc->is_goto())
484 const std::string cond=
from_expr(
ns,
"", it->cond_expr);
486 val.
data=
"["+cond+
"]";
515 step_nr=next_step_nr;
const typet & follow(const typet &src) const
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)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const componentst & components() const
unsignedbv_typet size_type()
Extract member of struct or union.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Expression classes for byte-level operators.
const irep_idt & get_line() const
void remove_l0_l1(exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
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
#define forall_operands(it, expr)
nodet::node_indext node_indext
bitvector_typet index_type()
xmlt & new_element(const std::string &name)
bool has_prefix(const std::string &s, const std::string &prefix)
const irep_idt & get_file() const
Base type of C structs and unions, and C++ classes.
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
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)
Witnesses for Traces and Proofs.