Skip to content

Commit 9d88bba

Browse files
tautschnigtautschnig
committed
GraphML witnesses: clang-format switch/case statement
1 parent c217c2e commit 9d88bba

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
@@ -439,78 +439,78 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
439439
case goto_trace_stept::typet::ASSERT:
440440
case goto_trace_stept::typet::GOTO:
441441
case goto_trace_stept::typet::SPAWN:
442+
{
443+
xmlt edge(
444+
"edge",
445+
{{"source", graphml[from].node_name},
446+
{"target", graphml[to].node_name}},
447+
{});
448+
442449
{
443-
xmlt edge(
444-
"edge",
445-
{{"source", graphml[from].node_name},
446-
{"target", graphml[to].node_name}},
447-
{});
450+
xmlt &data_f = edge.new_element("data");
451+
data_f.set_attribute("key", "originfile");
452+
data_f.data = id2string(graphml[from].file);
448453

449-
{
450-
xmlt &data_f=edge.new_element("data");
451-
data_f.set_attribute("key", "originfile");
452-
data_f.data=id2string(graphml[from].file);
454+
xmlt &data_l = edge.new_element("data");
455+
data_l.set_attribute("key", "startline");
456+
data_l.data = id2string(graphml[from].line);
453457

454-
xmlt &data_l=edge.new_element("data");
455-
data_l.set_attribute("key", "startline");
456-
data_l.data=id2string(graphml[from].line);
458+
xmlt &data_t = edge.new_element("data");
459+
data_t.set_attribute("key", "threadId");
460+
data_t.data = std::to_string(it->thread_nr);
461+
}
457462

458-
xmlt &data_t=edge.new_element("data");
459-
data_t.set_attribute("key", "threadId");
460-
data_t.data=std::to_string(it->thread_nr);
463+
const auto lhs_object = it->get_lhs_object();
464+
if(
465+
it->type == goto_trace_stept::typet::ASSIGNMENT &&
466+
lhs_object.has_value())
467+
{
468+
const std::string &lhs_id = id2string(lhs_object->get_identifier());
469+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
470+
{
471+
xmlt &data_t = edge.new_element("data");
472+
data_t.set_attribute("key", "createThread");
473+
data_t.data = std::to_string(++thread_id);
461474
}
462-
463-
const auto lhs_object = it->get_lhs_object();
464-
if(
465-
it->type == goto_trace_stept::typet::ASSIGNMENT &&
466-
lhs_object.has_value())
475+
else if(
476+
!contains_symbol_prefix(
477+
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
478+
!contains_symbol_prefix(
479+
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
480+
lhs_id.find("thread") == std::string::npos &&
481+
lhs_id.find("mutex") == std::string::npos &&
482+
(!it->full_lhs_value.is_constant() ||
483+
!it->full_lhs_value.has_operands() ||
484+
!has_prefix(
485+
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
467486
{
468-
const std::string &lhs_id = id2string(lhs_object->get_identifier());
469-
if(lhs_id.find("pthread_create::thread") != std::string::npos)
470-
{
471-
xmlt &data_t = edge.new_element("data");
472-
data_t.set_attribute("key", "createThread");
473-
data_t.data = std::to_string(++thread_id);
474-
}
475-
else if(
476-
!contains_symbol_prefix(
477-
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
478-
!contains_symbol_prefix(
479-
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
480-
lhs_id.find("thread") == std::string::npos &&
481-
lhs_id.find("mutex") == std::string::npos &&
482-
(!it->full_lhs_value.is_constant() ||
483-
!it->full_lhs_value.has_operands() ||
484-
!has_prefix(
485-
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
487+
xmlt &val = edge.new_element("data");
488+
val.set_attribute("key", "assumption");
489+
490+
code_assignt assign{it->full_lhs, it->full_lhs_value};
491+
val.data = convert_assign_rec(lhs_id, assign);
492+
493+
xmlt &val_s = edge.new_element("data");
494+
val_s.set_attribute("key", "assumption.scope");
495+
val_s.data = id2string(it->function_id);
496+
497+
if(has_prefix(val.data, "\\result ="))
486498
{
487-
xmlt &val = edge.new_element("data");
488-
val.set_attribute("key", "assumption");
489-
490-
code_assignt assign{it->full_lhs, it->full_lhs_value};
491-
val.data = convert_assign_rec(lhs_id, assign);
492-
493-
xmlt &val_s = edge.new_element("data");
494-
val_s.set_attribute("key", "assumption.scope");
495-
val_s.data = id2string(it->function_id);
496-
497-
if(has_prefix(val.data, "\\result ="))
498-
{
499-
xmlt &val_f = edge.new_element("data");
500-
val_f.set_attribute("key", "assumption.resultfunction");
501-
val_f.data = id2string(it->function_id);
502-
}
499+
xmlt &val_f = edge.new_element("data");
500+
val_f.set_attribute("key", "assumption.resultfunction");
501+
val_f.data = id2string(it->function_id);
503502
}
504503
}
505-
else if(it->type==goto_trace_stept::typet::GOTO &&
506-
it->pc->is_goto())
507-
{
508-
}
509-
510-
graphml[to].in[from].xml_node=edge;
511-
graphml[from].out[to].xml_node=edge;
512504
}
505+
else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
506+
{
507+
}
508+
509+
graphml[to].in[from].xml_node = edge;
510+
graphml[from].out[to].xml_node = edge;
511+
513512
break;
513+
}
514514

515515
case goto_trace_stept::typet::DECL:
516516
case goto_trace_stept::typet::FUNCTION_CALL:
@@ -628,40 +628,40 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
628628
case goto_trace_stept::typet::ASSERT:
629629
case goto_trace_stept::typet::GOTO:
630630
case goto_trace_stept::typet::SPAWN:
631+
{
632+
xmlt edge(
633+
"edge",
634+
{{"source", graphml[from].node_name},
635+
{"target", graphml[to].node_name}},
636+
{});
637+
631638
{
632-
xmlt edge(
633-
"edge",
634-
{{"source", graphml[from].node_name},
635-
{"target", graphml[to].node_name}},
636-
{});
639+
xmlt &data_f = edge.new_element("data");
640+
data_f.set_attribute("key", "originfile");
641+
data_f.data = id2string(graphml[from].file);
637642

638-
{
639-
xmlt &data_f=edge.new_element("data");
640-
data_f.set_attribute("key", "originfile");
641-
data_f.data=id2string(graphml[from].file);
643+
xmlt &data_l = edge.new_element("data");
644+
data_l.set_attribute("key", "startline");
645+
data_l.data = id2string(graphml[from].line);
646+
}
642647

643-
xmlt &data_l=edge.new_element("data");
644-
data_l.set_attribute("key", "startline");
645-
data_l.data=id2string(graphml[from].line);
646-
}
648+
if(
649+
(it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
650+
it->ssa_full_lhs.is_not_nil())
651+
{
652+
irep_idt identifier = it->ssa_lhs.get_object_name();
647653

648-
if((it->is_assignment() ||
649-
it->is_decl()) &&
650-
it->ssa_rhs.is_not_nil() &&
651-
it->ssa_full_lhs.is_not_nil())
652-
{
653-
irep_idt identifier=it->ssa_lhs.get_object_name();
654+
graphml[to].has_invariant = true;
655+
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
656+
graphml[to].invariant = convert_assign_rec(identifier, assign);
657+
graphml[to].invariant_scope = id2string(it->source.function_id);
658+
}
654659

655-
graphml[to].has_invariant=true;
656-
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
657-
graphml[to].invariant=convert_assign_rec(identifier, assign);
658-
graphml[to].invariant_scope = id2string(it->source.function_id);
659-
}
660+
graphml[to].in[from].xml_node = edge;
661+
graphml[from].out[to].xml_node = edge;
660662

661-
graphml[to].in[from].xml_node=edge;
662-
graphml[from].out[to].xml_node=edge;
663-
}
664663
break;
664+
}
665665

666666
case goto_trace_stept::typet::DECL:
667667
case goto_trace_stept::typet::FUNCTION_CALL:

0 commit comments

Comments
 (0)