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 
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 }
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:24
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.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void output_dot(std::ostream &out) const
Definition: graph.h:914
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 domains for the whole program as XML.
Definition: ai.cpp:122