42 if(expr.
id()==ID_symbol)
48 std::string identifier=
52 if(l0_l1!=std::string::npos)
54 identifier.resize(l0_l1);
61 else if(expr.
id() == ID_string_constant)
82 if(cit !=
cache.end())
87 if(assign.
rhs().
id() == ID_array_list)
90 const auto &ops = array_list.
operands();
92 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
101 else if(assign.
rhs().
id() == ID_array)
117 else if(assign.
rhs().
id()==ID_struct ||
118 assign.
rhs().
id()==ID_union)
123 assign.
lhs().
id() == ID_member &&
131 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
132 assign.
lhs().
id()==ID_byte_extract_big_endian)
145 exprt::operandst::const_iterator it=
147 for(
const auto &comp : components)
149 if(comp.type().id()==ID_code ||
150 comp.get_is_padding() ||
156 it != assign.
rhs().
operands().end(),
"expression must have operands");
168 if(assign.
rhs().
id()==ID_union)
172 else if(assign.
rhs().
id() == ID_with)
175 const auto &ops = with_expr.
operands();
177 for(std::size_t i = 1; i < ops.size(); i += 2)
182 if(ops[i].
id() == ID_member_name)
185 assign.
lhs(), ops[i].
get(ID_component_name), ops[i + 1].type()};
207 lhs.find(
"#return_value") != std::string::npos ||
208 (lhs.find(
'$') != std::string::npos &&
209 has_prefix(lhs,
"return_value___VERIFIER_nondet_")))
228 const goto_tracet::stepst::const_iterator &prev_it,
229 goto_tracet::stepst::const_iterator &it)
232 it->hidden && (!it->pc->is_assign() ||
233 it->pc->get_assign().rhs().id() != ID_side_effect ||
234 it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
237 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
243 if(prev_it!=goto_trace.
steps.end() &&
244 prev_it->pc->source_location==it->pc->source_location)
247 if(it->is_goto() && it->pc->get_condition().is_true())
252 if(source_location.
is_nil() ||
271 expr.
id() == ID_symbol &&
288 unsigned int max_thread_idx = 0;
289 bool trace_has_violation =
false;
290 for(goto_tracet::stepst::const_iterator it = goto_trace.
steps.begin();
291 it != goto_trace.
steps.end();
294 if(it->thread_nr > max_thread_idx)
295 max_thread_idx = it->thread_nr;
296 if(it->is_assert() && !it->cond_value)
297 trace_has_violation =
true;
303 graphml[sink].node_name=
"sink";
304 graphml[sink].is_violation=
false;
305 graphml[sink].has_invariant=
false;
307 if(max_thread_idx > 0 && trace_has_violation)
309 std::vector<graphmlt::node_indext> nodes;
311 for(
unsigned int i = 0; i <= max_thread_idx + 1; ++i)
315 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
316 graphml[nodes.back()].has_invariant =
false;
319 for(
auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
324 const auto thread_id = std::distance(nodes.cbegin(), it);
326 data.set_attribute(
"key",
"createThread");
331 data.set_attribute(
"key",
"enterFunction");
334 graphml[*std::next(it)].
in[*it].xml_node = edge;
335 graphml[*it].
out[*std::next(it)].xml_node = edge;
344 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
346 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
347 for(goto_tracet::stepst::const_iterator
348 it=goto_trace.
steps.begin();
349 it!=goto_trace.
steps.end();
354 step_to_node[it->step_nr]=sink;
360 goto_tracet::stepst::const_iterator next=it;
362 if(next!=goto_trace.
steps.end() &&
364 it->full_lhs==next->full_lhs &&
365 it->pc->source_location==next->pc->source_location)
367 step_to_node[it->step_nr]=sink;
383 graphml[node].has_invariant=
false;
385 step_to_node[it->step_nr]=node;
391 for(goto_tracet::stepst::const_iterator
392 it=goto_trace.
steps.begin();
393 it!=goto_trace.
steps.end();
396 const std::size_t from=step_to_node[it->step_nr];
399 if(from == sink ||
graphml[from].is_violation)
405 auto next = std::next(it);
406 for(; next != goto_trace.
steps.end() &&
407 (step_to_node[next->step_nr] == sink ||
413 const std::size_t to=
414 next==goto_trace.
steps.end()?
415 sink:step_to_node[next->step_nr];
426 {{
"source",
graphml[from].node_name},
427 {
"target",
graphml[to].node_name}},
444 const auto lhs_object = it->get_lhs_object();
447 lhs_object.has_value())
449 const std::string &lhs_id =
id2string(lhs_object->get_identifier());
450 if(lhs_id.find(
"pthread_create::thread") != std::string::npos)
461 lhs_id.find(
"thread") == std::string::npos &&
462 lhs_id.find(
"mutex") == std::string::npos &&
463 (!it->full_lhs_value.is_constant() ||
464 !it->full_lhs_value.has_operands() ||
478 irep_idt function_id = it->function_id;
479 const symbolt *symbol_ptr =
nullptr;
482 function_id = lhs_id.substr(0, lhs_id.find(
"::"));
533 graphml[sink].node_name=
"sink";
534 graphml[sink].is_violation=
false;
535 graphml[sink].has_invariant=
false;
538 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
540 std::size_t step_nr=1;
541 for(symex_target_equationt::SSA_stepst::const_iterator
550 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
551 (it->is_goto() && it->source.pc->get_condition().is_true()) ||
555 step_to_node[step_nr]=sink;
561 symex_target_equationt::SSA_stepst::const_iterator next=it;
564 next->is_assignment() &&
565 it->ssa_full_lhs==next->ssa_full_lhs &&
566 it->source.pc->source_location==next->source.pc->source_location)
568 step_to_node[step_nr]=sink;
579 graphml[node].is_violation=
false;
580 graphml[node].has_invariant=
false;
582 step_to_node[step_nr]=node;
587 for(symex_target_equationt::SSA_stepst::const_iterator
592 const std::size_t from=step_to_node[step_nr];
601 symex_target_equationt::SSA_stepst::const_iterator next=it;
602 std::size_t next_step_nr=step_nr;
603 for(++next, ++next_step_nr;
605 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
606 ++next, ++next_step_nr)
610 const std::size_t to=
612 sink:step_to_node[next_step_nr];
623 {{
"source",
graphml[from].node_name},
624 {
"target",
graphml[to].node_name}},
638 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
639 it->ssa_full_lhs.is_not_nil())
641 irep_idt identifier = it->ssa_lhs.get_object_name();
643 graphml[to].has_invariant =
true;
675 step_nr=next_step_nr;