#include "goto_trace.h"#include "structured_trace_util.h"#include <util/json.h>#include <util/json_irep.h>
Include dependency graph for json_goto_trace.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| struct | conversion_dependenciest |
| This is structure is here to facilitate passing arguments to the conversion functions. More... | |
Functions | |
| void | convert_assert (json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies) |
| Convert an ASSERT goto_trace step. More... | |
| void | convert_decl (json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options) |
| Convert a DECL goto_trace step. More... | |
| void | convert_output (json_objectt &json_output, const conversion_dependenciest &conversion_dependencies) |
| Convert an OUTPUT goto_trace step. More... | |
| void | convert_input (json_objectt &json_input, const conversion_dependenciest &conversion_dependencies) |
| Convert an INPUT goto_trace step. More... | |
| void | convert_return (json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies) |
| Convert a FUNCTION_RETURN goto_trace step. More... | |
| 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. More... | |
| template<typename json_arrayT > | |
| 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. More... | |
Detailed Description
Traces of GOTO Programs
Definition in file json_goto_trace.h.
Function Documentation
◆ convert()
template<typename json_arrayT >
| 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.
Works by dispatching to the more specialised conversion functions based on the type of the step that is being handled.
- Parameters
-
ns The namespace used for resolution of symbols. goto_trace The goto_trace from which we are going to convert the steps from. dest_array The JSON object that we are going to append the step information to. trace_options A list of trace options
Definition at line 113 of file json_goto_trace.h.
◆ convert_assert()
| void convert_assert | ( | json_objectt & | json_failure, |
| const conversion_dependenciest & | conversion_dependencies | ||
| ) |
Convert an ASSERT goto_trace step.
- Parameters
-
[out] json_failure The JSON object that will contain the information about the step after this function has run. conversion_dependencies A structure that contains information the conversion function needs.
Definition at line 32 of file json_goto_trace.cpp.
◆ convert_decl()
| void convert_decl | ( | json_objectt & | json_assignment, |
| const conversion_dependenciest & | conversion_dependencies, | ||
| const trace_optionst & | trace_options | ||
| ) |
Convert a DECL goto_trace step.
- Parameters
-
[out] json_assignment The JSON object that will contain the information about the step after this function has run. conversion_dependencies A structure that contains information the conversion function needs. trace_options Extra information used by this particular conversion function.
Definition at line 59 of file json_goto_trace.cpp.
◆ convert_default()
| 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.
- Parameters
-
[out] json_location_only The JSON object that will contain the information about the step after this function has run. default_step The procesed details about this step, see default_step_kind
Definition at line 279 of file json_goto_trace.cpp.
◆ convert_input()
| void convert_input | ( | json_objectt & | json_input, |
| const conversion_dependenciest & | conversion_dependencies | ||
| ) |
Convert an INPUT goto_trace step.
- Parameters
-
[out] json_input The JSON object that will contain the information about the step after this function has run. conversion_dependencies A structure that contains information the conversion function needs.
Definition at line 208 of file json_goto_trace.cpp.
◆ convert_output()
| void convert_output | ( | json_objectt & | json_output, |
| const conversion_dependenciest & | conversion_dependencies | ||
| ) |
Convert an OUTPUT goto_trace step.
- Parameters
-
[out] json_output The JSON object that will contain the information about the step after this function has run. conversion_dependencies A structure that contains information the conversion function needs.
Definition at line 166 of file json_goto_trace.cpp.
◆ convert_return()
| void convert_return | ( | json_objectt & | json_call_return, |
| const conversion_dependenciest & | conversion_dependencies | ||
| ) |
Convert a FUNCTION_RETURN goto_trace step.
- Parameters
-
[out] json_call_return The JSON object that will contain the information about the step after this function has run. conversion_dependencies A structure that contains information the conversion function needs.
Definition at line 250 of file json_goto_trace.cpp.
