cprover
show_goto_functions_xml.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/xml_expr.h>
18 #include <util/cprover_prefix.h>
19 #include <util/prefix.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "goto_functions.h"
24 #include "goto_model.h"
25 
30  const namespacet &_ns,
31  bool _list_only)
32  : ns(_ns), list_only(_list_only)
33 {}
34 
43  const goto_functionst &goto_functions)
44 {
45  xmlt xml_functions=xmlt("functions");
46  for(const auto &function_entry : goto_functions.function_map)
47  {
48  const irep_idt &function_name=function_entry.first;
49  const goto_functionst::goto_functiont &function=function_entry.second;
50 
51  xmlt &xml_function=xml_functions.new_element("function");
52  xml_function.set_attribute("name", id2string(function_name));
53  xml_function.set_attribute_bool(
54  "is_body_available", function.body_available());
55  bool is_internal=
56  has_prefix(id2string(function_name), CPROVER_PREFIX) ||
57  has_prefix(id2string(function_name), "java::array[") ||
58  has_prefix(id2string(function_name), "java::org.cprover") ||
59  has_prefix(id2string(function_name), "java::java");
60  xml_function.set_attribute_bool("is_internal", is_internal);
61 
62  if(list_only)
63  continue;
64 
65  if(function.body_available())
66  {
67  xmlt &xml_instructions=xml_function.new_element("instructions");
68  for(const goto_programt::instructiont &instruction :
69  function.body.instructions)
70  {
71  xmlt &instruction_entry=xml_instructions.new_element("instruction");
72 
73  instruction_entry.set_attribute(
74  "instruction_id", instruction.to_string());
75 
76  if(instruction.code.source_location().is_not_nil())
77  {
78  instruction_entry.new_element(
79  xml(instruction.code.source_location()));
80  }
81 
82  std::ostringstream instruction_builder;
83  function.body.output_instruction(
84  ns, function_name, instruction_builder, instruction);
85 
86  xmlt &instruction_value=
87  instruction_entry.new_element("instruction_value");
88  instruction_value.data=instruction_builder.str();
89  instruction_value.elements.clear();
90  }
91  }
92  }
93  return xml_functions;
94 }
95 
104  const goto_functionst &goto_functions,
105  std::ostream &out,
106  bool append)
107 {
108  if(append)
109  {
110  out << "\n";
111  }
112  out << convert(goto_functions);
113 }
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:63
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
std::string to_string() const
Definition: goto_program.h:386
#define CPROVER_PREFIX
void operator()(const goto_functionst &goto_functions, std::ostream &out, bool append=true)
Print the xml object generated by show_goto_functions_xmlt::show_goto_functions to the provided strea...
Goto Programs with Functions.
function_mapt function_map
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
elementst elements
Definition: xml.h:33
Symbol Table + CFG.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
Definition: xml.h:18
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
std::string data
Definition: xml.h:30
xmlt & new_element(const std::string &name)
Definition: xml.h:86
show_goto_functions_xmlt(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable xml format.
const source_locationt & source_location() const
Definition: expr.h:125
xmlt convert(const goto_functionst &goto_functions)
Walks through all of the functions in the program and returns an xml object representing all their fu...