Skip to content

Commit 7d57fda

Browse files
NathanJPhillipspeterschrammel
authored andcommitted
Add get-underlying-object utility
This looks through member expressions.
1 parent db44fce commit 7d57fda

File tree

2 files changed

+7
-0
lines changed

2 files changed

+7
-0
lines changed

src/util/expr_util.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -236,3 +236,8 @@ if_exprt lift_if(const exprt &src, std::size_t operand_number)
236236

237237
return result;
238238
}
239+
240+
const exprt &get_underlying_object(const exprt &in)
241+
{
242+
return in.id()!=ID_member ? in : get_underlying_object(in.op0());
243+
}

src/util/expr_util.h

+2
Original file line numberDiff line numberDiff line change
@@ -51,4 +51,6 @@ bool has_subexpr(const exprt &, const irep_idt &);
5151
/*! lift up an if_exprt one level */
5252
if_exprt lift_if(const exprt &, std::size_t operand_number);
5353

54+
const exprt &get_underlying_object(const exprt &possible_member);
55+
5456
#endif // CPROVER_UTIL_EXPR_UTIL_H

0 commit comments

Comments
 (0)