47 ?
id2string(step.
pc->source_location.get_function()) +
".unwind." +
59 json_failure[
"sourceLocation"] = location;
77 const jsont &json_location = conversion_dependencies.
location;
82 json_assignment[
"stepType"] =
json_stringt(
"assignment");
85 json_assignment[
"sourceLocation"] = json_location;
87 std::string value_string, type_string, full_lhs_string;
102 explicit comment_base_name_visitort(
const namespacet &ns) : ns(ns)
108 if(expr.
id() == ID_symbol)
115 "base_name comment does not match symbol's base_name");
121 comment_base_name_visitort comment_base_name_visitor(ns);
122 simplified.visit(comment_base_name_visitor);
125 full_lhs_string =
from_expr(ns, identifier, simplified);
130 if(!ns.
lookup(identifier, symbol))
134 if(type_string ==
"")
140 full_lhs_value =
json(simplified, ns, symbol->
mode);
146 "full_lhs_value in assignment must not be nil");
150 json_assignment[
"value"] = full_lhs_value;
196 mode = function_name->
mode;
200 for(
const auto &arg : step.
io_args)
207 json_output[
"sourceLocation"] = location;
239 mode = function_name->
mode;
243 for(
const auto &arg : step.
io_args)
250 json_input[
"sourceLocation"] = location;
281 json_function[
"sourceLocation"] =
json(symbol.
location);
284 json_call_return[
"sourceLocation"] = location;
302 json_location_only[
"stepType"] =
json_stringt(
"location-only");
305 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.
const irep_idt & get_function() const
const irep_idt & get_identifier() const
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...
goto_programt::const_targett pc
json_arrayt & make_array()
#define INVARIANT(CONDITION, REASON)
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.
Base class for tree-like data structures with sharing.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic 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
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.
source_locationt location
Source code location of definition 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.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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)
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 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