From d089ddd4f9a7735d193e113e6ba2aebf76a59c8a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Jun 2018 22:49:14 +0100 Subject: [PATCH] Do not use c_typecast in pointer-analysis goto-programs are not C specific. --- src/pointer-analysis/module_dependencies.txt | 1 - src/pointer-analysis/value_set_dereference.cpp | 13 ++++--------- 2 files changed, 4 insertions(+), 10 deletions(-) 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);