CBMC
Loading...
Searching...
No Matches
json_goto_trace.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs
4
5Author: Daniel Kroening
6
7Date: November 2005
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
15#define CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
16
17#include "goto_trace.h"
19
20#include <util/json.h>
21#include <util/json_irep.h>
22
26typedef struct
27{
30 const namespacet &ns;
32
43
53void convert_decl(
57
68
76void convert_input(
79
90
101
112template <typename json_arrayT>
114 const namespacet &ns,
115 const goto_tracet &goto_trace,
118{
120
121 for(const auto &step : goto_trace.steps)
122 {
123 const source_locationt &source_location = step.pc->source_location();
124
126
127 source_location.is_not_nil() && !source_location.get_file().empty()
128 ? json_location = json(source_location)
130
131 // NOLINTNEXTLINE(whitespace/braces)
133 json_location, step, ns};
134
135 switch(step.type)
136 {
138 if(!step.cond_value)
139 {
140 json_objectt &json_failure = dest_array.push_back().make_object();
142 }
143 break;
144
147 {
148 json_objectt &json_assignment = dest_array.push_back().make_object();
150 }
151 break;
152
154 {
155 json_objectt &json_output = dest_array.push_back().make_object();
157 }
158 break;
159
161 {
162 json_objectt &json_input = dest_array.push_back().make_object();
164 }
165 break;
166
169 {
170 json_objectt &json_call_return = dest_array.push_back().make_object();
172 }
173 break;
174
188 if(default_step)
189 {
190 json_objectt &json_location_only = dest_array.push_back().make_object();
192 }
193 break;
194 }
195
196 if(source_location.is_not_nil() && !source_location.get_file().empty())
197 previous_source_location = source_location;
198 }
199}
200
201#endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Step of the trace of a GOTO program.
Definition goto_trace.h:50
Trace of a GOTO program.
Definition goto_trace.h:177
bool is_not_nil() const
Definition irep.h:372
Definition json.h:27
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const irep_idt & get_file() const
Traces of GOTO Programs.
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
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.
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT 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_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.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
This is structure is here to facilitate passing arguments to the conversion functions.
const goto_trace_stept & step
const namespacet & ns
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:221
static const trace_optionst default_options
Definition goto_trace.h:238
std::optional< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Utilities for printing location info steps in the trace in a format agnostic way.