44 std::string result =
from_expr(ns,
id, expr);
77 const auto width =
bv_type->get_width();
114 xml_failure.set_attribute_bool(
"hidden", step.hidden);
115 xml_failure.set_attribute(
"thread", std::to_string(step.thread_nr));
116 xml_failure.set_attribute(
"step_nr", std::to_string(step.step_nr));
157 if(step.full_lhs.is_not_nil())
164 xml_assignment.set_attribute(
"thread", std::to_string(step.thread_nr));
165 xml_assignment.set_attribute(
"step_nr", std::to_string(step.step_nr));
169 step.assignment_type ==
185 xml_output.set_attribute_bool(
"hidden", step.hidden);
186 xml_output.set_attribute(
"thread", std::to_string(step.thread_nr));
187 xml_output.set_attribute(
"step_nr", std::to_string(step.step_nr));
192 for(
const auto &arg : step.io_args)
196 xml_output.new_element(
"value_expression").new_element(
xml(arg, ns));
206 xml_input.set_attribute_bool(
"hidden", step.hidden);
207 xml_input.set_attribute(
"thread", std::to_string(step.thread_nr));
208 xml_input.set_attribute(
"step_nr", std::to_string(step.step_nr));
210 for(
const auto &arg : step.io_args)
214 xml_input.new_element(
"value_expression").new_element(
xml(arg, ns));
224 std::string tag =
"function_call";
228 xml_call_return.set_attribute(
"thread", std::to_string(step.thread_nr));
229 xml_call_return.set_attribute(
"step_nr", std::to_string(step.step_nr));
245 std::string tag =
"function_return";
249 xml_call_return.set_attribute(
"thread", std::to_string(step.thread_nr));
250 xml_call_return.set_attribute(
"step_nr", std::to_string(step.step_nr));
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
Step of the trace of a GOTO program.
optionalt< symbol_exprt > get_lhs_object() const
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const irep_idt & get_file() const
array_exprt to_array_expr() const
convert string into array constant
source_locationt location
Source code location of definition of symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
const irep_idt & display_name() const
Return language specific display name if present.
irep_idt mode
Language mode.
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const std::string integer2binary(const mp_integer &n, std::size_t width)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
const string_constantt & to_string_constant(const exprt &expr)
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.
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Utilities for printing location info steps in the trace in a format agnostic way.
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
static std::string get_printable_xml(const namespacet &ns, const irep_idt &id, const exprt &expr)
Given an expression expr, produce a string representation that is printable in XML 1....
static void replace_string_constants_rec(exprt &expr)
Rewrite all string constants to their array counterparts.
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)