cprover
json_goto_trace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: Daniel Kroening
6 
7 Date: 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"
18 
19 #include <util/json.h>
20 #include <util/json_stream.h>
21 #include <util/json_expr.h>
22 #include <util/invariant.h>
23 
27 typedef struct
28 {
29  const jsont &location;
31  const namespacet &ns;
34 
42 void convert_assert(
43  json_objectt &json_failure,
44  const conversion_dependenciest &conversion_dependencies);
45 
55 void convert_decl(
56  json_objectt &json_assignment,
57  const conversion_dependenciest &conversion_dependencies,
58  const trace_optionst &trace_options);
59 
67 void convert_output(
68  json_objectt &json_output,
69  const conversion_dependenciest &conversion_dependencies);
70 
78 void convert_input(
79  json_objectt &json_input,
80  const conversion_dependenciest &conversion_dependencies);
81 
89 void convert_return(
90  json_objectt &json_call_return,
91  const conversion_dependenciest &conversion_dependencies);
92 
101 void convert_default(
102  json_objectt &json_location_only,
103  const conversion_dependenciest &conversion_dependencies);
104 
115 template <typename json_arrayT>
116 void convert(
117  const namespacet &ns,
118  const goto_tracet &goto_trace,
119  json_arrayT &dest_array,
121 {
122  source_locationt previous_source_location;
123 
124  for(const auto &step : goto_trace.steps)
125  {
126  const source_locationt &source_location = step.pc->source_location;
127 
128  jsont json_location;
129 
130  source_location.is_not_nil() && !source_location.get_file().empty()
131  ? json_location = json(source_location)
132  : json_location = json_nullt();
133 
134  // NOLINTNEXTLINE(whitespace/braces)
135  conversion_dependenciest conversion_dependencies = {
136  json_location, step, ns, source_location};
137 
138  switch(step.type)
139  {
141  if(!step.cond_value)
142  {
143  json_objectt &json_failure = dest_array.push_back().make_object();
144  convert_assert(json_failure, conversion_dependencies);
145  }
146  break;
147 
150  {
151  json_objectt &json_assignment = dest_array.push_back().make_object();
152  convert_decl(json_assignment, conversion_dependencies, trace_options);
153  }
154  break;
155 
157  {
158  json_objectt &json_output = dest_array.push_back().make_object();
159  convert_output(json_output, conversion_dependencies);
160  }
161  break;
162 
164  {
165  json_objectt &json_input = dest_array.push_back().make_object();
166  convert_input(json_input, conversion_dependencies);
167  }
168  break;
169 
172  {
173  json_objectt &json_call_return = dest_array.push_back().make_object();
174  convert_return(json_call_return, conversion_dependencies);
175  }
176  break;
177 
178  default:
179  if(source_location != previous_source_location)
180  {
181  json_objectt &json_location_only = dest_array.push_back().make_object();
182  convert_default(json_location_only, conversion_dependencies);
183  }
184  }
185 
186  if(source_location.is_not_nil() && !source_location.get_file().empty())
187  previous_source_location = source_location;
188  }
189 }
190 
191 #endif // CPROVER_GOTO_PROGRAMS_JSON_GOTO_TRACE_H
convert_assert
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
Definition: json_goto_trace.cpp:34
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
json_stream.h
conversion_dependenciest::source_location
const source_locationt & source_location
Definition: json_goto_trace.h:32
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
convert_return
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
Definition: json_goto_trace.cpp:263
invariant.h
goto_trace_stept
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
jsont
Definition: json.h:23
json_objectt
Definition: json.h:244
goto_trace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
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.
Definition: json_goto_trace.cpp:71
goto_trace_stept::typet::OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
goto_trace_stept::typet::DECL
goto_trace_stept::typet::ASSERT
json_expr.h
goto_trace_stept::typet::ASSIGNMENT
conversion_dependenciest::step
const goto_trace_stept & step
Definition: json_goto_trace.h:30
conversion_dependenciest
This is structure is here to facilitate passing arguments to the conversion functions.
Definition: json_goto_trace.h:27
dstringt::empty
bool empty() const
Definition: dstring.h:75
goto_trace_stept::typet::INPUT
conversion_dependenciest::ns
const namespacet & ns
Definition: json_goto_trace.h:31
source_locationt
Definition: source_location.h:20
convert_output
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
Definition: json_goto_trace.cpp:177
convert_input
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
Definition: json_goto_trace.cpp:220
trace_optionst
Definition: goto_trace.h:196
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:206
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.
Definition: json_goto_trace.cpp:302
json.h
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
conversion_dependenciest::location
const jsont & location
Definition: json_goto_trace.h:29
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
convert
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.
Definition: json_goto_trace.h:116
goto_trace_stept::typet::FUNCTION_CALL
json_nullt
Definition: json.h:278