diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index b2255cd2e95..c482eb9b961 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "arith_tools.h" #include "c_types.h" -#include "config.h" #include "expr_util.h" #include "namespace.h" #include "pointer_expr.h" @@ -400,23 +399,6 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr) { return from_integer(0, expr.type()); } - else - { - // this is a pointer, we can't use to_integer - const auto width = to_pointer_type(ptr.type()).get_width(); - mp_integer number = bvrep2integer(c_ptr.get_value(), width, false); - // a null pointer would have been caught above, return value 0 - // will indicate that conversion failed - if(number==0) - return unchanged(expr); - - // The constant address consists of OBJECT-ID || OFFSET. - mp_integer offset_bits = - *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits; - number%=power(2, offset_bits); - - return from_integer(number, expr.type()); - } } return unchanged(expr); diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 756666240a6..8219df4f45f 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -44,27 +44,6 @@ TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]") REQUIRE(offset_value==1); } -TEST_CASE("Simplify const pointer offset", "[core][util]") -{ - config.set_arch("none"); - - symbol_tablet symbol_table; - namespacet ns(symbol_table); - - // build a numeric constant of some pointer type - constant_exprt number=from_integer(1234, size_type()); - number.type()=pointer_type(char_type()); - - exprt p_o=pointer_offset(number); - - exprt simp=simplify_expr(p_o, ns); - - REQUIRE(simp.is_constant()); - const mp_integer offset_value = - numeric_cast_v(to_constant_expr(simp)); - REQUIRE(offset_value==1234); -} - TEST_CASE("Simplify byte extract", "[core][util]") { // this test does require a proper architecture to be set so that byte extract