json_goto_trace.cpp File Reference

#include "json_goto_trace.h"
#include <util/invariant.h>
#include <util/simplify_expr.h>
#include <util/symbol.h>
#include <langapi/language_util.h>
#include "goto_trace.h"
#include "json_expr.h"

Include dependency graph for json_goto_trace.cpp:

Go to the source code of this file.

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...

Detailed Description

Traces of GOTO Programs

Definition in file json_goto_trace.cpp.

Function Documentation

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.