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;