CBMC
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 <util/cprover_prefix.h>
15 #include <util/xml_irep.h>
16 
17 #include "goto_functions.h"
18 
19 #include <iostream>
20 
24  : list_only(_list_only)
25 {}
26 
37  const goto_functionst &goto_functions)
38 {
39  xmlt xml_functions=xmlt("functions");
40 
41  const auto sorted = goto_functions.sorted();
42 
43  for(const auto &function_entry : sorted)
44  {
45  const irep_idt &function_name = function_entry->first;
46  const goto_functionst::goto_functiont &function = function_entry->second;
47 
48  xmlt &xml_function=xml_functions.new_element("function");
49  xml_function.set_attribute("name", id2string(function_name));
50  xml_function.set_attribute_bool(
51  "is_body_available", function.body_available());
52  bool is_internal = function_name.starts_with(CPROVER_PREFIX) ||
53  function_name.starts_with("java::array[") ||
54  function_name.starts_with("java::org.cprover") ||
55  function_name.starts_with("java::java");
56  xml_function.set_attribute_bool("is_internal", is_internal);
57 
58  if(list_only)
59  continue;
60 
61  if(function.body_available())
62  {
63  xmlt &xml_instructions=xml_function.new_element("instructions");
64  for(const goto_programt::instructiont &instruction :
65  function.body.instructions)
66  {
67  xmlt &instruction_entry=xml_instructions.new_element("instruction");
68 
69  instruction_entry.set_attribute(
70  "instruction_id", instruction.to_string());
71 
72  if(instruction.code().source_location().is_not_nil())
73  {
74  instruction_entry.new_element(
75  xml(instruction.code().source_location()));
76  }
77 
78  std::ostringstream instruction_builder;
79  instruction.output(instruction_builder);
80 
81  xmlt &instruction_value=
82  instruction_entry.new_element("instruction_value");
83  instruction_value.data=instruction_builder.str();
84  instruction_value.elements.clear();
85  }
86  }
87  }
88  return xml_functions;
89 }
90 
99  const goto_functionst &goto_functions,
100  std::ostream &out,
101  bool append)
102 {
103  if(append)
104  {
105  out << "\n";
106  }
107  out << convert(goto_functions);
108 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
const source_locationt & source_location() const
Definition: expr.h:231
A collection of goto functions.
::goto_functiont goto_functiont
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition: goto_program.h:188
std::string to_string() const
Definition: goto_program.h:581
std::ostream & output(std::ostream &) const
Output this instruction to the given stream.
bool is_not_nil() const
Definition: irep.h:368
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...
show_goto_functions_xmlt(bool _list_only=false)
For outputting the GOTO program in a readable xml format.
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: xml.h:21
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:72
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
xmlt & new_element(const std::string &key)
Definition: xml.h:95
elementst elements
Definition: xml.h:42
std::string data
Definition: xml.h:39
#define CPROVER_PREFIX
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110