CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
c_qualifiers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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 <memory>
14#include <string>
15
16class typet;
17
19{
20public:
22 {
23 clear();
24 }
25
26 explicit c_qualifierst(const typet &src)
27 {
28 clear();
29 read(src);
30 }
31
32 virtual ~c_qualifierst() = default;
33
34protected:
36public:
37 virtual std::unique_ptr<c_qualifierst> clone() const;
38
39 virtual void clear()
40 {
41 is_constant=false;
42 is_volatile=false;
43 is_restricted=false;
44 is_atomic=false;
45 is_ptr32=is_ptr64=false;
47 is_nodiscard = false;
48 is_noreturn=false;
49 }
50
51 // standard ones
54
55 // MS Visual Studio extension
57
58 // gcc extension
60
61 // will likely add alignment here as well
62
63 virtual std::string as_string() const;
64 virtual void read(const typet &src);
65 virtual void write(typet &src) const;
66
67 static void clear(typet &dest);
68
69 bool is_subset_of(const c_qualifierst &other) const
70 {
71 return (!is_constant || other.is_constant) &&
72 (!is_volatile || other.is_volatile) &&
73 (!is_restricted || other.is_restricted) &&
74 (!is_atomic || other.is_atomic) && (!is_ptr32 || other.is_ptr32) &&
75 (!is_ptr64 || other.is_ptr64) &&
76 (!is_nodiscard || other.is_nodiscard) &&
77 (!is_noreturn || other.is_noreturn);
78
79 // is_transparent_union isn't checked
80 }
81
82 bool operator==(const c_qualifierst &other) const
83 {
84 return is_constant == other.is_constant &&
85 is_volatile == other.is_volatile &&
87 is_atomic == other.is_atomic && is_ptr32 == other.is_ptr32 &&
88 is_ptr64 == other.is_ptr64 &&
90 is_nodiscard == other.is_nodiscard &&
91 is_noreturn == other.is_noreturn;
92 }
93
94 bool operator!=(const c_qualifierst &other) const
95 {
96 return !(*this == other);
97 }
98
100 {
101 is_constant |= other.is_constant;
102 is_volatile |= other.is_volatile;
104 is_atomic |= other.is_atomic;
105 is_ptr32 |= other.is_ptr32;
106 is_ptr64 |= other.is_ptr64;
108 is_nodiscard |= other.is_nodiscard;
109 is_noreturn |= other.is_noreturn;
110 return *this;
111 }
112
113 virtual std::size_t count() const
114 {
117 }
118};
119
120#endif // CPROVER_ANSI_C_C_QUALIFIERS_H
c_qualifierst(const typet &src)
virtual void write(typet &src) const
bool operator!=(const c_qualifierst &other) const
virtual ~c_qualifierst()=default
c_qualifierst & operator+=(const c_qualifierst &other)
bool is_transparent_union
virtual std::unique_ptr< c_qualifierst > clone() const
bool is_subset_of(const c_qualifierst &other) const
virtual std::size_t count() const
virtual void clear()
virtual std::string as_string() const
c_qualifierst & operator=(const c_qualifierst &other)
bool operator==(const c_qualifierst &other) const
The type of an expression, extends irept.
Definition type.h:29
int __CPROVER_ID java::java io InputStream read
Definition java.io.c:5