diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index e272918c364..d393bc5c567 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -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( diff --git a/src/util/expr_util.h b/src/util/expr_util.h index eefe6903f37..fd0381cd704 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -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 diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 1da4141bd14..506298c26ce 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -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 diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e27e5b5f1e9..d9ca4f64bab 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -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)