Skip to content

Commit 01b7418

Browse files
author
Daniel Kroening
authored
Merge pull request #2710 from thomasspriggs/tas/struct_component
Add support for getting components by name to `struct_exprt`
2 parents b763877 + 21857a7 commit 01b7418

File tree

2 files changed

+33
-0
lines changed

2 files changed

+33
-0
lines changed

src/util/std_expr.cpp

+30
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
88

99
#include "std_expr.h"
1010

11+
#include <util/namespace.h>
12+
1113
#include <cassert>
1214

1315
#include "arith_tools.h"
@@ -167,3 +169,31 @@ address_of_exprt::address_of_exprt(const exprt &_op):
167169
unary_exprt(ID_address_of, _op, pointer_type(_op.type()))
168170
{
169171
}
172+
173+
// Implementation of struct_exprt::component for const / non const overloads.
174+
template <typename T>
175+
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns)
176+
-> decltype(struct_expr.op0())
177+
{
178+
static_assert(
179+
std::is_base_of<struct_exprt, T>::value, "T must be a struct_exprt.");
180+
const auto index =
181+
to_struct_type(ns.follow(struct_expr.type())).component_number(name);
182+
DATA_INVARIANT(
183+
index < struct_expr.operands().size(),
184+
"component matching index should exist");
185+
return struct_expr.operands()[index];
186+
}
187+
188+
/// \return The expression for a named component of this struct.
189+
exprt &struct_exprt::component(const irep_idt &name, const namespacet &ns)
190+
{
191+
return ::component(*this, name, ns);
192+
}
193+
194+
/// \return The expression for a named component of this struct.
195+
const exprt &
196+
struct_exprt::component(const irep_idt &name, const namespacet &ns) const
197+
{
198+
return ::component(*this, name, ns);
199+
}

src/util/std_expr.h

+3
Original file line numberDiff line numberDiff line change
@@ -1823,6 +1823,9 @@ class struct_exprt:public exprt
18231823
exprt(ID_struct, _type)
18241824
{
18251825
}
1826+
1827+
exprt &component(const irep_idt &name, const namespacet &ns);
1828+
const exprt &component(const irep_idt &name, const namespacet &ns) const;
18261829
};
18271830

18281831
/*! \brief Cast a generic exprt to a \ref struct_exprt

0 commit comments

Comments
 (0)