From 20757e2d36d129359a28285a5c3491ae9eb2676d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 26 Nov 2024 16:55:08 +0000 Subject: [PATCH] add range_type to from_integer/to_integer This adds support for range_typet to both from_integer and to_integer. --- src/util/arith_tools.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 87babfb8b68..73dc989bf99 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -31,8 +31,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value) return false; } } - else if(type_id==ID_integer || - type_id==ID_natural) + else if(type_id == ID_integer || type_id == ID_natural || type_id == ID_range) { int_value=string2integer(id2string(value)); return false; @@ -112,6 +111,13 @@ constant_exprt from_integer( PRECONDITION(int_value >= 0); return constant_exprt(integer2string(int_value), type); } + else if(type_id == ID_range) + { + auto &range_type = to_range_type(type); + PRECONDITION(int_value >= range_type.get_from()); + PRECONDITION(int_value <= range_type.get_to()); + return constant_exprt{integer2string(int_value), type}; + } else if(type_id==ID_unsignedbv) { std::size_t width=to_unsignedbv_type(type).get_width();