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/invariant.h>
20 #include <util/json.h>
21 #include <util/json_irep.h>
22 #include <util/json_stream.h>
23 
27 typedef struct
28 {
29  const jsont &location;
31  const namespacet &ns;
33 
41 void convert_assert(
42  json_objectt &json_failure,
43  const conversion_dependenciest &conversion_dependencies);
44 
54 void convert_decl(
55  json_objectt &json_assignment,
56  const conversion_dependenciest &conversion_dependencies,
57  const trace_optionst &trace_options);
58 
66 void convert_output(
67  json_objectt &json_output,
68  const conversion_dependenciest &conversion_dependencies);
69 
77 void convert_input(
78  json_objectt &json_input,
79  const conversion_dependenciest &conversion_dependencies);
80 
88 void convert_return(
89  json_objectt &json_call_return,
90  const conversion_dependenciest &conversion_dependencies);
91 
100 void convert_default(
101  json_objectt &json_location_only,
102  const conversion_dependenciest &conversion_dependencies);
103 
114 template <typename json_arrayT>
115 void convert(
116  const namespacet &ns,
117  const goto_tracet &goto_trace,
118  json_arrayT &dest_array,
120 {
121  source_locationt previous_source_location;
122 
123  for(const auto &step : goto_trace.steps)
124  {
125  const source_locationt &source_location = step.pc->source_location;
126 
127  jsont json_location;
128 
129  source_location.is_not_nil() && !source_location.get_file().empty()
130  ? json_location = json(source_location)
131  : json_location = json_nullt();
132 
133  // NOLINTNEXTLINE(whitespace/braces)
134  conversion_dependenciest conversion_dependencies = {
135  json_location, step, ns};
136 
137  switch(step.type)
138  {
140  if(!step.cond_value)
141  {
142  json_objectt &json_failure = dest_array.push_back().make_object();
143  convert_assert(json_failure, conversion_dependencies);
144  }
145  break;
146 
149  {
150  json_objectt &json_assignment = dest_array.push_back().make_object();
151  convert_decl(json_assignment, conversion_dependencies, trace_options);
152  }
153  break;
154 
156  {
157  json_objectt &json_output = dest_array.push_back().make_object();
158  convert_output(json_output, conversion_dependencies);
159  }
160  break;
161 
163  {
164  json_objectt &json_input = dest_array.push_back().make_object();
165  convert_input(json_input, conversion_dependencies);
166  }
167  break;
168 
171  {
172  json_objectt &json_call_return = dest_array.push_back().make_object();
173  convert_return(json_call_return, conversion_dependencies);
174  }
175  break;
176 
189  if(source_location != previous_source_location)
190  {
191  json_objectt &json_location_only = dest_array.push_back().make_object();
192  convert_default(json_location_only, conversion_dependencies);
193  }
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
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:32
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::typet::ASSUME
@ ASSUME
json_stream.h
invariant.h
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
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:250
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
jsont::make_object
json_objectt & make_object()
Definition: json.h:436
jsont
Definition: json.h:25
json_irep.h
json_objectt
Definition: json.h:298
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:92
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
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:59
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
goto_trace_stept::typet::DECL
@ DECL
goto_trace_stept::typet::ASSERT
@ ASSERT
goto_trace_stept::typet::NONE
@ NONE
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
goto_trace_stept::typet::ASSIGNMENT
@ 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:28
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
goto_trace_stept::typet::SPAWN
@ SPAWN
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:166
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::typet::GOTO
@ GOTO
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:208
trace_optionst
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:215
trace_optionst::default_options
static const trace_optionst default_options
Definition: goto_trace.h:232
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
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:287
json.h
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
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:36
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:115
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
json_nullt
Definition: json.h:413
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT