Go to the documentation of this file.
30 xmlt value_xml{
"full_lhs_value"};
38 lhs_object.has_value() ? lhs_object->get_identifier() :
irep_idt();
39 value_xml.data =
from_expr(ns, identifier, value);
41 const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.
type());
42 const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
43 if(bv_type && constant)
45 const auto width = bv_type->get_width();
51 const auto binary_representation =
53 value_xml.set_attribute(
"binary", binary_representation);
63 dest=
xmlt(
"goto_trace");
67 for(
const auto &step : goto_trace.
steps)
73 xml_location=
xml(source_location);
88 if(!xml_location.
name.empty())
96 auto lhs_object = step.get_lhs_object();
98 lhs_object.has_value() ? lhs_object->get_identifier() :
irep_idt();
101 if(!xml_location.
name.empty())
108 lhs_object.has_value() &&
109 !ns.
lookup(lhs_object->get_identifier(), symbol))
123 std::string full_lhs_string;
125 if(step.full_lhs.is_not_nil())
126 full_lhs_string =
from_expr(ns, identifier, step.full_lhs);
137 step.assignment_type ==
147 printf_formatter(
id2string(step.format_string), step.io_args);
148 std::string text = printf_formatter.
as_string();
157 if(!xml_location.
name.empty())
160 for(
const auto &arg : step.io_args)
178 for(
const auto &arg : step.io_args)
185 if(!xml_location.
name.empty())
192 std::string tag =
"function_call";
206 if(!xml_location.
name.empty())
213 std::string tag =
"function_return";
227 if(!xml_location.
name.empty())
248 xmlt &xml_location_only =
265 previous_source_location=source_location;
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
optionalt< symbol_exprt > get_lhs_object() const
const irep_idt & display_name() const
Return language specific display name if present.
typet type
Type of symbol.
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
std::string default_step_name(const default_step_kindt &step_type)
Turns a default_step_kindt into a string that can be used in the trace.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Step of the trace of a GOTO program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
irep_idt mode
Language mode.
const std::string & id2string(const irep_idt &d)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
void set_attribute(const std::string &attribute, unsigned value)
source_locationt location
Source code location of definition of symbol.
void set_attribute_bool(const std::string &attribute, bool value)
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
const irep_idt & get_file() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
Utilities for printing location info steps in the trace in a format agnostic way.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
irep_idt name
The unique identifier.
xmlt & new_element(const std::string &key)