cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
12
#include "
show_goto_functions_xml.h
"
13
14
#include <
util/cprover_prefix.h
>
15
#include <
util/xml_irep.h
>
16
17
#include "
goto_functions.h
"
18
21
show_goto_functions_xmlt::show_goto_functions_xmlt
(
bool
_list_only)
22
:
list_only
(_list_only)
23
{}
24
34
xmlt
show_goto_functions_xmlt::convert
(
35
const
goto_functionst
&goto_functions)
36
{
37
xmlt
xml_functions=
xmlt
(
"functions"
);
38
39
const
auto
sorted = goto_functions.
sorted
();
40
41
for
(
const
auto
&function_entry : sorted)
42
{
43
const
irep_idt
&function_name = function_entry->first;
44
const
goto_functionst::goto_functiont
&function = function_entry->second;
45
46
xmlt
&xml_function=xml_functions.
new_element
(
"function"
);
47
xml_function.
set_attribute
(
"name"
,
id2string
(function_name));
48
xml_function.
set_attribute_bool
(
49
"is_body_available"
, function.body_available());
50
bool
is_internal = function_name.
starts_with
(
CPROVER_PREFIX
) ||
51
function_name.
starts_with
(
"java::array["
) ||
52
function_name.
starts_with
(
"java::org.cprover"
) ||
53
function_name.
starts_with
(
"java::java"
);
54
xml_function.
set_attribute_bool
(
"is_internal"
, is_internal);
55
56
if
(
list_only
)
57
continue
;
58
59
if
(function.body_available())
60
{
61
xmlt
&xml_instructions=xml_function.
new_element
(
"instructions"
);
62
for
(
const
goto_programt::instructiont
&instruction :
63
function.body.instructions)
64
{
65
xmlt
&instruction_entry=xml_instructions.
new_element
(
"instruction"
);
66
67
instruction_entry.
set_attribute
(
68
"instruction_id"
, instruction.
to_string
());
69
70
if
(instruction.
code
().
source_location
().
is_not_nil
())
71
{
72
instruction_entry.
new_element
(
73
xml
(instruction.
code
().
source_location
()));
74
}
75
76
std::ostringstream instruction_builder;
77
instruction.
output
(instruction_builder);
78
79
xmlt
&instruction_value=
80
instruction_entry.
new_element
(
"instruction_value"
);
81
instruction_value.
data
=instruction_builder.str();
82
instruction_value.
elements
.clear();
83
}
84
}
85
}
86
return
xml_functions;
87
}
88
96
void
show_goto_functions_xmlt::operator()
(
97
const
goto_functionst
&goto_functions,
98
std::ostream &out,
99
bool
append)
100
{
101
if
(append)
102
{
103
out <<
"\n"
;
104
}
105
out <<
convert
(goto_functions);
106
}
dstringt::starts_with
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition
dstring.h:95
exprt::source_location
const source_locationt & source_location() const
Definition
expr.h:236
goto_functionst
A collection of goto functions.
Definition
goto_functions.h:25
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition
goto_functions.h:27
goto_functionst::sorted
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition
goto_functions.cpp:66
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition
goto_program.h:180
goto_programt::instructiont::code
const goto_instruction_codet & code() const
Get the code represented by this instruction.
Definition
goto_program.h:187
goto_programt::instructiont::to_string
std::string to_string() const
Definition
goto_program.h:580
goto_programt::instructiont::output
std::ostream & output(std::ostream &) const
Output this instruction to the given stream.
Definition
goto_program.cpp:49
irept::is_not_nil
bool is_not_nil() const
Definition
irep.h:372
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:34
show_goto_functions_xmlt::show_goto_functions_xmlt
show_goto_functions_xmlt(bool _list_only=false)
For outputting the GOTO program in a readable xml format.
Definition
show_goto_functions_xml.cpp: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:96
show_goto_functions_xmlt::list_only
bool list_only
Definition
show_goto_functions_xml.h:30
xmlt
Definition
xml.h:21
xmlt::set_attribute_bool
void set_attribute_bool(const std::string &attribute, bool value)
Definition
xml.h:72
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition
xml.h:95
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition
xml.cpp:198
xmlt::elements
elementst elements
Definition
xml.h:42
xmlt::data
std::string data
Definition
xml.h:39
cprover_prefix.h
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition
cprover_prefix.h:14
goto_functions.h
Goto Programs with Functions.
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:110
show_goto_functions_xml.h
Goto Program.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
xml_irep.h
goto-programs
show_goto_functions_xml.cpp
Generated by
1.17.0