Skip to content

Commit 1cc2c62

Browse files
committed
constructor for object_address_exprt with type
This adds a constructor for object_address_exprt that allows setting the type, e.g., to get the element type when construcing the address of an array.
1 parent e46d2f3 commit 1cc2c62

File tree

2 files changed

+10
-1
lines changed

2 files changed

+10
-1
lines changed

src/util/pointer_expr.cpp

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -122,7 +122,14 @@ address_of_exprt::address_of_exprt(const exprt &_op)
122122
}
123123

124124
object_address_exprt::object_address_exprt(const symbol_exprt &object)
125-
: nullary_exprt(ID_object_address, pointer_type(object.type()))
125+
: object_address_exprt(object, pointer_type(object.type()))
126+
{
127+
}
128+
129+
object_address_exprt::object_address_exprt(
130+
const symbol_exprt &object,
131+
pointer_typet type)
132+
: nullary_exprt(ID_object_address, std::move(type))
126133
{
127134
set(ID_identifier, object.get_identifier());
128135
}

src/util/pointer_expr.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -418,6 +418,8 @@ class object_address_exprt : public nullary_exprt
418418
public:
419419
explicit object_address_exprt(const symbol_exprt &);
420420

421+
object_address_exprt(const symbol_exprt &, pointer_typet);
422+
421423
irep_idt object_identifier() const
422424
{
423425
return get(ID_identifier);

0 commit comments

Comments
 (0)