47 ?
id2string(step.
pc->source_location.get_function()) +
".unwind." +
59 json_failure[
"sourceLocation"] = location;
77 const jsont &json_location = conversion_dependencies.
location;
83 lhs_object.has_value()?lhs_object->get_identifier():
irep_idt();
85 json_assignment[
"stepType"] =
json_stringt(
"assignment");
88 json_assignment[
"sourceLocation"] = json_location;
90 std::string value_string, type_string, full_lhs_string;
105 explicit comment_base_name_visitort(
const namespacet &ns) : ns(ns)
111 if(expr.
id() == ID_symbol)
118 "base_name comment does not match symbol's base_name");
124 comment_base_name_visitort comment_base_name_visitor(ns);
125 simplified.visit(comment_base_name_visitor);
128 full_lhs_string =
from_expr(ns, identifier, simplified);
133 if(!ns.
lookup(identifier, symbol))
137 if(type_string ==
"")
143 full_lhs_value =
json(simplified, ns, symbol->
mode);
149 "full_lhs_value in assignment must not be nil");
153 json_assignment[
"value"] = full_lhs_value;
199 mode = function_name->
mode;
203 for(
const auto &arg : step.
io_args)
210 json_output[
"sourceLocation"] = location;
242 mode = function_name->
mode;
246 for(
const auto &arg : step.
io_args)
253 json_input[
"sourceLocation"] = location;
280 const irep_idt &function_identifier =
286 json_function[
"displayName"] =
json_stringt(symbol.display_name());
287 json_function[
"identifier"] =
json_stringt(function_identifier);
288 json_function[
"sourceLocation"] =
json(symbol.location);
291 json_call_return[
"sourceLocation"] = location;
309 json_location_only[
"stepType"] =
json_stringt(
"location-only");
312 json_location_only[
"sourceLocation"] = location;
const std::string & id2string(const irep_idt &d)
exprt simplify_expr(const exprt &src, const namespacet &ns)
irep_idt mode
Language mode.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const irep_idt & get_function() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static jsont json_boolean(bool value)
goto_programt::const_targett pc
json_arrayt & make_array()
jsont & push_back(const jsont &json)
const irep_idt & id() const
const source_locationt & source_location
This is structure is here to facilitate passing arguments to the conversion functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
optionalt< symbol_exprt > get_lhs_object() const
Base class for tree-like data structures with sharing.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const goto_trace_stept & step
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const irep_idt & display_name() const
Return language specific display name if present.
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees...
typet type
Type of symbol.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
virtual void operator()(exprt &)
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_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.
irept & add(const irep_namet &name)
json_objectt & make_object()
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
const irep_idt & get_property_id() const
const irept & find(const irep_namet &name) const
json_objectt json(const source_locationt &location)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
assignment_typet assignment_type