Merge pull request #2200 from tautschnig/lvalue-prop

Fix replace_symbolt for non-lvalues

Author: tautschnig

src/util/replace_symbol.cpp

@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "replace_symbol.h"
 
+#include "expr_util.h"
 #include "invariant.h"
 #include "std_expr.h"
 #include "std_types.h"
@@ -322,7 +323,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<exprt &>(s) = e;

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]")