Skip to content

Commit 7566bbf

Browse files
committed
Construct with_exprt in a non-deprecated way
The default constructor is deprecated.
1 parent c6d6879 commit 7566bbf

File tree

2 files changed

+5
-11
lines changed

2 files changed

+5
-11
lines changed

src/goto-programs/wp.cpp

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -166,12 +166,9 @@ void rewrite_assignment(exprt &lhs, exprt &rhs)
166166
irep_idt component_name=member_expr.get_component_name();
167167
exprt new_lhs=member_expr.struct_op();
168168

169-
with_exprt new_rhs;
170-
new_rhs.type()=new_lhs.type();
171-
new_rhs.old()=new_lhs;
172-
new_rhs.where().id(ID_member_name);
169+
with_exprt new_rhs(new_lhs, exprt(ID_member_name), rhs);
173170
new_rhs.where().set(ID_component_name, component_name);
174-
new_rhs.new_value()=rhs;
171+
new_rhs.type() = new_lhs.type();
175172

176173
lhs=new_lhs;
177174
rhs=new_rhs;
@@ -183,11 +180,8 @@ void rewrite_assignment(exprt &lhs, exprt &rhs)
183180
const index_exprt index_expr=to_index_expr(lhs);
184181
exprt new_lhs=index_expr.array();
185182

186-
with_exprt new_rhs;
183+
with_exprt new_rhs(new_lhs, index_expr.index(), rhs);
187184
new_rhs.type()=new_lhs.type();
188-
new_rhs.old()=new_lhs;
189-
new_rhs.where()=index_expr.index();
190-
new_rhs.new_value()=rhs;
191185

192186
lhs=new_lhs;
193187
rhs=new_rhs;

src/util/expr_util.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -69,12 +69,12 @@ with_exprt make_with_expr(const update_exprt &src)
6969
const exprt::operandst &designator=src.designator();
7070
PRECONDITION(!designator.empty());
7171

72-
with_exprt result;
72+
with_exprt result{exprt{}, exprt{}, exprt{}};
7373
exprt *dest=&result;
7474

7575
forall_expr(it, designator)
7676
{
77-
with_exprt tmp;
77+
with_exprt tmp{exprt{}, exprt{}, exprt{}};
7878

7979
if(it->id()==ID_index_designator)
8080
{

0 commit comments

Comments
 (0)