File tree 1 file changed +11
-0
lines changed
1 file changed +11
-0
lines changed Original file line number Diff line number Diff line change @@ -1176,10 +1176,21 @@ class integer_bitvector_typet : public bitvector_typet
1176
1176
{
1177
1177
}
1178
1178
1179
+ // / Return the smallest value that can be represented using this type.
1179
1180
mp_integer smallest () const ;
1181
+ // / Return the largest value that can be represented using this type.
1180
1182
mp_integer largest () const ;
1183
+
1184
+ // If we ever need any of the following three methods in \ref fixedbv_typet or
1185
+ // \ref floatbv_typet, we might want to move them to a new class
1186
+ // numeric_bitvector_typet, which would be between integer_bitvector_typet and
1187
+ // bitvector_typet in the hierarchy.
1188
+
1189
+ // / Return an expression representing the smallest value of this type.
1181
1190
constant_exprt smallest_expr () const ;
1191
+ // / Return an expression representing the zero value of this type.
1182
1192
constant_exprt zero_expr () const ;
1193
+ // / Return an expression representing the largest value of this type.
1183
1194
constant_exprt largest_expr () const ;
1184
1195
};
1185
1196
You can’t perform that action at this time.
0 commit comments