cprover
c_qualifiers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_C_QUALIFIERS_H
11 #define CPROVER_ANSI_C_C_QUALIFIERS_H
12 
13 #include <iosfwd>
14 #include <memory>
15 
16 #include <util/expr.h>
17 
19 {
20 protected:
21  // Only derived classes can construct
22  qualifierst() = default;
23 
24 public:
25  // Copy/move construction/assignment is deleted here and in derived classes
26  qualifierst(const qualifierst &) = delete;
27  qualifierst(qualifierst &&) = delete;
28  qualifierst &operator=(const qualifierst &) = delete;
30 
31  // Destruction is virtual
32  virtual ~qualifierst() = default;
33 
34 public:
35  virtual std::unique_ptr<qualifierst> clone() const = 0;
36 
37  virtual qualifierst &operator+=(const qualifierst &b) = 0;
38 
39  virtual std::size_t count() const = 0;
40 
41  virtual void clear() = 0;
42 
43  virtual void read(const typet &src) = 0;
44  virtual void write(typet &src) const = 0;
45 
46  // Comparisons
47  virtual bool is_subset_of(const qualifierst &q) const = 0;
48  virtual bool operator==(const qualifierst &other) const = 0;
49  bool operator!=(const qualifierst &other) const
50  {
51  return !(*this == other);
52  }
53 
54  // String conversion
55  virtual std::string as_string() const = 0;
56  friend std::ostream &operator<<(std::ostream &, const qualifierst &);
57 };
58 
59 
60 class c_qualifierst : public qualifierst
61 {
62 public:
64  {
65  clear();
66  }
67 
68  explicit c_qualifierst(const typet &src)
69  {
70  clear();
71  read(src);
72  }
73 
74 protected:
75  c_qualifierst &operator=(const c_qualifierst &other);
76 public:
77  virtual std::unique_ptr<qualifierst> clone() const override;
78 
79  virtual void clear() override
80  {
81  is_constant=false;
82  is_volatile=false;
83  is_restricted=false;
84  is_atomic=false;
85  is_ptr32=is_ptr64=false;
87  is_noreturn=false;
88  }
89 
90  // standard ones
92 
93  // MS Visual Studio extension
95 
96  // gcc extension
98 
99  // will likely add alignment here as well
100 
101  virtual std::string as_string() const override;
102  virtual void read(const typet &src) override;
103  virtual void write(typet &src) const override;
104 
105  static void clear(typet &dest);
106 
107  virtual bool is_subset_of(const qualifierst &other) const override
108  {
109  const c_qualifierst *cq = dynamic_cast<const c_qualifierst *>(&other);
110  return
111  (!is_constant || cq->is_constant) &&
112  (!is_volatile || cq->is_volatile) &&
113  (!is_restricted || cq->is_restricted) &&
114  (!is_atomic || cq->is_atomic) &&
115  (!is_ptr32 || cq->is_ptr32) &&
116  (!is_ptr64 || cq->is_ptr64) &&
117  (!is_noreturn || cq->is_noreturn);
118 
119  // is_transparent_union isn't checked
120  }
121 
122  virtual bool operator==(const qualifierst &other) const override
123  {
124  const c_qualifierst *cq = dynamic_cast<const c_qualifierst *>(&other);
125  return
126  is_constant == cq->is_constant &&
127  is_volatile == cq->is_volatile &&
128  is_restricted == cq->is_restricted &&
129  is_atomic == cq->is_atomic &&
130  is_ptr32 == cq->is_ptr32 &&
131  is_ptr64 == cq->is_ptr64 &&
133  is_noreturn == cq->is_noreturn;
134  }
135 
136  virtual qualifierst &operator+=(const qualifierst &other) override
137  {
138  const c_qualifierst *cq = dynamic_cast<const c_qualifierst *>(&other);
139  is_constant |= cq->is_constant;
140  is_volatile |= cq->is_volatile;
142  is_atomic |= cq->is_atomic;
143  is_ptr32 |= cq->is_ptr32;
144  is_ptr64 |= cq->is_ptr64;
146  is_noreturn |= cq->is_noreturn;
147  return *this;
148  }
149 
150  virtual std::size_t count() const override
151  {
154  }
155 };
156 
157 #endif // CPROVER_ANSI_C_C_QUALIFIERS_H
c_qualifierst::read
virtual void read(const typet &src) override
Definition: c_qualifiers.cpp:62
qualifierst::qualifierst
qualifierst()=default
c_qualifierst::operator+=
virtual qualifierst & operator+=(const qualifierst &other) override
Definition: c_qualifiers.h:136
typet
The type of an expression, extends irept.
Definition: type.h:29
c_qualifierst::is_ptr64
bool is_ptr64
Definition: c_qualifiers.h:94
c_qualifierst::is_volatile
bool is_volatile
Definition: c_qualifiers.h:91
qualifierst::qualifierst
qualifierst(const qualifierst &)=delete
qualifierst::read
virtual void read(const typet &src)=0
c_qualifierst::is_subset_of
virtual bool is_subset_of(const qualifierst &other) const override
Definition: c_qualifiers.h:107
qualifierst
Definition: c_qualifiers.h:19
c_qualifierst::clear
virtual void clear() override
Definition: c_qualifiers.h:79
qualifierst::operator=
qualifierst & operator=(qualifierst &&)=delete
expr.h
c_qualifierst::is_constant
bool is_constant
Definition: c_qualifiers.h:91
qualifierst::operator<<
friend std::ostream & operator<<(std::ostream &, const qualifierst &)
pretty-print the qualifiers
Definition: c_qualifiers.cpp:144
c_qualifierst::operator==
virtual bool operator==(const qualifierst &other) const override
Definition: c_qualifiers.h:122
c_qualifierst::c_qualifierst
c_qualifierst()
Definition: c_qualifiers.h:63
qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const =0
c_qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const override
Definition: c_qualifiers.cpp:27
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
qualifierst::operator+=
virtual qualifierst & operator+=(const qualifierst &b)=0
c_qualifierst
Definition: c_qualifiers.h:61
qualifierst::operator=
qualifierst & operator=(const qualifierst &)=delete
c_qualifierst::count
virtual std::size_t count() const override
Definition: c_qualifiers.h:150
qualifierst::~qualifierst
virtual ~qualifierst()=default
c_qualifierst::operator=
c_qualifierst & operator=(const c_qualifierst &other)
Definition: c_qualifiers.cpp:14
qualifierst::is_subset_of
virtual bool is_subset_of(const qualifierst &q) const =0
qualifierst::operator!=
bool operator!=(const qualifierst &other) const
Definition: c_qualifiers.h:49
qualifierst::operator==
virtual bool operator==(const qualifierst &other) const =0
c_qualifierst::is_atomic
bool is_atomic
Definition: c_qualifiers.h:91
c_qualifierst::is_restricted
bool is_restricted
Definition: c_qualifiers.h:91
qualifierst::clear
virtual void clear()=0
c_qualifierst::c_qualifierst
c_qualifierst(const typet &src)
Definition: c_qualifiers.h:68
qualifierst::count
virtual std::size_t count() const =0
qualifierst::qualifierst
qualifierst(qualifierst &&)=delete
c_qualifierst::is_ptr32
bool is_ptr32
Definition: c_qualifiers.h:94
qualifierst::as_string
virtual std::string as_string() const =0
c_qualifierst::as_string
virtual std::string as_string() const override
Definition: c_qualifiers.cpp:34
c_qualifierst::is_noreturn
bool is_noreturn
Definition: c_qualifiers.h:91
qualifierst::write
virtual void write(typet &src) const =0
c_qualifierst::is_transparent_union
bool is_transparent_union
Definition: c_qualifiers.h:97