29 dest=
xmlt(
"goto_trace");
33 for(
const auto &step : goto_trace.
steps)
39 xml_location=
xml(source_location);
48 if(step.pc->is_assert())
50 else if(step.pc->is_goto())
53 id2string(step.pc->source_location.get_function())+
54 ".unwind."+std::to_string(step.pc->loop_number);
60 xml_failure.
set_attribute(
"thread", std::to_string(step.thread_nr));
61 xml_failure.
set_attribute(
"step_nr", std::to_string(step.step_nr));
65 if(xml_location.
name!=
"")
73 irep_idt identifier=step.lhs_object.get_identifier();
76 if(xml_location.
name!=
"")
79 std::string value_string, binary_string, type_string,
80 full_lhs_string, full_lhs_value_string;
82 if(step.lhs_object_value.is_not_nil())
83 value_string=
from_expr(ns, identifier, step.lhs_object_value);
85 if(step.full_lhs.is_not_nil())
86 full_lhs_string=
from_expr(ns, identifier, step.full_lhs);
88 if(step.full_lhs_value.is_not_nil())
89 full_lhs_value_string=
90 from_expr(ns, identifier, step.full_lhs_value);
92 if(step.lhs_object_value.type().is_not_nil())
94 from_type(ns, identifier, step.lhs_object_value.type());
99 if(!ns.
lookup(identifier, symbol))
111 xml_assignment.
new_element(
"full_lhs_value").
data=full_lhs_value_string;
115 xml_assignment.
set_attribute(
"thread", std::to_string(step.thread_nr));
119 xml_assignment.
set_attribute(
"step_nr", std::to_string(step.step_nr));
122 step.assignment_type==
124 "actual_parameter":
"state");
126 if(step.lhs_object_value.is_not_nil())
128 new_element(
xml(step.lhs_object_value, ns));
135 printf_formatter(
id2string(step.format_string), step.io_args);
136 std::string text=printf_formatter.
as_string();
142 xml_output.
set_attribute(
"thread", std::to_string(step.thread_nr));
143 xml_output.
set_attribute(
"step_nr", std::to_string(step.step_nr));
145 if(xml_location.
name!=
"")
148 for(
const auto &arg : step.io_args)
152 new_element(
xml(arg, ns));
163 xml_input.
set_attribute(
"thread", std::to_string(step.thread_nr));
164 xml_input.
set_attribute(
"step_nr", std::to_string(step.step_nr));
166 for(
const auto &arg : step.io_args)
170 new_element(
xml(arg, ns));
173 if(xml_location.
name!=
"")
183 "function_call":
"function_return";
187 xml_call_return.
set_attribute(
"thread", std::to_string(step.thread_nr));
188 xml_call_return.
set_attribute(
"step_nr", std::to_string(step.step_nr));
197 if(xml_location.
name!=
"")
203 if(source_location!=previous_source_location)
206 if(xml_location.
name!=
"")
212 "thread", std::to_string(step.thread_nr));
214 "step_nr", std::to_string(step.step_nr));
222 previous_source_location=source_location;
void set_attribute_bool(const std::string &attribute, bool value)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
const std::string & id2string(const irep_idt &d)
irep_idt mode
Language mode.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
xmlt xml(const source_locationt &location)
void set_attribute(const std::string &attribute, unsigned value)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
xmlt & new_element(const std::string &name)
const irep_idt & display_name() const
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
irep_idt base_name
Base (non-scoped) name.
const irep_idt & get_property_id() const