cprover
|
Traces of GOTO Programs. More...
#include "goto_trace.h"
#include <util/json.h>
#include <util/json_stream.h>
#include <util/json_expr.h>
#include <util/invariant.h>
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 conversion_dependenciest &conversion_dependencies) |
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... | |
Traces of GOTO Programs.
Definition in file json_goto_trace.h.
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.
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 116 of file json_goto_trace.h.
References goto_trace_stept::ASSERT, goto_trace_stept::ASSIGNMENT, convert_assert(), convert_decl(), convert_default(), convert_input(), convert_output(), convert_return(), goto_trace_stept::DECL, dstringt::empty(), goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, source_locationt::get_file(), goto_trace_stept::INPUT, irept::is_not_nil(), json(), jsont::make_object(), goto_trace_stept::OUTPUT, and goto_tracet::steps.
void convert_assert | ( | json_objectt & | json_failure, |
const conversion_dependenciest & | conversion_dependencies | ||
) |
Convert an ASSERT goto_trace step.
[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 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().
void convert_decl | ( | json_objectt & | json_assignment, |
const conversion_dependenciest & | conversion_dependencies, | ||
const trace_optionst & | trace_options | ||
) |
Convert a DECL goto_trace step.
[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 71 of file json_goto_trace.cpp.
References goto_trace_stept::ACTUAL_PARAMETER, irept::add(), goto_trace_stept::assignment_type, symbolt::base_name, json_irept::convert_from_irep(), DATA_INVARIANT, symbolt::display_name(), irept::find(), from_expr(), from_type(), goto_trace_stept::full_lhs, goto_trace_stept::full_lhs_value, symbol_exprt::get_identifier(), goto_trace_stept::hidden, irept::id(), goto_trace_stept::internal, INVARIANT, irept::is_not_nil(), jsont::is_null(), json(), jsont::json_boolean(), trace_optionst::json_full_lhs, goto_trace_stept::lhs_object, conversion_dependenciest::location, namespacet::lookup(), symbolt::mode, conversion_dependenciest::ns, expr_visitort::operator()(), simplify_expr(), conversion_dependenciest::step, goto_trace_stept::thread_nr, to_string(), to_symbol_expr(), and symbolt::type.
Referenced by convert().
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.
[out] | json_location_only | 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 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().
void convert_input | ( | json_objectt & | json_input, |
const conversion_dependenciest & | conversion_dependencies | ||
) |
Convert an INPUT goto_trace step.
[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 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().
void convert_output | ( | json_objectt & | json_output, |
const conversion_dependenciest & | conversion_dependencies | ||
) |
Convert an OUTPUT goto_trace step.
[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 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().
void convert_return | ( | json_objectt & | json_call_return, |
const conversion_dependenciest & | conversion_dependencies | ||
) |
Convert a FUNCTION_RETURN goto_trace step.
[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 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().