Skip to content

Commit 7106860

Browse files
committed
Construct with_exprt in a non-deprecated way
The default constructor is deprecated.
1 parent caeaa10 commit 7106860

File tree

2 files changed

+6
-11
lines changed

2 files changed

+6
-11
lines changed

src/goto-programs/wp.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -166,12 +166,10 @@ 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,
170+
exprt(ID_member_name), rhs);
173171
new_rhs.where().set(ID_component_name, component_name);
174-
new_rhs.new_value()=rhs;
172+
new_rhs.type()=new_lhs.type();
175173

176174
lhs=new_lhs;
177175
rhs=new_rhs;
@@ -183,11 +181,8 @@ void rewrite_assignment(exprt &lhs, exprt &rhs)
183181
const index_exprt index_expr=to_index_expr(lhs);
184182
exprt new_lhs=index_expr.array();
185183

186-
with_exprt new_rhs;
184+
with_exprt new_rhs(new_lhs, index_expr.index(), rhs);
187185
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;
191186

192187
lhs=new_lhs;
193188
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)