cprover
show_goto_functions_json.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Program
4 
5 Author: Thomas Kiley
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <iostream>
15 #include <sstream>
16 
17 #include <util/json_expr.h>
18 #include <util/json_irep.h>
19 #include <util/cprover_prefix.h>
20 #include <util/prefix.h>
21 
22 #include <langapi/language_util.h>
23 
24 #include "goto_functions.h"
25 #include "goto_model.h"
26 
30  ns(ns)
31 {}
32 
38 {
39  json_arrayt json_functions;
40  const json_irept no_comments_irep_converter(false);
41  for(const auto &function_entry : goto_functions.function_map)
42  {
43  const irep_idt &function_name=function_entry.first;
44  const goto_functionst::goto_functiont &function=function_entry.second;
45 
46  json_objectt &json_function=
47  json_functions.push_back(jsont()).make_object();
48  json_function["name"]=json_stringt(id2string(function_name));
49  json_function["isBodyAvailable"]=
50  jsont::json_boolean(function.body_available());
51  bool is_internal=(has_prefix(id2string(function_name), CPROVER_PREFIX) ||
52  function_name==goto_functions.entry_point());
53  json_function["isInternal"]=jsont::json_boolean(is_internal);
54 
55  if(function.body_available())
56  {
57  json_arrayt json_instruction_array=json_arrayt();
58 
59  for(const goto_programt::instructiont &instruction :
60  function.body.instructions)
61  {
62  json_objectt instruction_entry=json_objectt();
63 
64  instruction_entry["instructionId"]=
65  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  function.body.output_instruction(
75  ns, function_name, instruction_builder, instruction);
76 
77  instruction_entry["instruction"]=
78  json_stringt(instruction_builder.str());
79 
80  if(!instruction.code.operands().empty())
81  {
82  json_arrayt operand_array;
83  for(const exprt &operand : instruction.code.operands())
84  {
85  json_objectt operand_object;
86  no_comments_irep_converter.convert_from_irep(
87  operand, operand_object);
88  operand_array.push_back(operand_object);
89  }
90  instruction_entry["operands"]=operand_array;
91  }
92 
93  if(!instruction.guard.is_true())
94  {
95  json_objectt guard_object;
96  no_comments_irep_converter.convert_from_irep(
97  instruction.guard,
98  guard_object);
99 
100  instruction_entry["guard"]=guard_object;
101  }
102 
103  json_instruction_array.push_back(instruction_entry);
104  }
105 
106  json_function["instructions"]=json_instruction_array;
107  }
108  }
109  json_objectt json_result;
110  json_result["functions"]=json_functions;
111  return json_result;
112 }
113 
123  std::ostream &out,
124  bool append)
125 {
126  if(append)
127  {
128  out << ",\n";
129  }
130  out << convert(goto_functions);
131 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert_from_irep(const irept &irep, jsont &json) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees...
Definition: json_irep.cpp:31
#define CPROVER_PREFIX
Goto Programs with Functions.
Definition: json.h:21
static jsont json_boolean(bool value)
Definition: json.h:83
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...
jsont & push_back(const jsont &json)
Definition: json.h:157
Symbol Table + CFG.
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...
Expressions in JSON.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
show_goto_functions_jsont(const namespacet &ns)
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
Base class for all expressions.
Definition: expr.h:46
json_objectt & make_object()
Definition: json.h:234
operandst & operands()
Definition: expr.h:70
goto_functionst goto_functions
Definition: goto_model.h:26
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23