Skip to content

Commit ca263b5

Browse files
tautschnigtautschnig
committed
GraphML witnesses: clang-format switch/case statement
1 parent 5d000f6 commit ca263b5

File tree

1 file changed

+85
-87
lines changed

1 file changed

+85
-87
lines changed

‎src/goto-programs/graphml_witness.cpp

Lines changed: 85 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -429,76 +429,75 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
429429
case goto_trace_stept::typet::ASSERT:
430430
case goto_trace_stept::typet::GOTO:
431431
case goto_trace_stept::typet::SPAWN:
432+
{
433+
xmlt edge(
434+
"edge",
435+
{{"source", graphml[from].node_name},
436+
{"target", graphml[to].node_name}},
437+
{});
438+
432439
{
433-
xmlt edge(
434-
"edge",
435-
{{"source", graphml[from].node_name},
436-
{"target", graphml[to].node_name}},
437-
{});
440+
xmlt &data_f = edge.new_element("data");
441+
data_f.set_attribute("key", "originfile");
442+
data_f.data = id2string(graphml[from].file);
438443

439-
{
440-
xmlt &data_f=edge.new_element("data");
441-
data_f.set_attribute("key", "originfile");
442-
data_f.data=id2string(graphml[from].file);
444+
xmlt &data_l = edge.new_element("data");
445+
data_l.set_attribute("key", "startline");
446+
data_l.data = id2string(graphml[from].line);
443447

444-
xmlt &data_l=edge.new_element("data");
445-
data_l.set_attribute("key", "startline");
446-
data_l.data=id2string(graphml[from].line);
448+
xmlt &data_t = edge.new_element("data");
449+
data_t.set_attribute("key", "threadId");
450+
data_t.data = std::to_string(it->thread_nr);
451+
}
447452

448-
xmlt &data_t=edge.new_element("data");
449-
data_t.set_attribute("key", "threadId");
450-
data_t.data=std::to_string(it->thread_nr);
453+
const auto lhs_object = it->get_lhs_object();
454+
if(
455+
it->type == goto_trace_stept::typet::ASSIGNMENT &&
456+
lhs_object.has_value())
457+
{
458+
const std::string &lhs_id = id2string(lhs_object->get_identifier());
459+
if(lhs_id.find("pthread_create::thread") != std::string::npos)
460+
{
461+
xmlt &data_t = edge.new_element("data");
462+
data_t.set_attribute("key", "createThread");
463+
data_t.data = std::to_string(++thread_id);
451464
}
452-
453-
const auto lhs_object = it->get_lhs_object();
454-
if(
455-
it->type == goto_trace_stept::typet::ASSIGNMENT &&
456-
lhs_object.has_value())
465+
else if(
466+
!contains_symbol_prefix(
467+
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
468+
!contains_symbol_prefix(
469+
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
470+
lhs_id.find("thread") == std::string::npos &&
471+
lhs_id.find("mutex") == std::string::npos &&
472+
(!it->full_lhs_value.is_constant() ||
473+
!it->full_lhs_value.has_operands() ||
474+
!has_prefix(
475+
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
457476
{
458-
const std::string &lhs_id = id2string(lhs_object->get_identifier());
459-
if(lhs_id.find("pthread_create::thread") != std::string::npos)
460-
{
461-
xmlt &data_t = edge.new_element("data");
462-
data_t.set_attribute("key", "createThread");
463-
data_t.data = std::to_string(++thread_id);
464-
}
465-
else if(
466-
!contains_symbol_prefix(
467-
it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
468-
!contains_symbol_prefix(
469-
it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
470-
lhs_id.find("thread") == std::string::npos &&
471-
lhs_id.find("mutex") == std::string::npos &&
472-
(!it->full_lhs_value.is_constant() ||
473-
!it->full_lhs_value.has_operands() ||
474-
!has_prefix(
475-
id2string(it->full_lhs_value.op0().get(ID_value)), "INVALID-")))
477+
xmlt &val = edge.new_element("data");
478+
val.set_attribute("key", "assumption");
479+
480+
code_assignt assign{it->full_lhs, it->full_lhs_value};
481+
val.data = convert_assign_rec(lhs_id, assign);
482+
483+
xmlt &val_s = edge.new_element("data");
484+
val_s.set_attribute("key", "assumption.scope");
485+
val_s.data = id2string(it->function_id);
486+
487+
if(has_prefix(val.data, "\\result ="))
476488
{
477-
xmlt &val = edge.new_element("data");
478-
val.set_attribute("key", "assumption");
479-
480-
code_assignt assign{it->full_lhs, it->full_lhs_value};
481-
val.data = convert_assign_rec(lhs_id, assign);
482-
483-
xmlt &val_s = edge.new_element("data");
484-
val_s.set_attribute("key", "assumption.scope");
485-
val_s.data = id2string(it->function_id);
486-
487-
if(has_prefix(val.data, "\\result ="))
488-
{
489-
xmlt &val_f = edge.new_element("data");
490-
val_f.set_attribute("key", "assumption.resultfunction");
491-
val_f.data = id2string(it->function_id);
492-
}
489+
xmlt &val_f = edge.new_element("data");
490+
val_f.set_attribute("key", "assumption.resultfunction");
491+
val_f.data = id2string(it->function_id);
493492
}
494493
}
495-
else if(it->type==goto_trace_stept::typet::GOTO &&
496-
it->pc->is_goto())
497-
{
498-
}
494+
}
495+
else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
496+
{
497+
}
499498

500-
graphml[to].in[from].xml_node=edge;
501-
graphml[from].out[to].xml_node=edge;
499+
graphml[to].in[from].xml_node = edge;
500+
graphml[from].out[to].xml_node = edge;
502501
}
503502
break;
504503

@@ -618,38 +617,37 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
618617
case goto_trace_stept::typet::ASSERT:
619618
case goto_trace_stept::typet::GOTO:
620619
case goto_trace_stept::typet::SPAWN:
621-
{
622-
xmlt edge(
623-
"edge",
624-
{{"source", graphml[from].node_name},
625-
{"target", graphml[to].node_name}},
626-
{});
620+
{
621+
xmlt edge(
622+
"edge",
623+
{{"source", graphml[from].node_name},
624+
{"target", graphml[to].node_name}},
625+
{});
627626

628-
{
629-
xmlt &data_f=edge.new_element("data");
630-
data_f.set_attribute("key", "originfile");
631-
data_f.data=id2string(graphml[from].file);
627+
{
628+
xmlt &data_f = edge.new_element("data");
629+
data_f.set_attribute("key", "originfile");
630+
data_f.data = id2string(graphml[from].file);
632631

633-
xmlt &data_l=edge.new_element("data");
634-
data_l.set_attribute("key", "startline");
635-
data_l.data=id2string(graphml[from].line);
636-
}
632+
xmlt &data_l = edge.new_element("data");
633+
data_l.set_attribute("key", "startline");
634+
data_l.data = id2string(graphml[from].line);
635+
}
637636

638-
if((it->is_assignment() ||
639-
it->is_decl()) &&
640-
it->ssa_rhs.is_not_nil() &&
641-
it->ssa_full_lhs.is_not_nil())
642-
{
643-
irep_idt identifier=it->ssa_lhs.get_object_name();
637+
if(
638+
(it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
639+
it->ssa_full_lhs.is_not_nil())
640+
{
641+
irep_idt identifier = it->ssa_lhs.get_object_name();
644642

645-
graphml[to].has_invariant=true;
646-
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
647-
graphml[to].invariant=convert_assign_rec(identifier, assign);
648-
graphml[to].invariant_scope = id2string(it->source.function_id);
649-
}
643+
graphml[to].has_invariant = true;
644+
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
645+
graphml[to].invariant = convert_assign_rec(identifier, assign);
646+
graphml[to].invariant_scope = id2string(it->source.function_id);
647+
}
650648

651-
graphml[to].in[from].xml_node=edge;
652-
graphml[from].out[to].xml_node=edge;
649+
graphml[to].in[from].xml_node = edge;
650+
graphml[from].out[to].xml_node = edge;
653651
}
654652
break;
655653

0 commit comments

Comments
 (0)