Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move make_with_expr to update_exprt #8448

Merged
merged 1 commit into from
Sep 13, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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 @@

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 @@
}
}

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
Loading