37 const auto sorted = goto_functions.
sorted();
59 if(function.body_available())
64 function.body.instructions)
67 {
"instructionId",
json_stringt(instruction.to_string())}};
69 if(instruction.code().source_location().is_not_nil())
72 json(instruction.code().source_location());
81 if(!instruction.code().operands().empty())
84 for(
const exprt &
operand : instruction.code().operands())
94 if(instruction.has_condition())
98 instruction.condition());
129 out <<
convert(goto_functions);
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
::goto_functiont goto_functiont
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
This class represents an instruction in the GOTO intermediate representation.
static jsont json_boolean(bool value)
void operator()(const goto_functionst &goto_functions, std::ostream &out, bool append=true)
Print the json object generated by show_goto_functions_jsont::show_goto_functions to the provided str...
json_objectt convert(const goto_functionst &goto_functions)
Walks through all of the functions in the program and returns a JSON object representing all their fu...
show_goto_functions_jsont(bool _list_only=false)
For outputting the GOTO program in a readable JSON format.
bool has_prefix(const std::string &s, const std::string &prefix)
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)