Skip to content

Commit 7baa16c

Browse files
tautschnigtautschnig
committed
GraphML witnesses: clang-format switch/case statement
1 parent b686a8f commit 7baa16c

File tree

1 file changed

+88
-88
lines changed

1 file changed

+88
-88
lines changed

‎src/goto-programs/graphml_witness.cpp

Lines changed: 88 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -429,78 +429,78 @@ 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-
}
499-
500-
graphml[to].in[from].xml_node=edge;
501-
graphml[from].out[to].xml_node=edge;
502494
}
495+
else if(it->type == goto_trace_stept::typet::GOTO && it->pc->is_goto())
496+
{
497+
}
498+
499+
graphml[to].in[from].xml_node = edge;
500+
graphml[from].out[to].xml_node = edge;
501+
503502
break;
503+
}
504504

505505
case goto_trace_stept::typet::DECL:
506506
case goto_trace_stept::typet::FUNCTION_CALL:
@@ -618,40 +618,40 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
618618
case goto_trace_stept::typet::ASSERT:
619619
case goto_trace_stept::typet::GOTO:
620620
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+
{});
627+
621628
{
622-
xmlt edge(
623-
"edge",
624-
{{"source", graphml[from].node_name},
625-
{"target", graphml[to].node_name}},
626-
{});
629+
xmlt &data_f = edge.new_element("data");
630+
data_f.set_attribute("key", "originfile");
631+
data_f.data = id2string(graphml[from].file);
627632

628-
{
629-
xmlt &data_f=edge.new_element("data");
630-
data_f.set_attribute("key", "originfile");
631-
data_f.data=id2string(graphml[from].file);
633+
xmlt &data_l = edge.new_element("data");
634+
data_l.set_attribute("key", "startline");
635+
data_l.data = id2string(graphml[from].line);
636+
}
632637

633-
xmlt &data_l=edge.new_element("data");
634-
data_l.set_attribute("key", "startline");
635-
data_l.data=id2string(graphml[from].line);
636-
}
638+
if(
639+
(it->is_assignment() || it->is_decl()) && it->ssa_rhs.is_not_nil() &&
640+
it->ssa_full_lhs.is_not_nil())
641+
{
642+
irep_idt identifier = it->ssa_lhs.get_object_name();
637643

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

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-
}
650+
graphml[to].in[from].xml_node = edge;
651+
graphml[from].out[to].xml_node = edge;
650652

651-
graphml[to].in[from].xml_node=edge;
652-
graphml[from].out[to].xml_node=edge;
653-
}
654653
break;
654+
}
655655

656656
case goto_trace_stept::typet::DECL:
657657
case goto_trace_stept::typet::FUNCTION_CALL:

0 commit comments

Comments
 (0)