diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index a5cf83a86a9..4a89216ea2f 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -711,14 +711,14 @@ exprt assume_eq_unbounded( const left_and_right_valuest &operands, const namespacet &ns) { - if(operands.left->is_top() && is_lvalue(operands.lhs)) + if(operands.left->is_top() && is_assignable(operands.lhs)) { // TOP == x auto constrained = std::make_shared( operands.right_interval(), env, ns); prune_assign(env, operands.left, operands.lhs, constrained, ns); } - if(operands.right->is_top() && is_lvalue(operands.rhs)) + if(operands.right->is_top() && is_assignable(operands.rhs)) { // x == TOP auto constrained = std::make_shared( @@ -746,9 +746,9 @@ exprt assume_eq( if(meet->is_bottom()) return false_exprt(); - if(is_lvalue(operands.lhs)) + if(is_assignable(operands.lhs)) prune_assign(env, operands.left, operands.lhs, meet, ns); - if(is_lvalue(operands.rhs)) + if(is_assignable(operands.rhs)) prune_assign(env, operands.right, operands.rhs, meet, ns); return true_exprt(); } @@ -781,7 +781,7 @@ exprt assume_less_than_unbounded( const left_and_right_valuest &operands, const namespacet &ns) { - if(operands.left->is_top() && is_lvalue(operands.lhs)) + if(operands.left->is_top() && is_assignable(operands.lhs)) { // TOP < x, so prune range is min->right.upper auto pruned_expr = constant_interval_exprt( @@ -792,7 +792,7 @@ exprt assume_less_than_unbounded( std::make_shared(pruned_expr, env, ns); prune_assign(env, operands.left, operands.lhs, constrained, ns); } - if(operands.right->is_top() && is_lvalue(operands.rhs)) + if(operands.right->is_top() && is_assignable(operands.rhs)) { // x < TOP, so prune range is left.lower->max auto pruned_expr = constant_interval_exprt( @@ -830,7 +830,7 @@ exprt assume_less_than( auto result = env.eval(reduced_le_expr, ns)->to_constant(); if(result.is_true()) { - if(is_lvalue(operands.lhs)) + if(is_assignable(operands.lhs)) { auto pruned_upper = constant_interval_exprt::get_min( left_interval.get_upper(), right_upper); @@ -838,7 +838,7 @@ exprt assume_less_than( as_value(operands.left)->constrain(left_lower, pruned_upper); prune_assign(env, operands.left, operands.lhs, constrained, ns); } - if(is_lvalue(operands.rhs)) + if(is_assignable(operands.rhs)) { auto pruned_lower = constant_interval_exprt::get_max( left_lower, right_interval.get_lower()); diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 404f4a4a88e..9fedaa6d136 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -597,7 +597,7 @@ exprt make_va_list(const exprt &expr) if(result.id() == ID_address_of) { const auto &address_of_expr = to_address_of_expr(result); - if(is_lvalue(address_of_expr.object())) + if(is_assignable(address_of_expr.object())) result = address_of_expr.object(); } @@ -1156,7 +1156,7 @@ void goto_convertt::do_function_call_symbol( exprt dest_expr=make_va_list(arguments[0]); const typecast_exprt src_expr(arguments[1], dest_expr.type()); - if(!is_lvalue(dest_expr)) + if(!is_assignable(dest_expr)) { error().source_location=dest_expr.find_source_location(); error() << "va_copy argument expected to be lvalue" << eom; @@ -1179,7 +1179,7 @@ void goto_convertt::do_function_call_symbol( exprt dest_expr=make_va_list(arguments[0]); - if(!is_lvalue(dest_expr)) + if(!is_assignable(dest_expr)) { error().source_location=dest_expr.find_source_location(); error() << "va_start argument expected to be lvalue" << eom; @@ -1214,7 +1214,7 @@ void goto_convertt::do_function_call_symbol( exprt dest_expr=make_va_list(arguments[0]); - if(!is_lvalue(dest_expr)) + if(!is_assignable(dest_expr)) { error().source_location=dest_expr.find_source_location(); error() << "va_end argument expected to be lvalue" << eom; diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 9ced8646b33..d88065fa280 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -18,12 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_expr.h" #include "std_expr.h" -bool is_lvalue(const exprt &expr) +bool is_assignable(const exprt &expr) { if(expr.id() == ID_index) - return is_lvalue(to_index_expr(expr).array()); + return is_assignable(to_index_expr(expr).array()); else if(expr.id() == ID_member) - return is_lvalue(to_member_expr(expr).compound()); + return is_assignable(to_member_expr(expr).compound()); else if(expr.id() == ID_dereference) return true; else if(expr.id() == ID_symbol) @@ -31,6 +31,7 @@ bool is_lvalue(const exprt &expr) else return false; } + exprt make_binary(const exprt &expr) { const exprt::operandst &operands=expr.operands(); diff --git a/src/util/expr_util.h b/src/util/expr_util.h index 737d265ba05..e77ed4deb87 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -29,8 +29,12 @@ class if_exprt; class typet; class namespacet; -/// Returns true iff the argument is (syntactically) an lvalue. -bool is_lvalue(const exprt &expr); +/// Returns true iff the argument is one of the following: +/// * a symbol +/// * a dereference +/// * an array element +/// * a struct member +bool is_assignable(const exprt &); /// splits an expression with >=3 operands into nested binary expressions exprt make_binary(const exprt &); diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index e6d6ee427ee..55a5ce39944 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -335,7 +335,7 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr( if(unchecked_replace_symbolt::replace_symbol_expr(s_copy)) return true; - if(require_lvalue && !is_lvalue(s_copy)) + if(require_lvalue && !is_assignable(s_copy)) return true; // Note s_copy is no longer a symbol_exprt due to the replace operation,