Skip to content

Commit d350db8

Browse files
tautschnigtautschnig
committed
GraphML witnesses: clang-format switch/case statement
1 parent b8ea9a2 commit d350db8

File tree

1 file changed

+88
-88
lines changed

1 file changed

+88
-88
lines changed

‎src/goto-programs/graphml_witness.cpp

+88-88
Original file line numberDiff line numberDiff line change
@@ -413,78 +413,78 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
413413
case goto_trace_stept::typet::ASSERT:
414414
case goto_trace_stept::typet::GOTO:
415415
case goto_trace_stept::typet::SPAWN:
416+
{
417+
xmlt edge(
418+
"edge",
419+
{{"source", graphml[from].node_name},
420+
{"target", graphml[to].node_name}},
421+
{});
422+
416423
{
417-
xmlt edge(
418-
"edge",
419-
{{"source", graphml[from].node_name},
420-
{"target", graphml[to].node_name}},
421-
{});
424+
xmlt &data_f = edge.new_element("data");
425+
data_f.set_attribute("key", "originfile");
426+
data_f.data = id2string(graphml[from].file);
422427

423-
{
424-
xmlt &data_f=edge.new_element("data");
425-
data_f.set_attribute("key", "originfile");
426-
data_f.data=id2string(graphml[from].file);
428+
xmlt &data_l = edge.new_element("data");
429+
data_l.set_attribute("key", "startline");
430+
data_l.data = id2string(graphml[from].line);
427431

428-
xmlt &data_l=edge.new_element("data");
429-
data_l.set_attribute("key", "startline");
430-
data_l.data=id2string(graphml[from].line);
432+
xmlt &data_t = edge.new_element("data");
433+
data_t.set_attribute("key", "threadId");
434+
data_t.data = std::to_string(it->thread_nr);
435+
}
431436

432-
xmlt &data_t=edge.new_element("data");
433-
data_t.set_attribute("key", "threadId");
434-
data_t.data=std::to_string(it->thread_nr);
437+
const auto lhs_object = it->get_lhs_object();
438+
if(
439+
it->type == goto_trace_stept::typet::ASSIGNMENT &&
440+
lhs_object.has_value())
441+
{
442+
const std::string &lhs_id = id2string(lhs_object->get_identifier());
443+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
444+
{
445+
xmlt &data_t = edge.new_element("data");
446+
data_t.set_attribute("key", "createThread");
447+
data_t.data = std::to_string(++thread_id);
435448
}
436-
437-
const auto lhs_object = it->get_lhs_object();
438-
if(
439-
it->type == goto_trace_stept::typet::ASSIGNMENT &&
440-
lhs_object.has_value())
449+
else if(
450+
!contains_symbol_prefix(
451+
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
452+
!contains_symbol_prefix(
453+
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
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() ||
458+
!has_prefix(
459+
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
441460
{
442-
const std::string &lhs_id = id2string(lhs_object->get_identifier());
443-
if(lhs_id.find("pthread_create::thread") != std::string::npos)
444-
{
445-
xmlt &data_t = edge.new_element("data");
446-
data_t.set_attribute("key", "createThread");
447-
data_t.data = std::to_string(++thread_id);
448-
}
449-
else if(
450-
!contains_symbol_prefix(
451-
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
452-
!contains_symbol_prefix(
453-
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
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() ||
458-
!has_prefix(
459-
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
461+
xmlt &val = edge.new_element("data");
462+
val.set_attribute("key", "assumption");
463+
464+
code_assignt assign{it->full_lhs, it->full_lhs_value};
465+
val.data = convert_assign_rec(lhs_id, assign);
466+
467+
xmlt &val_s = edge.new_element("data");
468+
val_s.set_attribute("key", "assumption.scope");
469+
val_s.data = id2string(it->function_id);
470+
471+
if(has_prefix(val.data, "\\result ="))
460472
{
461-
xmlt &val = edge.new_element("data");
462-
val.set_attribute("key", "assumption");
463-
464-
code_assignt assign{it->full_lhs, it->full_lhs_value};
465-
val.data = convert_assign_rec(lhs_id, assign);
466-
467-
xmlt &val_s = edge.new_element("data");
468-
val_s.set_attribute("key", "assumption.scope");
469-
val_s.data = id2string(it->function_id);
470-
471-
if(has_prefix(val.data, "\\result ="))
472-
{
473-
xmlt &val_f = edge.new_element("data");
474-
val_f.set_attribute("key", "assumption.resultfunction");
475-
val_f.data = id2string(it->function_id);
476-
}
473+
xmlt &val_f = edge.new_element("data");
474+
val_f.set_attribute("key", "assumption.resultfunction");
475+
val_f.data = id2string(it->function_id);
477476
}
478477
}
479-
else if(it->type==goto_trace_stept::typet::GOTO &&
480-
it->pc->is_goto())
481-
{
482-
}
483-
484-
graphml[to].in[from].xml_node=edge;
485-
graphml[from].out[to].xml_node=edge;
486478
}
479+
else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
480+
{
481+
}
482+
483+
graphml[to].in[from].xml_node = edge;
484+
graphml[from].out[to].xml_node = edge;
485+
487486
break;
487+
}
488488

489489
case goto_trace_stept::typet::DECL:
490490
case goto_trace_stept::typet::FUNCTION_CALL:
@@ -602,40 +602,40 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
602602
case goto_trace_stept::typet::ASSERT:
603603
case goto_trace_stept::typet::GOTO:
604604
case goto_trace_stept::typet::SPAWN:
605+
{
606+
xmlt edge(
607+
"edge",
608+
{{"source", graphml[from].node_name},
609+
{"target", graphml[to].node_name}},
610+
{});
611+
605612
{
606-
xmlt edge(
607-
"edge",
608-
{{"source", graphml[from].node_name},
609-
{"target", graphml[to].node_name}},
610-
{});
613+
xmlt &data_f = edge.new_element("data");
614+
data_f.set_attribute("key", "originfile");
615+
data_f.data = id2string(graphml[from].file);
611616

612-
{
613-
xmlt &data_f=edge.new_element("data");
614-
data_f.set_attribute("key", "originfile");
615-
data_f.data=id2string(graphml[from].file);
617+
xmlt &data_l = edge.new_element("data");
618+
data_l.set_attribute("key", "startline");
619+
data_l.data = id2string(graphml[from].line);
620+
}
616621

617-
xmlt &data_l=edge.new_element("data");
618-
data_l.set_attribute("key", "startline");
619-
data_l.data=id2string(graphml[from].line);
620-
}
622+
if(
623+
(it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
624+
it->ssa_full_lhs.is_not_nil())
625+
{
626+
irep_idt identifier = it->ssa_lhs.get_object_name();
621627

622-
if((it->is_assignment() ||
623-
it->is_decl()) &&
624-
it->ssa_rhs.is_not_nil() &&
625-
it->ssa_full_lhs.is_not_nil())
626-
{
627-
irep_idt identifier=it->ssa_lhs.get_object_name();
628+
graphml[to].has_invariant = true;
629+
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
630+
graphml[to].invariant = convert_assign_rec(identifier, assign);
631+
graphml[to].invariant_scope = id2string(it->source.function_id);
632+
}
628633

629-
graphml[to].has_invariant=true;
630-
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
631-
graphml[to].invariant=convert_assign_rec(identifier, assign);
632-
graphml[to].invariant_scope = id2string(it->source.function_id);
633-
}
634+
graphml[to].in[from].xml_node = edge;
635+
graphml[from].out[to].xml_node = edge;
634636

635-
graphml[to].in[from].xml_node=edge;
636-
graphml[from].out[to].xml_node=edge;
637-
}
638637
break;
638+
}
639639

640640
case goto_trace_stept::typet::DECL:
641641
case goto_trace_stept::typet::FUNCTION_CALL:

0 commit comments

Comments
 (0)