cprover
json_goto_trace.cpp File Reference

Traces of GOTO Programs. More...

#include "json_goto_trace.h"
#include "goto_trace.h"
#include <util/json_expr.h>
#include <util/json.h>
#include <util/json_stream.h>
#include <util/arith_tools.h>
#include <util/config.h>
#include <util/invariant.h>
#include <util/simplify_expr.h>
#include <util/json_irep.h>
#include <langapi/language_util.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 conversion_dependenciest &conversion_dependencies)
 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_failureThe JSON object that will contain the information about the step after this function has run.
conversion_dependenciesA structure that contains information the conversion function needs.

Definition at line 34 of file json_goto_trace.cpp.

References goto_trace_stept::comment, source_locationt::get_property_id(), goto_trace_stept::hidden, id2string(), goto_trace_stept::internal, jsont::is_null(), jsont::json_boolean(), conversion_dependenciest::location, goto_trace_stept::pc, conversion_dependenciest::source_location, conversion_dependenciest::step, goto_trace_stept::thread_nr, and to_string().

Referenced by convert().

◆ convert_decl()

void convert_decl ( json_objectt json_assignment,
const conversion_dependenciest conversion_dependencies,
const trace_optionst trace_options 
)

◆ convert_default()

void convert_default ( json_objectt json_location_only,
const conversion_dependenciest conversion_dependencies 
)

Convert all other types of steps not already handled by the other conversion functions.

Parameters
[out]json_location_onlyThe JSON object that will contain the information about the step after this function has run.
conversion_dependenciesA structure that contains information the conversion function needs.

Definition at line 295 of file json_goto_trace.cpp.

References goto_trace_stept::hidden, jsont::json_boolean(), conversion_dependenciest::location, conversion_dependenciest::step, goto_trace_stept::thread_nr, and to_string().

Referenced by convert().

◆ convert_input()

void convert_input ( json_objectt json_input,
const conversion_dependenciest conversion_dependencies 
)

Convert an INPUT goto_trace step.

Parameters
[out]json_inputThe JSON object that will contain the information about the step after this function has run.
conversion_dependenciesA structure that contains information the conversion function needs.

Definition at line 217 of file json_goto_trace.cpp.

References source_locationt::get_function(), goto_trace_stept::hidden, goto_trace_stept::internal, goto_trace_stept::io_args, goto_trace_stept::io_id, jsont::is_null(), json(), jsont::json_boolean(), conversion_dependenciest::location, namespacet::lookup(), jsont::make_array(), symbolt::mode, conversion_dependenciest::ns, goto_trace_stept::pc, json_arrayt::push_back(), conversion_dependenciest::step, goto_trace_stept::thread_nr, and to_string().

Referenced by convert().

◆ convert_output()

void convert_output ( json_objectt json_output,
const conversion_dependenciest conversion_dependencies 
)

Convert an OUTPUT goto_trace step.

Parameters
[out]json_outputThe JSON object that will contain the information about the step after this function has run.
conversion_dependenciesA structure that contains information the conversion function needs.

Definition at line 174 of file json_goto_trace.cpp.

References source_locationt::get_function(), goto_trace_stept::hidden, goto_trace_stept::internal, goto_trace_stept::io_args, goto_trace_stept::io_id, jsont::is_null(), json(), jsont::json_boolean(), conversion_dependenciest::location, namespacet::lookup(), jsont::make_array(), symbolt::mode, conversion_dependenciest::ns, goto_trace_stept::pc, json_arrayt::push_back(), conversion_dependenciest::step, goto_trace_stept::thread_nr, and to_string().

Referenced by convert().

◆ 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_returnThe JSON object that will contain the information about the step after this function has run.
conversion_dependenciesA structure that contains information the conversion function needs.

Definition at line 260 of file json_goto_trace.cpp.

References symbolt::display_name(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::hidden, goto_trace_stept::identifier, goto_trace_stept::internal, jsont::is_null(), json(), jsont::json_boolean(), conversion_dependenciest::location, symbolt::location, namespacet::lookup(), jsont::make_object(), conversion_dependenciest::ns, conversion_dependenciest::step, goto_trace_stept::thread_nr, to_string(), and goto_trace_stept::type.

Referenced by convert().