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 <iostream>
15
16#include <util/json_irep.h>
17#include <util/cprover_prefix.h>
18#include <util/prefix.h>
19
20#include "goto_functions.h"
21
25 : list_only(_list_only)
26{}
27
32 const goto_functionst &goto_functions)
33{
34 json_arrayt json_functions;
35 const json_irept no_comments_irep_converter(false);
36
37 const auto sorted = goto_functions.sorted();
38
39 for(const auto &function_entry : sorted)
40 {
41 const irep_idt &function_name = function_entry->first;
42 const goto_functionst::goto_functiont &function = function_entry->second;
43
44 json_objectt &json_function=
45 json_functions.push_back(jsont()).make_object();
46 json_function["name"] = json_stringt(function_name);
47 json_function["isBodyAvailable"]=
48 jsont::json_boolean(function.body_available());
49 bool is_internal=
50 has_prefix(id2string(function_name), CPROVER_PREFIX) ||
51 has_prefix(id2string(function_name), "java::array[") ||
52 has_prefix(id2string(function_name), "java::org.cprover") ||
53 has_prefix(id2string(function_name), "java::java");
54 json_function["isInternal"]=jsont::json_boolean(is_internal);
55
56 if(list_only)
57 continue;
58
59 if(function.body_available())
60 {
61 json_arrayt json_instruction_array=json_arrayt();
62
63 for(const goto_programt::instructiont &instruction :
64 function.body.instructions)
65 {
66 json_objectt instruction_entry{
67 {"instructionId", json_stringt(instruction.to_string())}};
68
69 if(instruction.code().source_location().is_not_nil())
70 {
71 instruction_entry["sourceLocation"] =
72 json(instruction.code().source_location());
73 }
74
75 std::ostringstream instruction_builder;
76 instruction.output(instruction_builder);
77
78 instruction_entry["instruction"]=
79 json_stringt(instruction_builder.str());
80
81 if(!instruction.code().operands().empty())
82 {
83 json_arrayt operand_array;
84 for(const exprt &operand : instruction.code().operands())
85 {
86 json_objectt operand_object=
87 no_comments_irep_converter.convert_from_irep(
88 operand);
89 operand_array.push_back(operand_object);
90 }
91 instruction_entry["operands"] = std::move(operand_array);
92 }
93
94 if(instruction.has_condition())
95 {
96 json_objectt guard_object =
97 no_comments_irep_converter.convert_from_irep(
98 instruction.condition());
99
100 instruction_entry["guard"] = std::move(guard_object);
101 }
102
103 json_instruction_array.push_back(std::move(instruction_entry));
104 }
105
106 json_function["instructions"] = std::move(json_instruction_array);
107 }
108 }
109
110 return json_objectt({{"functions", json_functions}});
111}
112
121 const goto_functionst &goto_functions,
122 std::ostream &out,
123 bool append)
124{
125 if(append)
126 {
127 out << ",\n";
128 }
129 out << convert(goto_functions);
130}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
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.
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
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.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)