cprover
Loading...
Searching...
No Matches
show_goto_functions_json.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Program
4
5Author: Thomas Kiley
6
7\*******************************************************************/
8
11
13
14#include <util/cprover_prefix.h>
15#include <util/json_irep.h>
16
17#include "goto_functions.h"
18
19#include <iostream>
20
26
31 const goto_functionst &goto_functions)
32{
33 json_arrayt json_functions;
34 const json_irept no_comments_irep_converter(false);
35
36 const auto sorted = goto_functions.sorted();
37
38 for(const auto &function_entry : sorted)
39 {
40 const irep_idt &function_name = function_entry->first;
41 const goto_functionst::goto_functiont &function = function_entry->second;
42
43 json_objectt &json_function=
44 json_functions.push_back(jsont()).make_object();
45 json_function["name"] = json_stringt(function_name);
46 json_function["isBodyAvailable"]=
47 jsont::json_boolean(function.body_available());
48 bool is_internal = function_name.starts_with(CPROVER_PREFIX) ||
49 function_name.starts_with("java::array[") ||
50 function_name.starts_with("java::org.cprover") ||
51 function_name.starts_with("java::java");
52 json_function["isInternal"]=jsont::json_boolean(is_internal);
53
54 if(list_only)
55 continue;
56
57 if(function.body_available())
58 {
59 json_arrayt json_instruction_array=json_arrayt();
60
61 for(const goto_programt::instructiont &instruction :
62 function.body.instructions)
63 {
64 json_objectt instruction_entry{
65 {"instructionId", json_stringt(instruction.to_string())}};
66
67 if(instruction.code().source_location().is_not_nil())
68 {
69 instruction_entry["sourceLocation"] =
70 json(instruction.code().source_location());
71 }
72
73 std::ostringstream instruction_builder;
74 instruction.output(instruction_builder);
75
76 instruction_entry["instruction"]=
77 json_stringt(instruction_builder.str());
78
79 if(!instruction.code().operands().empty())
80 {
81 json_arrayt operand_array;
82 for(const exprt &operand : instruction.code().operands())
83 {
84 json_objectt operand_object=
85 no_comments_irep_converter.convert_from_irep(
86 operand);
87 operand_array.push_back(operand_object);
88 }
89 instruction_entry["operands"] = std::move(operand_array);
90 }
91
92 if(instruction.has_condition())
93 {
94 json_objectt guard_object =
95 no_comments_irep_converter.convert_from_irep(
96 instruction.condition());
97
98 instruction_entry["guard"] = std::move(guard_object);
99 }
100
101 json_instruction_array.push_back(std::move(instruction_entry));
102 }
103
104 json_function["instructions"] = std::move(json_instruction_array);
105 }
106 }
107
108 return json_objectt({{"functions", json_functions}});
109}
110
119 const goto_functionst &goto_functions,
120 std::ostream &out,
121 bool append)
122{
123 if(append)
124 {
125 out << ",\n";
126 }
127 out << convert(goto_functions);
128}
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
A collection of goto functions.
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
::goto_functiont goto_functiont
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
std::string to_string() const
std::ostream & output(std::ostream &) const
Output this instruction to the given stream.
const exprt & condition() const
Get the condition of gotos, assume, assert.
bool is_not_nil() const
Definition irep.h:372
jsont & push_back(const jsont &json)
Definition json.h:212
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.
Definition json_irep.cpp:31
Definition json.h:27
json_objectt & make_object()
Definition json.h:436
static jsont json_boolean(bool value)
Definition json.h:97
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.
#define CPROVER_PREFIX
Goto Programs with Functions.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
dstringt irep_idt