From 92fc16d9cddd4cf8d70393d478044144155c5ed0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 May 2018 11:41:56 +0000 Subject: [PATCH] replace_symbolt must consider all non-lvalues Literal constants are not the only ones: for example, address-of isn't an lvalue either. Make is_lvalue globally available to accomplish this. --- src/util/replace_symbol.cpp | 3 ++- unit/util/replace_symbol.cpp | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 55d9bd46ee4..58f9d839f6c 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "replace_symbol.h" +#include "expr_util.h" #include "invariant.h" #include "std_expr.h" #include "std_types.h" @@ -340,7 +341,7 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr( const exprt &e = it->second; - if(require_lvalue && e.is_constant()) // Would give non l-value. + if(require_lvalue && !is_lvalue(e)) return true; static_cast(s) = e; diff --git a/unit/util/replace_symbol.cpp b/unit/util/replace_symbol.cpp index 6ef30235bda..d983e25398e 100644 --- a/unit/util/replace_symbol.cpp +++ b/unit/util/replace_symbol.cpp @@ -71,6 +71,13 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]") to_index_expr(to_address_of_expr(binary.op1()).object()); REQUIRE(to_array_type(index_expr.array().type()).size() == c); REQUIRE(index_expr.index() == c); + + address_of_exprt address_of(s1); + r.erase("a"); + r.insert(s1, address_of); + + REQUIRE(r.replace(binary) == true); + REQUIRE(binary.op0() == address_of_exprt(s1)); } TEST_CASE("Replace always", "[core][util][replace_symbol]")