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 
23  const goto_modelt &goto_model,
24  const ai_baset &ai,
25  const optionst &options,
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 }
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
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.
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
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void output_dot(std::ostream &out) const
Definition: graph.h:784
Definition: ai.h:128
Options.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
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