Skip to content

Commit

Permalink
Merge pull request #8448 from tautschnig/move-make_with_expr
Browse files Browse the repository at this point in the history
Move make_with_expr to update_exprt
  • Loading branch information
tautschnig authored Sep 13, 2024
2 parents e08b025 + 1aa2d83 commit 2212cd6
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();
}

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
{
const exprt::operandst &designators = designator();
PRECONDITION(!designators.empty());

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

for(const auto &expr : designators)
{
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;
}

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 2212cd6

Please sign in to comment.