Skip to content

Commit dc199a9

Browse files
tautschnigtautschnig
committed
GraphML witnesses: clang-format switch/case statement
1 parent 00b6031 commit dc199a9

File tree

1 file changed

+85
-87
lines changed

1 file changed

+85
-87
lines changed

‎src/goto-programs/graphml_witness.cpp

+85-87
Original file line numberDiff line numberDiff line change
@@ -427,76 +427,75 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
427427
case goto_trace_stept::typet::ASSERT:
428428
case goto_trace_stept::typet::GOTO:
429429
case goto_trace_stept::typet::SPAWN:
430+
{
431+
xmlt edge(
432+
"edge",
433+
{{"source", graphml[from].node_name},
434+
{"target", graphml[to].node_name}},
435+
{});
436+
430437
{
431-
xmlt edge(
432-
"edge",
433-
{{"source", graphml[from].node_name},
434-
{"target", graphml[to].node_name}},
435-
{});
438+
xmlt &data_f = edge.new_element("data");
439+
data_f.set_attribute("key", "originfile");
440+
data_f.data = id2string(graphml[from].file);
436441

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

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

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

498-
graphml[to].in[from].xml_node=edge;
499-
graphml[from].out[to].xml_node=edge;
497+
graphml[to].in[from].xml_node = edge;
498+
graphml[from].out[to].xml_node = edge;
500499
}
501500
break;
502501

@@ -616,38 +615,37 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
616615
case goto_trace_stept::typet::ASSERT:
617616
case goto_trace_stept::typet::GOTO:
618617
case goto_trace_stept::typet::SPAWN:
619-
{
620-
xmlt edge(
621-
"edge",
622-
{{"source", graphml[from].node_name},
623-
{"target", graphml[to].node_name}},
624-
{});
618+
{
619+
xmlt edge(
620+
"edge",
621+
{{"source", graphml[from].node_name},
622+
{"target", graphml[to].node_name}},
623+
{});
625624

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

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

636-
if((it->is_assignment() ||
637-
it->is_decl()) &&
638-
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();
635+
if(
636+
(it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
637+
it->ssa_full_lhs.is_not_nil())
638+
{
639+
irep_idt identifier = it->ssa_lhs.get_object_name();
642640

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-
}
641+
graphml[to].has_invariant = true;
642+
code_assignt assign(it->ssa_lhs, it->ssa_rhs);
643+
graphml[to].invariant = convert_assign_rec(identifier, assign);
644+
graphml[to].invariant_scope = id2string(it->source.function_id);
645+
}
648646

649-
graphml[to].in[from].xml_node=edge;
650-
graphml[from].out[to].xml_node=edge;
647+
graphml[to].in[from].xml_node = edge;
648+
graphml[from].out[to].xml_node = edge;
651649
}
652650
break;
653651

0 commit comments

Comments
 (0)