diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index b907cef042f..e5bd4416fbd 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -117,11 +117,6 @@ class goto_checkt void invalidate(const exprt &lhs); - inline static bool has_dereference(const exprt &src) - { - return has_subexpr(src, ID_dereference); - } - bool enable_bounds_check; bool enable_pointer_check; bool enable_memory_leak_check; @@ -200,8 +195,7 @@ void goto_checkt::invalidate(const exprt &lhs) assertionst::iterator next=it; next++; - if(has_symbol(*it, find_symbols_set) || - has_dereference(*it)) + if(has_symbol(*it, find_symbols_set) || has_subexpr(*it, ID_dereference)) assertions.erase(it); it=next; diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index be0f162c539..1e75359671b 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -14,6 +14,7 @@ Date: April 2010 #include #include +#include #include #include #include @@ -617,8 +618,7 @@ void rw_range_set_value_sett::get_objects_dereference( // value_set_dereferencet::build_reference_to will turn *p into // DYNAMIC_OBJECT(p) ? *p : invalid_objectN - if(object.is_not_nil() && - !value_set_dereferencet::has_dereference(object)) + if(object.is_not_nil() && !has_subexpr(object, ID_dereference)) get_objects_rec(mode, object, range_start, new_size); } diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index fbcbcde2ee1..efc0dd510fd 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_program_dereference.h" +#include #include #include #include @@ -97,7 +98,7 @@ void goto_program_dereferencet::dereference_rec( guardt &guard, const value_set_dereferencet::modet mode) { - if(!dereference.has_dereference(expr)) + if(!has_subexpr(expr, ID_dereference)) return; if(expr.id()==ID_and || expr.id()==ID_or) @@ -114,7 +115,7 @@ void goto_program_dereferencet::dereference_rec( throw expr.id_string()+" takes Boolean operands only, but got "+ op.pretty(); - if(dereference.has_dereference(op)) + if(has_subexpr(op, ID_dereference)) dereference_rec(op, guard, value_set_dereferencet::modet::READ); if(expr.id()==ID_or) @@ -146,8 +147,8 @@ void goto_program_dereferencet::dereference_rec( dereference_rec(expr.op0(), guard, value_set_dereferencet::modet::READ); - bool o1=dereference.has_dereference(expr.op1()); - bool o2=dereference.has_dereference(expr.op2()); + bool o1 = has_subexpr(expr.op1(), ID_dereference); + bool o2 = has_subexpr(expr.op2(), ID_dereference); if(o1) { diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index c29cd31fc3c..70f07ffad59 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -47,11 +47,6 @@ Author: Daniel Kroening, kroening@kroening.com // global data, horrible unsigned int value_set_dereferencet::invalid_counter=0; -bool value_set_dereferencet::has_dereference(const exprt &expr) -{ - return has_subexpr(expr, ID_dereference); -} - const exprt &value_set_dereferencet::get_symbol(const exprt &expr) { if(expr.id()==ID_member || expr.id()==ID_index) diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h index 4687d671ec6..a2475823b1c 100644 --- a/src/pointer-analysis/value_set_dereference.h +++ b/src/pointer-analysis/value_set_dereference.h @@ -72,10 +72,6 @@ class value_set_dereferencet const guardt &guard, const modet mode); - /*! \brief Returns 'true' iff the given expression contains unary '*' - */ - static bool has_dereference(const exprt &expr); - typedef std::unordered_set expr_sett; private: