cprover
static_show_domain.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: goto-analyzer
4
5
Author: Martin Brain, martin.brain@cs.ox.ac.uk
6
7
\*******************************************************************/
8
9
#include "
static_show_domain.h
"
10
11
#include <
util/options.h
>
12
13
#include <
analyses/dependence_graph.h
>
14
22
bool
static_show_domain
(
23
const
goto_modelt
&goto_model,
24
const
ai_baset
&ai,
25
const
optionst
&options,
26
message_handlert
&
message_handler
,
27
std::ostream &out)
28
{
29
if
(options.
get_bool_option
(
"json"
))
30
{
31
out << ai.
output_json
(goto_model);
32
}
33
else
if
(options.
get_bool_option
(
"xml"
))
34
{
35
out << ai.
output_xml
(goto_model);
36
}
37
else
if
(options.
get_bool_option
(
"dot"
) &&
38
options.
get_bool_option
(
"dependence-graph"
))
39
{
40
const
dependence_grapht
*d=
dynamic_cast<
const
dependence_grapht
*
>
(&ai);
41
INVARIANT
(d!=
nullptr
,
42
"--dependence-graph sets ai to be a dependence_graph"
);
43
44
out <<
"digraph g {\n"
;
45
d->
output_dot
(out);
46
out <<
"}\n"
;
47
}
48
else
49
{
50
INVARIANT
(options.
get_bool_option
(
"text"
),
"Other output formats handled"
);
51
ai.
output
(goto_model, out);
52
}
53
54
return
false
;
55
}
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static_show_domain
bool static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition:
static_show_domain.cpp:22
ai_baset::output_json
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as JSON.
Definition:
ai.cpp:134
optionst
Definition:
options.h:19
INVARIANT
#define INVARIANT(CONDITION, REASON)
Definition:
invariant.h:205
goto_modelt
Definition:
goto_model.h:24
ai_baset::output
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition:
ai.cpp:92
static_show_domain.h
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition:
options.cpp:42
message_handlert
Definition:
message.h:25
grapht::output_dot
void output_dot(std::ostream &out) const
Definition:
graph.h:784
ai_baset
Definition:
ai.h:128
options.h
Options.
dependence_grapht
Definition:
dependence_graph.h:215
message_handler
goto_programt coverage_criteriont message_handlert & message_handler
Definition:
cover.cpp:66
ai_baset::output_xml
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as XML.
Definition:
ai.cpp:189
goto-analyzer
static_show_domain.cpp
Generated by
1.8.14