Loading...

Searching...

No Matches

json_goto_trace.cpp File Reference

Traces of GOTO Programs. More...

#include "json_goto_trace.h"
#include <util/invariant.h>
#include <util/namespace.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.

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_output (json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)

Convert an OUTPUT goto_trace step.

void convert_input (json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)

Convert an INPUT 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.

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