30 dest=
xmlt(
"goto_trace");
34 for(
const auto &step : goto_trace.
steps)
40 xml_location=
xml(source_location);
49 if(step.pc->is_assert())
51 else if(step.pc->is_goto())
54 id2string(step.pc->source_location.get_function())+
66 if(xml_location.
name!=
"")
74 auto lhs_object=step.get_lhs_object();
76 lhs_object.has_value()?lhs_object->get_identifier():
irep_idt();
79 if(xml_location.
name!=
"")
83 auto lhs_object=step.get_lhs_object();
87 if(lhs_object.has_value() &&
88 !ns.
lookup(lhs_object->get_identifier(), symbol))
100 std::string full_lhs_string, full_lhs_value_string;
102 if(step.full_lhs.is_not_nil())
103 full_lhs_string=
from_expr(ns, identifier, step.full_lhs);
105 if(step.full_lhs_value.is_not_nil())
106 full_lhs_value_string=
107 from_expr(ns, identifier, step.full_lhs_value);
110 xml_assignment.
new_element(
"full_lhs_value").
data=full_lhs_value_string;
117 step.assignment_type==
119 "actual_parameter":
"state");
126 printf_formatter(
id2string(step.format_string), step.io_args);
127 std::string text=printf_formatter.
as_string();
136 if(xml_location.
name!=
"")
139 for(
const auto &arg : step.io_args)
144 new_element(
xml(arg, ns));
158 for(
const auto &arg : step.io_args)
163 new_element(
xml(arg, ns));
166 if(xml_location.
name!=
"")
173 std::string tag =
"function_call";
187 if(xml_location.
name !=
"")
194 std::string tag =
"function_return";
208 if(xml_location.
name!=
"")
214 if(source_location!=previous_source_location)
217 if(xml_location.
name!=
"")
233 previous_source_location=source_location;
irep_idt name
The unique identifier.
void set_attribute_bool(const std::string &attribute, bool value)
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 to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
xmlt xml(const source_locationt &location)
void set_attribute(const std::string &attribute, unsigned value)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const irep_idt & display_name() const
Return language specific display name if present.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
xmlt & new_element(const std::string &key)
irep_idt base_name
Base (non-scoped) name.
const irep_idt & get_property_id() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().