Skip to content

Commit 63701a7

Browse files
committed
Move make_with_expr to update_exprt
This will eventually remove one of the functions from the expr_util translation unit, which is supposed to be deprecated.
1 parent 4ae54e6 commit 63701a7

File tree

4 files changed

+36
-27
lines changed

4 files changed

+36
-27
lines changed

src/util/expr_util.cpp

Lines changed: 1 addition & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -68,33 +68,7 @@ exprt make_binary(const exprt &expr)
6868

6969
with_exprt make_with_expr(const update_exprt &src)
7070
{
71-
const exprt::operandst &designator=src.designator();
72-
PRECONDITION(!designator.empty());
73-
74-
with_exprt result{exprt{}, exprt{}, exprt{}};
75-
exprt *dest=&result;
76-
77-
for(const auto &expr : designator)
78-
{
79-
with_exprt tmp{exprt{}, exprt{}, exprt{}};
80-
81-
if(expr.id() == ID_index_designator)
82-
{
83-
tmp.where() = to_index_designator(expr).index();
84-
}
85-
else if(expr.id() == ID_member_designator)
86-
{
87-
// irep_idt component_name=
88-
// to_member_designator(*it).get_component_name();
89-
}
90-
else
91-
UNREACHABLE;
92-
93-
*dest=tmp;
94-
dest=&to_with_expr(*dest).new_value();
95-
}
96-
97-
return result;
71+
return src.make_with_expr();
9872
}
9973

10074
exprt is_not_zero(

src/util/expr_util.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ bool is_assignable(const exprt &);
4040
exprt make_binary(const exprt &);
4141

4242
/// converts an update expr into a (possibly nested) with expression
43+
DEPRECATED(SINCE(2024, 9, 10, "use update_exprt::make_with_expr() instead"))
4344
with_exprt make_with_expr(const update_exprt &);
4445

4546
/// converts a scalar/float expression to C/C++ Booleans

src/util/std_expr.cpp

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -174,6 +174,37 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
174174
}
175175
}
176176

177+
with_exprt update_exprt::make_with_expr() const
178+
{
179+
const exprt::operandst &designators = designator();
180+
PRECONDITION(!designators.empty());
181+
182+
with_exprt result{exprt{}, exprt{}, exprt{}};
183+
exprt *dest = &result;
184+
185+
for(const auto &expr : designators)
186+
{
187+
with_exprt tmp{exprt{}, exprt{}, exprt{}};
188+
189+
if(expr.id() == ID_index_designator)
190+
{
191+
tmp.where() = to_index_designator(expr).index();
192+
}
193+
else if(expr.id() == ID_member_designator)
194+
{
195+
// irep_idt component_name=
196+
// to_member_designator(*it).get_component_name();
197+
}
198+
else
199+
UNREACHABLE;
200+
201+
*dest = tmp;
202+
dest = &to_with_expr(*dest).new_value();
203+
}
204+
205+
return result;
206+
}
207+
177208
exprt binding_exprt::instantiate(const operandst &values) const
178209
{
179210
// number of values must match the number of bound variables

src/util/std_expr.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2698,6 +2698,9 @@ class update_exprt : public ternary_exprt
26982698
return op2();
26992699
}
27002700

2701+
/// converts an update expr into a (possibly nested) with expression
2702+
with_exprt make_with_expr() const;
2703+
27012704
static void check(
27022705
const exprt &expr,
27032706
const validation_modet vm = validation_modet::INVARIANT)

0 commit comments

Comments
 (0)