cprover
loc_ref.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Locations
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_PATH_SYMEX_LOC_REF_H
13 #define CPROVER_PATH_SYMEX_LOC_REF_H
14 
15 #include <ostream>
16 
17 class loc_reft
18 {
19 public:
20  unsigned loc_number;
21 
23  {
24  loc_reft tmp=*this;
25  tmp.increase();
26  return tmp;
27  }
28 
29  void increase()
30  {
31  loc_number++;
32  }
33 
34  void decrease()
35  {
36  loc_number--;
37  }
38 
39  bool is_nil() const
40  {
41  return loc_number==nil().loc_number;
42  }
43 
44  loc_reft():loc_number(-1) // ugly conversion
45  {
46  }
47 
48  static inline loc_reft nil()
49  {
50  return loc_reft();
51  }
52 
53  loc_reft &operator++() // this is pre-increment
54  {
55  increase();
56  return *this;
57  }
58 
59  loc_reft &operator--() // this is pre-decrement
60  {
61  decrease();
62  return *this;
63  }
64 
65  bool operator<(const loc_reft other) const
66  {
67  return loc_number<other.loc_number;
68  }
69 
70  bool operator!=(const loc_reft other) const
71  {
72  return loc_number!=other.loc_number;
73  }
74 
75  bool operator==(const loc_reft other) const
76  {
77  return loc_number==other.loc_number;
78  }
79 };
80 
81 inline std::ostream &operator<<(std::ostream &out, const loc_reft l)
82 {
83  if(l.is_nil())
84  return out << "nil";
85  else
86  return out << l.loc_number;
87 }
88 
89 #endif // CPROVER_PATH_SYMEX_LOC_REF_H
loc_reft()
Definition: loc_ref.h:44
bool operator!=(const loc_reft other) const
Definition: loc_ref.h:70
unsigned loc_number
Definition: loc_ref.h:20
loc_reft & operator--()
Definition: loc_ref.h:59
bool is_nil() const
Definition: loc_ref.h:39
std::ostream & operator<<(std::ostream &out, const loc_reft l)
Definition: loc_ref.h:81
bool operator<(const loc_reft other) const
Definition: loc_ref.h:65
bool operator==(const loc_reft other) const
Definition: loc_ref.h:75
void increase()
Definition: loc_ref.h:29
loc_reft next_loc() const
Definition: loc_ref.h:22
loc_reft & operator++()
Definition: loc_ref.h:53
static loc_reft nil()
Definition: loc_ref.h:48
void decrease()
Definition: loc_ref.h:34