Skip to content

Commit b06a27d

Browse files
Introduce abstract qualifierst base class
1 parent e6fb3bf commit b06a27d

File tree

9 files changed

+126
-113
lines changed

9 files changed

+126
-113
lines changed

src/ansi-c/c_qualifiers.cpp

+4-6
Original file line numberDiff line numberDiff line change
@@ -24,11 +24,11 @@ c_qualifierst &c_qualifierst::operator=(const c_qualifierst &other)
2424
return *this;
2525
}
2626

27-
std::unique_ptr<c_qualifierst> c_qualifierst::clone() const
27+
std::unique_ptr<qualifierst> c_qualifierst::clone() const
2828
{
2929
auto other = util_make_unique<c_qualifierst>();
3030
*other = *this;
31-
return other;
31+
return std::move(other);
3232
}
3333

3434
std::string c_qualifierst::as_string() const
@@ -141,9 +141,7 @@ void c_qualifierst::clear(typet &dest)
141141
}
142142

143143
/// pretty-print the qualifiers
144-
std::ostream &operator << (
145-
std::ostream &out,
146-
const c_qualifierst &c_qualifiers)
144+
std::ostream &operator<<(std::ostream &out, const qualifierst &qualifiers)
147145
{
148-
return out << c_qualifiers.as_string();
146+
return out << qualifiers.as_string();
149147
}

src/ansi-c/c_qualifiers.h

+83-44
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,49 @@ Author: Daniel Kroening, [email protected]
1515

1616
#include <util/expr.h>
1717

18-
class c_qualifierst
18+
class qualifierst
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;
29+
qualifierst &operator=(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
1961
{
2062
public:
2163
c_qualifierst()
@@ -29,13 +71,12 @@ class c_qualifierst
2971
read(src);
3072
}
3173

32-
c_qualifierst(const c_qualifierst &other) = delete;
33-
virtual c_qualifierst &operator=(const c_qualifierst &other);
34-
virtual std::unique_ptr<c_qualifierst> clone() const;
35-
36-
virtual ~c_qualifierst() = default;
74+
protected:
75+
c_qualifierst &operator=(const c_qualifierst &other);
76+
public:
77+
virtual std::unique_ptr<qualifierst> clone() const override;
3778

38-
virtual void clear()
79+
virtual void clear() override
3980
{
4081
is_constant=false;
4182
is_volatile=false;
@@ -57,62 +98,60 @@ class c_qualifierst
5798

5899
// will likely add alignment here as well
59100

60-
virtual std::string as_string() const;
61-
virtual void read(const typet &src);
62-
virtual void write(typet &src) const;
101+
virtual std::string as_string() const override;
102+
virtual void read(const typet &src) override;
103+
virtual void write(typet &src) const override;
63104

64105
static void clear(typet &dest);
65106

66-
virtual bool is_subset_of(const c_qualifierst &q) const
107+
virtual bool is_subset_of(const qualifierst &other) const override
67108
{
68-
return (!is_constant || q.is_constant) &&
69-
(!is_volatile || q.is_volatile) &&
70-
(!is_restricted || q.is_restricted) &&
71-
(!is_atomic || q.is_atomic) &&
72-
(!is_ptr32 || q.is_ptr32) &&
73-
(!is_ptr64 || q.is_ptr64) &&
74-
(!is_noreturn || q.is_noreturn);
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);
75118

76119
// is_transparent_union isn't checked
77120
}
78121

79-
virtual bool operator==(const c_qualifierst &other) const
122+
virtual bool operator==(const qualifierst &other) const override
80123
{
81-
return is_constant==other.is_constant &&
82-
is_volatile==other.is_volatile &&
83-
is_restricted==other.is_restricted &&
84-
is_atomic==other.is_atomic &&
85-
is_ptr32==other.is_ptr32 &&
86-
is_ptr64==other.is_ptr64 &&
87-
is_transparent_union==other.is_transparent_union &&
88-
is_noreturn==other.is_noreturn;
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 &&
132+
is_transparent_union == cq->is_transparent_union &&
133+
is_noreturn == cq->is_noreturn;
89134
}
90135

91-
bool operator!=(const c_qualifierst &other) const
136+
virtual qualifierst &operator+=(const qualifierst &other) override
92137
{
93-
return !(*this==other);
94-
}
95-
96-
virtual c_qualifierst &operator+=(const c_qualifierst &b)
97-
{
98-
is_constant|=b.is_constant;
99-
is_volatile|=b.is_volatile;
100-
is_restricted|=b.is_restricted;
101-
is_atomic|=b.is_atomic;
102-
is_ptr32|=b.is_ptr32;
103-
is_ptr64|=b.is_ptr64;
104-
is_transparent_union|=b.is_transparent_union;
105-
is_noreturn|=b.is_noreturn;
138+
const c_qualifierst *cq = dynamic_cast<const c_qualifierst *>(&other);
139+
is_constant |= cq->is_constant;
140+
is_volatile |= cq->is_volatile;
141+
is_restricted |= cq->is_restricted;
142+
is_atomic |= cq->is_atomic;
143+
is_ptr32 |= cq->is_ptr32;
144+
is_ptr64 |= cq->is_ptr64;
145+
is_transparent_union |= cq->is_transparent_union;
146+
is_noreturn |= cq->is_noreturn;
106147
return *this;
107148
}
108149

109-
virtual std::size_t count() const
150+
virtual std::size_t count() const override
110151
{
111152
return is_constant+is_volatile+is_restricted+is_atomic+
112153
is_ptr32+is_ptr64+is_noreturn;
113154
}
114155
};
115156

116-
std::ostream &operator << (std::ostream &, const c_qualifierst &);
117-
118157
#endif // CPROVER_ANSI_C_C_QUALIFIERS_H

src/ansi-c/expr2c.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -162,11 +162,11 @@ std::string expr2ct::convert(const typet &src)
162162

163163
std::string expr2ct::convert_rec(
164164
const typet &src,
165-
const c_qualifierst &qualifiers,
165+
const qualifierst &qualifiers,
166166
const std::string &declarator)
167167
{
168-
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
169-
c_qualifierst &new_qualifiers = *clone;
168+
std::unique_ptr<qualifierst> clone = qualifiers.clone();
169+
c_qualifierst &new_qualifiers = dynamic_cast<c_qualifierst &>(*clone);
170170
new_qualifiers.read(src);
171171

172172
std::string q=new_qualifiers.as_string();
@@ -737,7 +737,7 @@ std::string expr2ct::convert_struct_type(
737737
/// \return A C-like type declaration of an array
738738
std::string expr2ct::convert_array_type(
739739
const typet &src,
740-
const c_qualifierst &qualifiers,
740+
const qualifierst &qualifiers,
741741
const std::string &declarator_str)
742742
{
743743
return convert_array_type(src, qualifiers, declarator_str, true);
@@ -753,7 +753,7 @@ std::string expr2ct::convert_array_type(
753753
/// \return A C-like type declaration of an array
754754
std::string expr2ct::convert_array_type(
755755
const typet &src,
756-
const c_qualifierst &qualifiers,
756+
const qualifierst &qualifiers,
757757
const std::string &declarator_str,
758758
bool inc_size_if_possible)
759759
{

src/ansi-c/expr2c_class.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/std_code.h>
1818
#include <util/std_expr.h>
1919

20-
class c_qualifierst;
20+
class qualifierst;
2121
class namespacet;
2222

2323
class expr2ct
@@ -36,7 +36,7 @@ class expr2ct
3636

3737
virtual std::string convert_rec(
3838
const typet &src,
39-
const c_qualifierst &qualifiers,
39+
const qualifierst &qualifiers,
4040
const std::string &declarator);
4141

4242
virtual std::string convert_struct_type(
@@ -53,12 +53,12 @@ class expr2ct
5353

5454
virtual std::string convert_array_type(
5555
const typet &src,
56-
const c_qualifierst &qualifiers,
56+
const qualifierst &qualifiers,
5757
const std::string &declarator_str);
5858

5959
std::string convert_array_type(
6060
const typet &src,
61-
const c_qualifierst &qualifiers,
61+
const qualifierst &qualifiers,
6262
const std::string &declarator_str,
6363
bool inc_size_if_possible);
6464

src/cpp/expr2cpp.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ class expr2cppt:public expr2ct
4141

4242
std::string convert_rec(
4343
const typet &src,
44-
const c_qualifierst &qualifiers,
44+
const qualifierst &qualifiers,
4545
const std::string &declarator) override;
4646

4747
typedef std::unordered_set<std::string, string_hash> id_sett;
@@ -129,11 +129,11 @@ std::string expr2cppt::convert_constant(
129129

130130
std::string expr2cppt::convert_rec(
131131
const typet &src,
132-
const c_qualifierst &qualifiers,
132+
const qualifierst &qualifiers,
133133
const std::string &declarator)
134134
{
135-
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
136-
c_qualifierst &new_qualifiers = *clone;
135+
std::unique_ptr<qualifierst> clone = qualifiers.clone();
136+
qualifierst &new_qualifiers = *clone;
137137
new_qualifiers.read(src);
138138

139139
const std::string d=

src/java_bytecode/expr2java.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -251,11 +251,11 @@ std::string expr2javat::convert_constant(
251251

252252
std::string expr2javat::convert_rec(
253253
const typet &src,
254-
const c_qualifierst &qualifiers,
254+
const qualifierst &qualifiers,
255255
const std::string &declarator)
256256
{
257-
std::unique_ptr<c_qualifierst> clone = qualifiers.clone();
258-
c_qualifierst &new_qualifiers = *clone;
257+
std::unique_ptr<qualifierst> clone = qualifiers.clone();
258+
qualifierst &new_qualifiers = *clone;
259259
new_qualifiers.read(src);
260260

261261
const std::string d=

src/java_bytecode/expr2java.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ class expr2javat:public expr2ct
4141

4242
virtual std::string convert_rec(
4343
const typet &src,
44-
const c_qualifierst &qualifiers,
44+
const qualifierst &qualifiers,
4545
const std::string &declarator) override;
4646

4747
// length of string representation of Java Char

src/java_bytecode/java_qualifiers.cpp

+16-40
Original file line numberDiff line numberDiff line change
@@ -19,30 +19,7 @@ java_qualifierst &java_qualifierst::operator=(const java_qualifierst &other)
1919
return *this;
2020
}
2121

22-
java_qualifierst &java_qualifierst::operator=(java_qualifierst &&other)
23-
{
24-
INVARIANT(
25-
&other.ns == &ns,
26-
"Can only assign from a java_qualifierst using the same namespace");
27-
annotations = std::move(other.annotations);
28-
c_qualifierst::operator=(other);
29-
return *this;
30-
}
31-
32-
c_qualifierst &java_qualifierst::operator=(const c_qualifierst &c_other)
33-
{
34-
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
35-
if(other != nullptr)
36-
*this = *other;
37-
else
38-
{
39-
annotations.clear();
40-
c_qualifierst::operator=(c_other);
41-
}
42-
return *this;
43-
}
44-
45-
std::unique_ptr<c_qualifierst> java_qualifierst::clone() const
22+
std::unique_ptr<qualifierst> java_qualifierst::clone() const
4623
{
4724
auto other = util_make_unique<java_qualifierst>(ns);
4825
*other = *this;
@@ -74,37 +51,36 @@ void java_qualifierst::write(typet &src) const
7451
annotated_type.get_annotations() = annotations;
7552
}
7653

77-
c_qualifierst &java_qualifierst::operator+=(const c_qualifierst &c_other)
54+
qualifierst &java_qualifierst::operator+=(const qualifierst &other)
7855
{
79-
c_qualifierst::operator+=(c_other);
80-
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
81-
if(other != nullptr)
56+
c_qualifierst::operator+=(other);
57+
auto jq = dynamic_cast<const java_qualifierst *>(&other);
58+
if(jq != nullptr)
8259
{
8360
std::copy(
84-
other->annotations.begin(),
85-
other->annotations.end(),
61+
jq->annotations.begin(),
62+
jq->annotations.end(),
8663
std::back_inserter(annotations));
8764
}
8865
return *this;
8966
}
9067

91-
bool java_qualifierst::operator==(const c_qualifierst &c_other) const
68+
bool java_qualifierst::operator==(const qualifierst &other) const
9269
{
93-
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
94-
if(other == nullptr)
70+
auto jq = dynamic_cast<const java_qualifierst *>(&other);
71+
if(jq == nullptr)
9572
return false;
96-
return
97-
c_qualifierst::operator==(c_other) && annotations == other->annotations;
73+
return c_qualifierst::operator==(other) && annotations == jq->annotations;
9874
}
9975

100-
bool java_qualifierst::is_subset_of(const c_qualifierst &c_other) const
76+
bool java_qualifierst::is_subset_of(const qualifierst &other) const
10177
{
102-
if(!c_qualifierst::is_subset_of(c_other))
78+
if(!c_qualifierst::is_subset_of(other))
10379
return false;
104-
auto other = dynamic_cast<const java_qualifierst *>(&c_other);
105-
if(other == nullptr)
80+
auto jq = dynamic_cast<const java_qualifierst *>(&other);
81+
if(jq == nullptr)
10682
return annotations.empty();
107-
auto &other_a = other->annotations;
83+
auto &other_a = jq->annotations;
10884
for(const auto &annotation : annotations)
10985
{
11086
if(std::find(other_a.begin(), other_a.end(), annotation) == other_a.end())

0 commit comments

Comments
 (0)