Skip to content

Commit cbc2700

Browse files
author
kroening
committed
added has_subexpr()
1 parent 7bd7f16 commit cbc2700

File tree

4 files changed

+30
-24
lines changed

4 files changed

+30
-24
lines changed

src/analyses/goto_check.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -88,17 +88,9 @@ class goto_checkt
8888

8989
void invalidate(const exprt &lhs);
9090

91-
static bool has_dereference(const exprt &src)
91+
inline static bool has_dereference(const exprt &src)
9292
{
93-
if(src.id()==ID_dereference)
94-
return true;
95-
else
96-
{
97-
forall_operands(it, src)
98-
if(has_dereference(*it)) return true;
99-
100-
return false;
101-
}
93+
return has_subexpr(src, ID_dereference);
10294
}
10395

10496
bool enable_bounds_check;

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -60,20 +60,7 @@ Function: value_set_dereferencet::has_dereference
6060

6161
bool value_set_dereferencet::has_dereference(const exprt &expr)
6262
{
63-
forall_operands(it, expr)
64-
if(has_dereference(*it))
65-
return true;
66-
67-
if(expr.id()==ID_dereference)
68-
return true;
69-
70-
// we no longer do this one
71-
if(expr.id()==ID_index &&
72-
expr.operands().size()==2 &&
73-
expr.op0().type().id()==ID_pointer)
74-
assert(false);
75-
76-
return false;
63+
return has_subexpr(expr, ID_dereference);
7764
}
7865

7966
/*******************************************************************\

src/util/expr_util.cpp

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -414,3 +414,27 @@ exprt boolean_negate(const exprt &src)
414414
else
415415
return not_exprt(src);
416416
}
417+
418+
/*******************************************************************\
419+
420+
Function: has_subexpr
421+
422+
Inputs:
423+
424+
Outputs:
425+
426+
Purpose:
427+
428+
\*******************************************************************/
429+
430+
bool has_subexpr(const exprt &src, const irep_idt &id)
431+
{
432+
if(src.id()==id) return true;
433+
434+
forall_operands(it, src)
435+
if(has_subexpr(*it, id))
436+
return true;
437+
438+
return false;
439+
}
440+

src/util/expr_util.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,3 +52,6 @@ exprt is_not_zero(const exprt &, const namespacet &ns);
5252
/*! negate a Boolean expression, possibly removing a not_exprt,
5353
and swapping false and true */
5454
exprt boolean_negate(const exprt &);
55+
56+
/*! returns true if the expression has a subexpresion with given ID */
57+
bool has_subexpr(const exprt &, const irep_idt &);

0 commit comments

Comments
 (0)