14#ifndef CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
15#define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
112template <
typename json_arrayT>
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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...
const irep_idt & get_file() const
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
void convert(const namespacet &ns, const goto_tracet &goto_trace, json_arrayT &dest_array, trace_optionst trace_options=trace_optionst::default_options)
Templated version of the conversion method.
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
void convert_decl(json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options)
Convert a DECL goto_trace step.
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
void convert_default(json_objectt &json_location_only, const default_trace_stept &default_step)
Convert all other types of steps not already handled by the other conversion functions.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
This is structure is here to facilitate passing arguments to the conversion functions.
const goto_trace_stept & step
Options for printing the trace using show_goto_trace.
static const trace_optionst default_options
std::optional< 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.