File tree 1 file changed +5
-4
lines changed 1 file changed +5
-4
lines changed Original file line number Diff line number Diff line change 13
13
#include " std_types.h"
14
14
15
15
#include " arith_tools.h"
16
+ #include " bv_arithmetic.h"
16
17
#include " namespace.h"
17
18
#include " std_expr.h"
18
19
#include " string2int.h"
@@ -163,12 +164,12 @@ mp_integer range_typet::get_to() const
163
164
164
165
mp_integer signedbv_typet::smallest () const
165
166
{
166
- return - power ( 2 , get_width ()- 1 );
167
+ return bv_spect (* this ). min_value ( );
167
168
}
168
169
169
170
mp_integer signedbv_typet::largest () const
170
171
{
171
- return power ( 2 , get_width ()- 1 )- 1 ;
172
+ return bv_spect (* this ). max_value () ;
172
173
}
173
174
174
175
constant_exprt signedbv_typet::zero_expr () const
@@ -188,12 +189,12 @@ constant_exprt signedbv_typet::largest_expr() const
188
189
189
190
mp_integer unsignedbv_typet::smallest () const
190
191
{
191
- return 0 ;
192
+ return bv_spect (* this ). min_value () ;
192
193
}
193
194
194
195
mp_integer unsignedbv_typet::largest () const
195
196
{
196
- return power ( 2 , get_width ())- 1 ;
197
+ return bv_spect (* this ). max_value () ;
197
198
}
198
199
199
200
constant_exprt unsignedbv_typet::zero_expr () const
You can’t perform that action at this time.
0 commit comments