Skip to content

Commit ee8d275

Browse files
authored
Merge pull request #8520 from diffblue/range_type_arith_tools
add range_type to `from_integer`/`to_integer`
2 parents 162e0f7 + 20757e2 commit ee8d275

File tree

1 file changed

+8
-2
lines changed

1 file changed

+8
-2
lines changed

src/util/arith_tools.cpp

+8-2
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
3131
return false;
3232
}
3333
}
34-
else if(type_id==ID_integer ||
35-
type_id==ID_natural)
34+
else if(type_id == ID_integer || type_id == ID_natural || type_id == ID_range)
3635
{
3736
int_value=string2integer(id2string(value));
3837
return false;
@@ -112,6 +111,13 @@ constant_exprt from_integer(
112111
PRECONDITION(int_value >= 0);
113112
return constant_exprt(integer2string(int_value), type);
114113
}
114+
else if(type_id == ID_range)
115+
{
116+
auto &range_type = to_range_type(type);
117+
PRECONDITION(int_value >= range_type.get_from());
118+
PRECONDITION(int_value <= range_type.get_to());
119+
return constant_exprt{integer2string(int_value), type};
120+
}
115121
else if(type_id==ID_unsignedbv)
116122
{
117123
std::size_t width=to_unsignedbv_type(type).get_width();

0 commit comments

Comments
 (0)