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 irep_idt identifier=step.lhs_object.get_identifier();
77 if(xml_location.
name!=
"")
80 std::string value_string, type_string,
81 full_lhs_string, full_lhs_value_string;
83 if(step.lhs_object_value.is_not_nil())
84 value_string=
from_expr(ns, identifier, step.lhs_object_value);
86 if(step.full_lhs.is_not_nil())
87 full_lhs_string=
from_expr(ns, identifier, step.full_lhs);
89 if(step.full_lhs_value.is_not_nil())
90 full_lhs_value_string=
91 from_expr(ns, identifier, step.full_lhs_value);
93 if(step.lhs_object_value.type().is_not_nil())
95 from_type(ns, identifier, step.lhs_object_value.type());
100 if(!ns.
lookup(identifier, symbol))
112 xml_assignment.
new_element(
"full_lhs_value").
data=full_lhs_value_string;
123 step.assignment_type==
125 "actual_parameter":
"state");
127 if(step.lhs_object_value.is_not_nil())
129 new_element(
xml(step.lhs_object_value, ns));
136 printf_formatter(
id2string(step.format_string), step.io_args);
137 std::string text=printf_formatter.
as_string();
146 if(xml_location.
name!=
"")
149 for(
const auto &arg : step.io_args)
154 new_element(
xml(arg, ns));
168 for(
const auto &arg : step.io_args)
173 new_element(
xml(arg, ns));
176 if(xml_location.
name!=
"")
186 "function_call":
"function_return";
200 if(xml_location.
name!=
"")
206 if(source_location!=previous_source_location)
209 if(xml_location.
name!=
"")
225 previous_source_location=source_location;
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 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)
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)
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.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const irep_idt & get_property_id() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().