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 
14 
21  const goto_modelt &goto_model,
22  const ai_baset &ai,
23  const optionst &options,
24  std::ostream &out)
25 {
26  if(options.get_bool_option("json"))
27  {
28  out << ai.output_json(goto_model);
29  }
30  else if(options.get_bool_option("xml"))
31  {
32  out << ai.output_xml(goto_model);
33  }
34  else if(options.get_bool_option("dot") &&
35  options.get_bool_option("dependence-graph"))
36  {
37  const dependence_grapht *d=dynamic_cast<const dependence_grapht*>(&ai);
38  INVARIANT(d!=nullptr,
39  "--dependence-graph sets ai to be a dependence_graph");
40 
41  out << "digraph g {\n";
42  d->output_dot(out);
43  out << "}\n";
44  }
45  else
46  {
47  // 'text' or console output
48  ai.output(goto_model, out);
49  }
50 }
ai_baset::output_json
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
Definition: ai.cpp:62
dependence_grapht
Definition: dependence_graph.h:217
optionst
Definition: options.h:23
ai_baset::output_xml
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Definition: ai.cpp:109
goto_modelt
Definition: goto_model.h:26
options.h
Options.
static_show_domain
void 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:20
ai_baset::output
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition: ai.cpp:42
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
grapht::output_dot
void output_dot(std::ostream &out) const
Definition: graph.h:963
static_show_domain.h
validation_modet::INVARIANT
@ INVARIANT
dependence_graph.h
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.