Skip to content

Commit

Permalink
Move make_with_expr to update_exprt
Browse files Browse the repository at this point in the history
This will eventually remove one of the functions from the expr_util
translation unit, which is supposed to be deprecated.
  • Loading branch information
tautschnig committed Sep 13, 2024
1 parent dc8793c commit 1aa2d83
Show file tree
Hide file tree
Showing 4 changed files with 36 additions and 27 deletions.
28 changes: 1 addition & 27 deletions src/util/expr_util.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -68,33 +68,7 @@ exprt make_binary(const exprt &expr)

with_exprt make_with_expr(const update_exprt &src)
{
const exprt::operandst &designator=src.designator();
PRECONDITION(!designator.empty());

with_exprt result{exprt{}, exprt{}, exprt{}};
exprt *dest=&result;

for(const auto &expr : designator)
{
with_exprt tmp{exprt{}, exprt{}, exprt{}};

if(expr.id() == ID_index_designator)
{
tmp.where() = to_index_designator(expr).index();
}
else if(expr.id() == ID_member_designator)
{
// irep_idt component_name=
// to_member_designator(*it).get_component_name();
}
else
UNREACHABLE;

*dest=tmp;
dest=&to_with_expr(*dest).new_value();
}

return result;
return src.make_with_expr();

Check warning on line 71 in src/util/expr_util.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/expr_util.cpp#L71

Added line #L71 was not covered by tests
}

exprt is_not_zero(
Expand Down
1 change: 1 addition & 0 deletions src/util/expr_util.h
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ bool is_assignable(const exprt &);
exprt make_binary(const exprt &);

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

/// converts a scalar/float expression to C/C++ Booleans
Expand Down
31 changes: 31 additions & 0 deletions src/util/std_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,37 @@ void let_exprt::validate(const exprt &expr, const validation_modet vm)
}
}

with_exprt update_exprt::make_with_expr() const

Check warning on line 194 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L194

Added line #L194 was not covered by tests
{
const exprt::operandst &designators = designator();
PRECONDITION(!designators.empty());

Check warning on line 197 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L196-L197

Added lines #L196 - L197 were not covered by tests

with_exprt result{exprt{}, exprt{}, exprt{}};
exprt *dest = &result;

Check warning on line 200 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L199-L200

Added lines #L199 - L200 were not covered by tests

for(const auto &expr : designators)
{
with_exprt tmp{exprt{}, exprt{}, exprt{}};

Check warning on line 204 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L204

Added line #L204 was not covered by tests

if(expr.id() == ID_index_designator)
{
tmp.where() = to_index_designator(expr).index();

Check warning on line 208 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L208

Added line #L208 was not covered by tests
}
else if(expr.id() == ID_member_designator)

Check warning on line 210 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L210

Added line #L210 was not covered by tests
{
// irep_idt component_name=
// to_member_designator(*it).get_component_name();
}
else
UNREACHABLE;

Check warning on line 216 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L216

Added line #L216 was not covered by tests

*dest = tmp;
dest = &to_with_expr(*dest).new_value();

Check warning on line 219 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L218-L219

Added lines #L218 - L219 were not covered by tests
}

return result;

Check warning on line 222 in src/util/std_expr.cpp

View check run for this annotation

Codecov / codecov/patch

src/util/std_expr.cpp#L222

Added line #L222 was not covered by tests
}

exprt binding_exprt::instantiate(const operandst &values) const
{
// number of values must match the number of bound variables
Expand Down
3 changes: 3 additions & 0 deletions src/util/std_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -2698,6 +2698,9 @@ class update_exprt : public ternary_exprt
return op2();
}

/// converts an update expr into a (possibly nested) with expression
with_exprt make_with_expr() const;

static void check(
const exprt &expr,
const validation_modet vm = validation_modet::INVARIANT)
Expand Down

0 comments on commit 1aa2d83

Please sign in to comment.