Skip to content

Commit 22cf9a5

Browse files
committed
Move methods from (un)signedbv typet to parent class
These methods are now all identical and can be inherited from bitvector_typet.
1 parent 13a058c commit 22cf9a5

File tree

2 files changed

+11
-42
lines changed

2 files changed

+11
-42
lines changed

src/util/std_types.cpp

Lines changed: 5 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -162,52 +162,27 @@ mp_integer range_typet::get_to() const
162162
return string2integer(get_string(ID_to));
163163
}
164164

165-
mp_integer signedbv_typet::smallest() const
165+
mp_integer bitvector_typet::smallest() const
166166
{
167167
return bv_spect(*this).min_value();
168168
}
169169

170-
mp_integer signedbv_typet::largest() const
170+
mp_integer bitvector_typet::largest() const
171171
{
172172
return bv_spect(*this).max_value();
173173
}
174174

175-
constant_exprt signedbv_typet::zero_expr() const
175+
constant_exprt bitvector_typet::zero_expr() const
176176
{
177177
return from_integer(0, *this);
178178
}
179179

180-
constant_exprt signedbv_typet::smallest_expr() const
180+
constant_exprt bitvector_typet::smallest_expr() const
181181
{
182182
return from_integer(smallest(), *this);
183183
}
184184

185-
constant_exprt signedbv_typet::largest_expr() const
186-
{
187-
return from_integer(largest(), *this);
188-
}
189-
190-
mp_integer unsignedbv_typet::smallest() const
191-
{
192-
return bv_spect(*this).min_value();
193-
}
194-
195-
mp_integer unsignedbv_typet::largest() const
196-
{
197-
return bv_spect(*this).max_value();
198-
}
199-
200-
constant_exprt unsignedbv_typet::zero_expr() const
201-
{
202-
return from_integer(0, *this);
203-
}
204-
205-
constant_exprt unsignedbv_typet::smallest_expr() const
206-
{
207-
return from_integer(smallest(), *this);
208-
}
209-
210-
constant_exprt unsignedbv_typet::largest_expr() const
185+
constant_exprt bitvector_typet::largest_expr() const
211186
{
212187
return from_integer(largest(), *this);
213188
}

src/util/std_types.h

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1071,6 +1071,12 @@ class bitvector_typet : public typet
10711071
set(ID_width, narrow_cast<long long>(width));
10721072
}
10731073

1074+
mp_integer smallest() const;
1075+
mp_integer largest() const;
1076+
constant_exprt smallest_expr() const;
1077+
constant_exprt zero_expr() const;
1078+
constant_exprt largest_expr() const;
1079+
10741080
static void check(
10751081
const typet &type,
10761082
const validation_modet vm = validation_modet::INVARIANT)
@@ -1176,12 +1182,6 @@ class unsignedbv_typet:public bitvector_typet
11761182
{
11771183
}
11781184

1179-
mp_integer smallest() const;
1180-
mp_integer largest() const;
1181-
constant_exprt smallest_expr() const;
1182-
constant_exprt zero_expr() const;
1183-
constant_exprt largest_expr() const;
1184-
11851185
static void check(
11861186
const typet &type,
11871187
const validation_modet vm = validation_modet::INVARIANT)
@@ -1231,12 +1231,6 @@ class signedbv_typet:public bitvector_typet
12311231
{
12321232
}
12331233

1234-
mp_integer smallest() const;
1235-
mp_integer largest() const;
1236-
constant_exprt smallest_expr() const;
1237-
constant_exprt zero_expr() const;
1238-
constant_exprt largest_expr() const;
1239-
12401234
static void check(
12411235
const typet &type,
12421236
const validation_modet vm = validation_modet::INVARIANT)

0 commit comments

Comments
 (0)