diff --git a/src/pointer-analysis/module_dependencies.txt b/src/pointer-analysis/module_dependencies.txt index 8962462ddc2..25dc8fec88e 100644 --- a/src/pointer-analysis/module_dependencies.txt +++ b/src/pointer-analysis/module_dependencies.txt @@ -1,5 +1,4 @@ analyses -ansi-c # should go away goto-programs langapi # should go away pointer-analysis diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 047de523144..739f6dd1b07 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -31,8 +31,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include - // global data, horrible unsigned int value_set_dereferencet::invalid_counter=0; @@ -712,13 +710,10 @@ void value_set_dereferencet::bounds_check( if(size_expr.is_nil()) throw "index array operand of wrong type"; - binary_relation_exprt inequality(expr.index(), ID_ge, size_expr); - - if(c_implicit_typecast( - inequality.op0(), - inequality.op1().type(), - ns)) - throw "index address of wrong type"; + binary_relation_exprt inequality( + typecast_exprt::conditional_cast(expr.index(), size_expr.type()), + ID_ge, + size_expr); guardt tmp_guard(guard); tmp_guard.add(inequality);