diff --git a/jbmc/src/java_bytecode/java_pointer_casts.cpp b/jbmc/src/java_bytecode/java_pointer_casts.cpp index 68992ca76fd..7dce1a3b524 100644 --- a/jbmc/src/java_bytecode/java_pointer_casts.cpp +++ b/jbmc/src/java_bytecode/java_pointer_casts.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_pointer_casts.h" +#include #include #include #include @@ -64,21 +65,6 @@ bool find_superclass_with_type( } } - -/// \par parameters: input expression -/// \return recursively search target of typecast -static const exprt &look_through_casts(const exprt &in) -{ - if(in.id()==ID_typecast) - { - assert(in.type().id()==ID_pointer); - return look_through_casts(to_typecast_expr(in).op()); - } - else - return in; -} - - /// \par parameters: raw pointer /// target type /// namespace @@ -88,7 +74,7 @@ exprt make_clean_pointer_cast( const pointer_typet &target_type, const namespacet &ns) { - const exprt &ptr=look_through_casts(rawptr); + const exprt &ptr = skip_typecast(rawptr); PRECONDITION(ptr.type().id()==ID_pointer); diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index c293ac2eca1..7ad4eb52908 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -10,6 +10,7 @@ #include #include +#include #include #include #include @@ -74,15 +75,6 @@ static index_range_implementation_ptrt make_interval_index_range( return util_make_unique(interval, n); } -static inline exprt look_through_casts(exprt e) -{ - while(e.id() == ID_typecast) - { - e = to_typecast_expr(e).op(); - } - return e; -} - static inline bool bvint_value_is_max(const typet &type, const mp_integer &value) { @@ -153,15 +145,16 @@ interval_from_x_gt_value(const exprt &value) return constant_interval_exprt::bottom(value.type()); } -static inline bool represents_interval(exprt e) +static inline bool represents_interval(const exprt &expr) { - e = look_through_casts(e); + const exprt &e = skip_typecast(expr); return (e.id() == ID_constant_interval || e.id() == ID_constant); } -static inline constant_interval_exprt make_interval_expr(exprt e) +static inline constant_interval_exprt make_interval_expr(const exprt &expr) { - e = look_through_casts(e); + const exprt &e = skip_typecast(expr); + if(e.id() == ID_constant_interval) { return to_constant_interval_expr(e);