diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 83a727967c5..18153048c5b 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -124,11 +124,11 @@ xmlt ai_baset::output_xml( forall_goto_functions(f_it, goto_functions) { - xmlt function("function"); - function.set_attribute("name", id2string(f_it->first)); - function.set_attribute( - "body_available", - f_it->second.body_available() ? "true" : "false"); + xmlt function( + "function", + {{"name", id2string(f_it->first)}, + {"body_available", f_it->second.body_available() ? "true" : "false"}}, + {}); if(f_it->second.body_available()) { @@ -156,15 +156,11 @@ xmlt ai_baset::output_xml( forall_goto_program_instructions(i_it, goto_program) { - xmlt location; - location.set_attribute( - "location_number", - std::to_string(i_it->location_number)); - location.set_attribute( - "source_location", - i_it->source_location.as_string()); - - location.new_element(abstract_state_before(i_it)->output_xml(*this, ns)); + xmlt location( + "", + {{"location_number", std::to_string(i_it->location_number)}, + {"source_location", i_it->source_location.as_string()}}, + {abstract_state_before(i_it)->output_xml(*this, ns)}); // Ideally we need output_instruction_xml std::ostringstream out; diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index 4f5048b8268..8f3854ddbeb 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -250,9 +250,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals) { for(const auto &g : goal_map) { - xmlt xml_result("result"); - xml_result.set_attribute("property", id2string(g.first)); - xml_result.set_attribute("status", g.second.status_string()); + xmlt xml_result( + "result", + {{"property", id2string(g.first)}, + {"status", g.second.status_string()}}, + {}); if(g.second.status==goalt::statust::FAILURE) convert(bmc.ns, g.second.goto_trace, xml_result.new_element()); diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index ec27fb22fb4..5857471e3b7 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -293,10 +293,12 @@ bool bmc_covert::operator()() { const goalt &goal=goal_pair.second; - xmlt xml_result("goal"); - xml_result.set_attribute("id", id2string(goal_pair.first)); - xml_result.set_attribute("description", goal.description); - xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED"); + xmlt xml_result( + "goal", + {{"id", id2string(goal_pair.first)}, + {"description", goal.description}, + {"status", goal.satisfied ? "SATISFIED" : "FAILED"}}, + {}); if(goal.source_location.is_not_nil()) xml_result.new_element()=xml(goal.source_location); diff --git a/src/cbmc/fault_localization.cpp b/src/cbmc/fault_localization.cpp index 3ffa1eb0479..e9c84713af3 100644 --- a/src/cbmc/fault_localization.cpp +++ b/src/cbmc/fault_localization.cpp @@ -298,9 +298,7 @@ safety_checkert::resultt fault_localizationt::stop_on_fail() } case ui_message_handlert::uit::XML_UI: { - xmlt dest("fault-localization"); - xmlt xml_diagnosis=report_xml(ID_nil); - dest.new_element().swap(xml_diagnosis); + xmlt dest("fault-localization", {}, {report_xml(ID_nil)}); status() << dest; break; } diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index b1821cfde78..9b362b00ff9 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -264,9 +264,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: { - xmlt edge("edge"); - edge.set_attribute("source", graphml[from].node_name); - edge.set_attribute("target", graphml[to].node_name); + xmlt edge( + "edge", + {{"source", graphml[from].node_name}, + {"target", graphml[to].node_name}}, + {}); { xmlt &data_f=edge.new_element("data"); @@ -302,9 +304,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace) val.data="["+(it->cond_value ? cond : neg_cond)+"]"; #if 0 - xmlt edge2("edge"); - edge2.set_attribute("source", graphml[from].node_name); - edge2.set_attribute("target", graphml[sink].node_name); + xmlt edge2("edge", { + {"source", graphml[from].node_name}, + {"target", graphml[sink].node_name}}, {}); xmlt &data_f2=edge2.new_element("data"); data_f2.set_attribute("key", "originfile"); @@ -447,9 +449,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation) case goto_trace_stept::typet::ASSERT: case goto_trace_stept::typet::GOTO: { - xmlt edge("edge"); - edge.set_attribute("source", graphml[from].node_name); - edge.set_attribute("target", graphml[to].node_name); + xmlt edge( + "edge", + {{"source", graphml[from].node_name}, + {"target", graphml[to].node_name}}, + {}); { xmlt &data_f=edge.new_element("data"); diff --git a/src/goto-programs/loop_ids.cpp b/src/goto-programs/loop_ids.cpp index c460efa7bb9..c485c5a0f0b 100644 --- a/src/goto-programs/loop_ids.cpp +++ b/src/goto-programs/loop_ids.cpp @@ -59,8 +59,7 @@ void show_loop_ids( std::string id = id2string(function_identifier) + "." + std::to_string(loop_id); - xmlt xml_loop("loop"); - xml_loop.set_attribute("name", id); + xmlt xml_loop("loop", {{"name", id}}, {}); xml_loop.new_element("loop-id").data=id; xml_loop.new_element()=xml(it->source_location); std::cout << xml_loop << "\n"; diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp index 10428d870ca..353f1aa0f2f 100644 --- a/src/goto-programs/show_properties.cpp +++ b/src/goto-programs/show_properties.cpp @@ -73,9 +73,11 @@ void show_properties( case ui_message_handlert::uit::XML_UI: { // use me instead - xmlt xml_property("property"); - xml_property.set_attribute("name", id2string(property_id)); - xml_property.set_attribute("class", id2string(property_class)); + xmlt xml_property( + "property", + {{"name", id2string(property_id)}, + {"class", id2string(property_class)}}, + {}); xmlt &property_l=xml_property.new_element(); property_l=xml(source_location); diff --git a/src/util/xml.h b/src/util/xml.h index 17dea427664..51856c5576e 100644 --- a/src/util/xml.h +++ b/src/util/xml.h @@ -27,6 +27,13 @@ class xmlt typedef std::list elementst; typedef std::map attributest; + xmlt(std::string &&_name, attributest &&_attributes, elementst &&_elements) + : name(std::move(_name)), + attributes(std::move(_attributes)), + elements(std::move(_elements)) + { + } + std::string name, data; attributest attributes;