cprover
locs.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: CFG made of Program Locations, built from goto_functionst
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_LOCS_H
13 #define CPROVER_PATH_SYMEX_LOCS_H
14 
15 #include <util/std_expr.h>
16 
18 
19 #include "loc_ref.h"
20 
21 struct loct
22 {
23 public:
26  const irep_idt &_function):
27  target(_target),
28  function(_function)
29  {
30  }
31 
33  irep_idt function;
34 
35  // we only support a single branch target
37 };
38 
39 class locst
40 {
41 public:
42  typedef std::vector<loct> loc_vectort;
45 
47  {
48  public:
51  };
52 
53  typedef std::map<irep_idt, function_entryt> function_mapt;
55 
56  explicit locst(const namespacet &_ns);
57  void build(const goto_functionst &goto_functions);
58  void output(std::ostream &out) const;
59 
61  {
62  assert(l.loc_number<loc_vector.size());
63  return loc_vector[l.loc_number];
64  }
65 
66  const loct &operator[] (loc_reft l) const
67  {
68  assert(l.loc_number<loc_vector.size());
69  return loc_vector[l.loc_number];
70  }
71 
72  static inline loc_reft begin()
73  {
74  loc_reft tmp;
75  tmp.loc_number=0;
76  return tmp;
77  }
78 
79  loc_reft end() const
80  {
81  loc_reft tmp;
82  tmp.loc_number=loc_vector.size();
83  return tmp;
84  }
85 
86  std::size_t size() const
87  {
88  return loc_vector.size();
89  }
90 
91 protected:
92  const namespacet &ns;
93 };
94 
96 {
97 public:
98  explicit target_to_loc_mapt(const locst &locs)
99  {
100  for(loc_reft it=locs.begin(); it!=locs.end(); ++it)
101  map[locs[it].target]=it;
102  }
103 
105  {
106  mapt::const_iterator it=map.find(t);
107  assert(it!=map.end());
108  return it->second;
109  }
110 
111 protected:
112  typedef std::map<goto_programt::const_targett, loc_reft> mapt;
114 };
115 
116 #endif // CPROVER_PATH_SYMEX_LOCS_H
loc_reft entry_loc
Definition: locs.h:44
code_typet type
Definition: locs.h:50
loc_reft operator[](const goto_programt::const_targett t) const
Definition: locs.h:104
Base type of functions.
Definition: std_types.h:734
unsigned loc_number
Definition: loc_ref.h:20
Goto Programs with Functions.
static loc_reft begin()
Definition: locs.h:72
const namespacet & ns
Definition: locs.h:92
void output(std::ostream &out) const
Definition: locs.cpp:84
loc_reft branch_target
Definition: locs.h:36
locst(const namespacet &_ns)
Definition: locs.cpp:14
instructionst::const_iterator const_targett
std::vector< loct > loc_vectort
Definition: locs.h:42
loct & operator[](loc_reft l)
Definition: locs.h:60
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
loc_vectort loc_vector
Definition: locs.h:43
std::map< irep_idt, function_entryt > function_mapt
Definition: locs.h:53
loct(goto_programt::const_targett _target, const irep_idt &_function)
Definition: locs.h:24
goto_programt::const_targett target
Definition: locs.h:32
irep_idt function
Definition: locs.h:33
std::map< goto_programt::const_targett, loc_reft > mapt
Definition: locs.h:112
Definition: locs.h:39
std::size_t size() const
Definition: locs.h:86
Definition: locs.h:21
function_mapt function_map
Definition: locs.h:54
loc_reft first_loc
Definition: locs.h:49
loc_reft end() const
Definition: locs.h:79
target_to_loc_mapt(const locst &locs)
Definition: locs.h:98
Program Locations.
void build(const goto_functionst &goto_functions)
Definition: locs.cpp:20