cprover
show_goto_functions_xml.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/cprover_prefix.h>
17#include <util/prefix.h>
18#include <util/xml_irep.h>
19
20#include "goto_functions.h"
21
26 const namespacet &_ns,
27 bool _list_only)
28 : ns(_ns), list_only(_list_only)
29{}
30
41 const goto_functionst &goto_functions)
42{
43 xmlt xml_functions=xmlt("functions");
44
45 const auto sorted = goto_functions.sorted();
46
47 for(const auto &function_entry : sorted)
48 {
49 const irep_idt &function_name = function_entry->first;
50 const goto_functionst::goto_functiont &function = function_entry->second;
51
52 xmlt &xml_function=xml_functions.new_element("function");
53 xml_function.set_attribute("name", id2string(function_name));
54 xml_function.set_attribute_bool(
55 "is_body_available", function.body_available());
56 bool is_internal=
57 has_prefix(id2string(function_name), CPROVER_PREFIX) ||
58 has_prefix(id2string(function_name), "java::array[") ||
59 has_prefix(id2string(function_name), "java::org.cprover") ||
60 has_prefix(id2string(function_name), "java::java");
61 xml_function.set_attribute_bool("is_internal", is_internal);
62
63 if(list_only)
64 continue;
65
66 if(function.body_available())
67 {
68 xmlt &xml_instructions=xml_function.new_element("instructions");
69 for(const goto_programt::instructiont &instruction :
70 function.body.instructions)
71 {
72 xmlt &instruction_entry=xml_instructions.new_element("instruction");
73
74 instruction_entry.set_attribute(
75 "instruction_id", instruction.to_string());
76
77 if(instruction.get_code().source_location().is_not_nil())
78 {
79 instruction_entry.new_element(
80 xml(instruction.get_code().source_location()));
81 }
82
83 std::ostringstream instruction_builder;
84 function.body.output_instruction(
85 ns, function_name, instruction_builder, instruction);
86
87 xmlt &instruction_value=
88 instruction_entry.new_element("instruction_value");
89 instruction_value.data=instruction_builder.str();
90 instruction_value.elements.clear();
91 }
92 }
93 }
94 return xml_functions;
95}
96
105 const goto_functionst &goto_functions,
106 std::ostream &out,
107 bool append)
108{
109 if(append)
110 {
111 out << "\n";
112 }
113 out << convert(goto_functions);
114}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const source_locationt & source_location() const
Definition: expr.h:230
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:180
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
std::string to_string() const
Definition: goto_program.h:562
bool is_not_nil() const
Definition: irep.h:380
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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...
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...
show_goto_functions_xmlt(const namespacet &_ns, bool _list_only=false)
For outputting the GOTO program in a readable xml format.
Definition: xml.h:21
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:72
xmlt & new_element(const std::string &key)
Definition: xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
elementst elements
Definition: xml.h:42
std::string data
Definition: xml.h:39
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
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108