cprover
path.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_H
14 
15 #include <iosfwd>
16 #include <list>
17 
18 #include <util/std_expr.h>
19 #include <util/namespace.h>
20 
22 
24 {
25 public:
26  explicit path_nodet(const goto_programt::targett &_loc):
27  loc(_loc),
28  guard(nil_exprt())
29  {
30  }
31 
33  const exprt &_guard) :
34  loc(_loc),
35  guard(_guard)
36  {
37  }
38 
39  void output(const goto_programt &program, std::ostream &str) const;
40 
42  const exprt guard;
43 };
44 
45 typedef std::list<path_nodet> patht;
46 typedef std::list<patht> pathst;
47 
48 void output_path(
49  const patht &path,
50  const goto_programt &program,
51  const namespacet &ns,
52  std::ostream &str);
53 
54 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_PATH_H
pathst
std::list< patht > pathst
Definition: path.h:46
path_nodet::path_nodet
path_nodet(const goto_programt::targett &_loc, const exprt &_guard)
Definition: path.h:32
exprt
Base class for all expressions.
Definition: expr.h:53
path_nodet::path_nodet
path_nodet(const goto_programt::targett &_loc)
Definition: path.h:26
path_nodet
Definition: path.h:24
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
output_path
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
Definition: path.cpp:18
goto_program.h
Concrete Goto Program.
patht
std::list< path_nodet > patht
Definition: path.h:45
path_nodet::output
void output(const goto_programt &program, std::ostream &str) const
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
path_nodet::loc
goto_programt::targett loc
Definition: path.h:41
std_expr.h
API to expression classes.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
path_nodet::guard
const exprt guard
Definition: path.h:42