41 if(expr.
id()==ID_symbol)
47 std::string identifier=
51 if(l0_l1!=std::string::npos)
53 identifier.resize(l0_l1);
75 if(cit !=
cache.end())
80 if(assign.
rhs().
id() == ID_array_list)
83 const auto &ops = array_list.
operands();
85 for(std::size_t listidx = 0; listidx != ops.size(); listidx += 2)
94 else if(assign.
rhs().
id() == ID_array)
110 else if(assign.
rhs().
id()==ID_struct ||
111 assign.
rhs().
id()==ID_union)
116 assign.
lhs().
id() == ID_member &&
124 else if(assign.
lhs().
id()==ID_byte_extract_little_endian ||
125 assign.
lhs().
id()==ID_byte_extract_big_endian)
138 exprt::operandst::const_iterator it=
140 for(
const auto &comp : components)
142 if(comp.type().id()==ID_code ||
143 comp.get_is_padding() ||
149 it != assign.
rhs().
operands().end(),
"expression must have operands");
161 if(assign.
rhs().
id()==ID_union)
165 else if(assign.
rhs().
id() == ID_with)
168 const auto &ops = with_expr.
operands();
170 for(std::size_t i = 1; i < ops.size(); i += 2)
175 if(ops[i].
id() == ID_member_name)
178 assign.
lhs(), ops[i].
get(ID_component_name), ops[i + 1].type()};
200 lhs.find(
"#return_value") != std::string::npos ||
201 (lhs.find(
'$') != std::string::npos &&
202 has_prefix(lhs,
"return_value___VERIFIER_nondet_")))
221 const goto_tracet::stepst::const_iterator &prev_it,
222 goto_tracet::stepst::const_iterator &it)
225 it->hidden && (!it->pc->is_assign() ||
226 it->pc->get_assign().rhs().id() != ID_side_effect ||
227 it->pc->get_assign().rhs().get(ID_statement) != ID_nondet))
230 if(!it->is_assignment() && !it->is_goto() && !it->is_assert())
236 if(prev_it!=goto_trace.
steps.end() &&
237 prev_it->pc->source_location==it->pc->source_location)
240 if(it->is_goto() && it->pc->get_condition().is_true())
245 if(source_location.
is_nil() ||
264 expr.
id() == ID_symbol &&
281 unsigned int max_thread_idx = 0;
282 bool trace_has_violation =
false;
283 for(goto_tracet::stepst::const_iterator it = goto_trace.
steps.begin();
284 it != goto_trace.
steps.end();
287 if(it->thread_nr > max_thread_idx)
288 max_thread_idx = it->thread_nr;
289 if(it->is_assert() && !it->cond_value)
290 trace_has_violation =
true;
296 graphml[sink].node_name=
"sink";
297 graphml[sink].is_violation=
false;
298 graphml[sink].has_invariant=
false;
300 if(max_thread_idx > 0 && trace_has_violation)
302 std::vector<graphmlt::node_indext> nodes;
304 for(
unsigned int i = 0; i <= max_thread_idx + 1; ++i)
308 graphml[nodes.back()].is_violation = i == max_thread_idx + 1;
309 graphml[nodes.back()].has_invariant =
false;
312 for(
auto it = nodes.cbegin(); std::next(it) != nodes.cend(); ++it)
317 const auto thread_id = std::distance(nodes.cbegin(), it);
319 data.set_attribute(
"key",
"createThread");
324 data.set_attribute(
"key",
"enterFunction");
327 graphml[*std::next(it)].
in[*it].xml_node = edge;
328 graphml[*it].
out[*std::next(it)].xml_node = edge;
337 std::vector<std::size_t> step_to_node(goto_trace.
steps.size()+1, 0);
339 goto_tracet::stepst::const_iterator prev_it=goto_trace.
steps.end();
340 for(goto_tracet::stepst::const_iterator
341 it=goto_trace.
steps.begin();
342 it!=goto_trace.
steps.end();
347 step_to_node[it->step_nr]=sink;
353 goto_tracet::stepst::const_iterator next=it;
355 if(next!=goto_trace.
steps.end() &&
357 it->full_lhs==next->full_lhs &&
358 it->pc->source_location==next->pc->source_location)
360 step_to_node[it->step_nr]=sink;
376 graphml[node].has_invariant=
false;
378 step_to_node[it->step_nr]=node;
384 for(goto_tracet::stepst::const_iterator
385 it=goto_trace.
steps.begin();
386 it!=goto_trace.
steps.end();
389 const std::size_t from=step_to_node[it->step_nr];
392 if(from == sink ||
graphml[from].is_violation)
398 auto next = std::next(it);
399 for(; next != goto_trace.
steps.end() &&
400 (step_to_node[next->step_nr] == sink ||
406 const std::size_t to=
407 next==goto_trace.
steps.end()?
408 sink:step_to_node[next->step_nr];
419 {{
"source",
graphml[from].node_name},
420 {
"target",
graphml[to].node_name}},
437 const auto lhs_object = it->get_lhs_object();
440 lhs_object.has_value())
442 const std::string &lhs_id =
id2string(lhs_object->get_identifier());
443 if(lhs_id.find(
"pthread_create::thread") != std::string::npos)
454 lhs_id.find(
"thread") == std::string::npos &&
455 lhs_id.find(
"mutex") == std::string::npos &&
456 (!it->full_lhs_value.is_constant() ||
457 !it->full_lhs_value.has_operands() ||
471 irep_idt function_id = it->function_id;
472 const symbolt *symbol_ptr =
nullptr;
475 function_id = lhs_id.substr(0, lhs_id.find(
"::"));
526 graphml[sink].node_name=
"sink";
527 graphml[sink].is_violation=
false;
528 graphml[sink].has_invariant=
false;
531 std::vector<std::size_t> step_to_node(equation.
SSA_steps.size()+1, 0);
533 std::size_t step_nr=1;
534 for(symex_target_equationt::SSA_stepst::const_iterator
543 (!it->is_assignment() && !it->is_goto() && !it->is_assert()) ||
544 (it->is_goto() && it->source.pc->get_condition().is_true()) ||
548 step_to_node[step_nr]=sink;
554 symex_target_equationt::SSA_stepst::const_iterator next=it;
557 next->is_assignment() &&
558 it->ssa_full_lhs==next->ssa_full_lhs &&
559 it->source.pc->source_location==next->source.pc->source_location)
561 step_to_node[step_nr]=sink;
572 graphml[node].is_violation=
false;
573 graphml[node].has_invariant=
false;
575 step_to_node[step_nr]=node;
580 for(symex_target_equationt::SSA_stepst::const_iterator
585 const std::size_t from=step_to_node[step_nr];
594 symex_target_equationt::SSA_stepst::const_iterator next=it;
595 std::size_t next_step_nr=step_nr;
596 for(++next, ++next_step_nr;
598 (step_to_node[next_step_nr]==sink || it->source.pc==next->source.pc);
599 ++next, ++next_step_nr)
603 const std::size_t to=
605 sink:step_to_node[next_step_nr];
616 {{
"source",
graphml[from].node_name},
617 {
"target",
graphml[to].node_name}},
631 (it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
632 it->ssa_full_lhs.is_not_nil())
634 irep_idt identifier = it->ssa_lhs.get_object_name();
636 graphml[to].has_invariant =
true;
668 step_nr=next_step_nr;