31 for(
const auto &step : goto_trace.
steps)
38 json_location=
json(source_location);
49 if(step.pc->is_assert())
51 else if(step.pc->is_goto())
54 id2string(step.pc->source_location.get_function())+
55 ".unwind."+std::to_string(step.pc->loop_number);
62 json_failure[
"thread"]=
json_numbert(std::to_string(step.thread_nr));
67 json_failure[
"sourceLocation"]=json_location;
74 irep_idt identifier=step.lhs_object.get_identifier();
80 json_assignment[
"sourceLocation"]=json_location;
82 std::string value_string, binary_string, type_string, full_lhs_string;
85 if(step.full_lhs.is_not_nil())
86 full_lhs_string=
from_expr(ns, identifier, step.full_lhs);
89 if(it.full_lhs_value.is_not_nil())
90 full_lhs_value_string=
from_expr(ns, identifier, it.full_lhs_value);
93 if(step.full_lhs_value.is_not_nil())
94 full_lhs_value =
json(step.full_lhs_value, ns);
99 if(!ns.
lookup(identifier, symbol))
109 json_assignment[
"value"]=full_lhs_value;
112 json_assignment[
"thread"]=
json_numbert(std::to_string(step.thread_nr));
114 json_assignment[
"assignmentType"]=
116 step.assignment_type==
129 json_output[
"thread"]=
json_numbert(std::to_string(step.thread_nr));
134 for(
const auto &arg : step.io_args)
143 json_output[
"sourceLocation"]=json_location;
153 json_input[
"thread"]=
json_numbert(std::to_string(step.thread_nr));
158 for(
const auto &arg : step.io_args)
167 json_input[
"sourceLocation"]=json_location;
176 "function-call":
"function-return";
181 json_call_return[
"thread"]=
json_numbert(std::to_string(step.thread_nr));
185 json_function[
"displayName"]=
191 json_call_return[
"sourceLocation"]=json_location;
196 if(source_location!=previous_source_location)
202 json_location_only[
"stepType"]=
json_stringt(
"location-only");
204 json_location_only[
"thread"]=
206 json_location_only[
"sourceLocation"]=json_location;
212 previous_source_location=source_location;
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
irep_idt mode
Language mode.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static jsont json_boolean(bool value)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
json_arrayt & make_array()
jsont & push_back(const jsont &json)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void convert(const namespacet &ns, const goto_tracet &goto_trace, jsont &dest)
const irep_idt & display_name() const
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const irep_idt & get_file() const
irep_idt base_name
Base (non-scoped) name.
json_objectt & make_object()
const irep_idt & get_property_id() const
json_objectt json(const source_locationt &location)