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 }
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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.
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:63
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.cpp:24
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void output_dot(std::ostream &out) const
Definition: graph.h:961
The basic interface of an abstract interpreter.
Definition: ai.h:32
Options.
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:119