Skip to content

Commit ab22e9f

Browse files
authored
Merge pull request #8493 from diffblue/zero-extend-smt2
use `zero_extend_exprt` in SMT2 front-end
2 parents 875fbd9 + 7687a69 commit ab22e9f

File tree

2 files changed

+22
-7
lines changed

2 files changed

+22
-7
lines changed

src/solvers/smt2/smt2_parser.cpp

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -656,7 +656,7 @@ exprt smt2_parsert::function_application()
656656
if(next_token() != smt2_tokenizert::NUMERAL)
657657
throw error() << "expected numeral after " << id;
658658

659-
auto index = std::stoll(smt2_tokenizer.get_buffer());
659+
auto index = string2integer(smt2_tokenizer.get_buffer());
660660

661661
if(next_token() != smt2_tokenizert::CLOSE)
662662
throw error() << "expected ')' after " << id << " index";
@@ -681,21 +681,21 @@ exprt smt2_parsert::function_application()
681681
// we first convert to a signed type of the original width,
682682
// then extend to the new width, and then go to unsigned
683683
const auto width = to_unsignedbv_type(op[0].type()).get_width();
684-
const signedbv_typet small_signed_type(width);
685-
const signedbv_typet large_signed_type(width + index);
686-
const unsignedbv_typet unsigned_type(width + index);
684+
const signedbv_typet small_signed_type{width};
685+
const signedbv_typet large_signed_type{width + index};
686+
const unsignedbv_typet unsigned_type{width + index};
687687

688688
return typecast_exprt(
689689
typecast_exprt(
690690
typecast_exprt(op[0], small_signed_type), large_signed_type),
691691
unsigned_type);
692692
}
693-
else if(id=="zero_extend")
693+
else if(id == ID_zero_extend)
694694
{
695695
auto width=to_unsignedbv_type(op[0].type()).get_width();
696-
unsignedbv_typet unsigned_type(width+index);
696+
unsignedbv_typet unsigned_type{width + index};
697697

698-
return typecast_exprt(op[0], unsigned_type);
698+
return zero_extend_exprt{op[0], unsigned_type};
699699
}
700700
else if(id == ID_repeat)
701701
{

src/util/bitvector_types.h

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,11 @@ class integer_bitvector_typet : public bitvector_typet
107107
{
108108
}
109109

110+
integer_bitvector_typet(const irep_idt &id, const mp_integer &width)
111+
: bitvector_typet(id, width)
112+
{
113+
}
114+
110115
/// Return the smallest value that can be represented using this type.
111116
mp_integer smallest() const;
112117
/// Return the largest value that can be represented using this type.
@@ -167,6 +172,11 @@ class unsignedbv_typet : public integer_bitvector_typet
167172
{
168173
}
169174

175+
explicit unsignedbv_typet(const mp_integer &width)
176+
: integer_bitvector_typet(ID_unsignedbv, width)
177+
{
178+
}
179+
170180
static void check(
171181
const typet &type,
172182
const validation_modet vm = validation_modet::INVARIANT)
@@ -216,6 +226,11 @@ class signedbv_typet : public integer_bitvector_typet
216226
{
217227
}
218228

229+
explicit signedbv_typet(const mp_integer &width)
230+
: integer_bitvector_typet(ID_signedbv, width)
231+
{
232+
}
233+
219234
static void check(
220235
const typet &type,
221236
const validation_modet vm = validation_modet::INVARIANT)

0 commit comments

Comments
 (0)