json_goto_trace.h File Reference

Traces of GOTO Programs. More...

#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 33 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 60 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 280 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 209 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 167 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 251 of file json_goto_trace.cpp.