add range_type to from_integer/to_integer

This adds support for range_typet to both from_integer and to_integer.
diffblue · Nov 26, 2024 · 20757e2 · 20757e2
1 parent 162e0f7
commit 20757e2
Showing 1 changed file with 8 additions and 2 deletions.
diff --git 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();