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/cprover_prefix.h>
18 #include <util/prefix.h>
19 #include <util/xml_irep.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 
45  const goto_functionst &goto_functions)
46 {
47  xmlt xml_functions=xmlt("functions");
48 
49  const auto sorted = goto_functions.sorted();
50 
51  for(const auto &function_entry : sorted)
52  {
53  const irep_idt &function_name = function_entry->first;
54  const goto_functionst::goto_functiont &function = function_entry->second;
55 
56  xmlt &xml_function=xml_functions.new_element("function");
57  xml_function.set_attribute("name", id2string(function_name));
58  xml_function.set_attribute_bool(
59  "is_body_available", function.body_available());
60  bool is_internal=
61  has_prefix(id2string(function_name), CPROVER_PREFIX) ||
62  has_prefix(id2string(function_name), "java::array[") ||
63  has_prefix(id2string(function_name), "java::org.cprover") ||
64  has_prefix(id2string(function_name), "java::java");
65  xml_function.set_attribute_bool("is_internal", is_internal);
66 
67  if(list_only)
68  continue;
69 
70  if(function.body_available())
71  {
72  xmlt &xml_instructions=xml_function.new_element("instructions");
73  for(const goto_programt::instructiont &instruction :
74  function.body.instructions)
75  {
76  xmlt &instruction_entry=xml_instructions.new_element("instruction");
77 
78  instruction_entry.set_attribute(
79  "instruction_id", instruction.to_string());
80 
81  if(instruction.code.source_location().is_not_nil())
82  {
83  instruction_entry.new_element(
84  xml(instruction.code.source_location()));
85  }
86 
87  std::ostringstream instruction_builder;
88  function.body.output_instruction(
89  ns, function_name, instruction_builder, instruction);
90 
91  xmlt &instruction_value=
92  instruction_entry.new_element("instruction_value");
93  instruction_value.data=instruction_builder.str();
94  instruction_value.elements.clear();
95  }
96  }
97  }
98  return xml_functions;
99 }
100 
109  const goto_functionst &goto_functions,
110  std::ostream &out,
111  bool append)
112 {
113  if(append)
114  {
115  out << "\n";
116  }
117  out << convert(goto_functions);
118 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
xmlt::elements
elementst elements
Definition: xml.h:42
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:549
prefix.h
goto_model.h
Symbol Table + CFG.
xml_irep.h
show_goto_functions_xmlt::convert
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...
Definition: show_goto_functions_xml.cpp:44
show_goto_functions_xmlt::ns
const namespacet & ns
Definition: show_goto_functions_xml.h:32
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
show_goto_functions_xml.h
Goto Program.
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
show_goto_functions_xmlt::show_goto_functions_xmlt
show_goto_functions_xmlt(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable xml format.
Definition: show_goto_functions_xml.cpp:29
language_util.h
show_goto_functions_xmlt::list_only
bool list_only
Definition: show_goto_functions_xml.h:33
cprover_prefix.h
xmlt
Definition: xml.h:21
show_goto_functions_xmlt::operator()
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...
Definition: show_goto_functions_xml.cpp:108
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
xmlt::set_attribute_bool
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:72
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functions.h
Goto Programs with Functions.
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
xmlt::data
std::string data
Definition: xml.h:39
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:179
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition: goto_functions.cpp:62
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95