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
21
bool
static_show_domain
(
22
const
goto_modelt
&goto_model,
23
const
ai_baset
&ai,
24
const
optionst
&options,
25
std::ostream &out)
26
{
27
if
(options.
get_bool_option
(
"json"
))
28
{
29
out << ai.
output_json
(goto_model);
30
}
31
else
if
(options.
get_bool_option
(
"xml"
))
32
{
33
out << ai.
output_xml
(goto_model);
34
}
35
else
if
(options.
get_bool_option
(
"dot"
) &&
36
options.
get_bool_option
(
"dependence-graph"
))
37
{
38
const
dependence_grapht
*d=
dynamic_cast<
const
dependence_grapht
*
>
(&ai);
39
INVARIANT
(d!=
nullptr
,
40
"--dependence-graph sets ai to be a dependence_graph"
);
41
42
out <<
"digraph g {\n"
;
43
d->
output_dot
(out);
44
out <<
"}\n"
;
45
}
46
else
47
{
48
INVARIANT
(options.
get_bool_option
(
"text"
),
"Other output formats handled"
);
49
ai.
output
(goto_model, out);
50
}
51
52
return
false
;
53
}
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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:66
optionst
Definition:
options.h:19
INVARIANT
#define INVARIANT(CONDITION, REASON)
Definition:
invariant.h:204
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:24
static_show_domain.h
static_show_domain
bool static_show_domain(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, std::ostream &out)
Runs the analyzer and then prints out the domain.
Definition:
static_show_domain.cpp:21
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition:
options.cpp:42
grapht::output_dot
void output_dot(std::ostream &out) const
Definition:
graph.h:914
ai_baset
The basic interface of an abstract interpreter.
Definition:
ai.h:32
options.h
Options.
dependence_grapht
Definition:
dependence_graph.h:215
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:122
goto-analyzer
static_show_domain.cpp
Generated by
1.8.14