Skip to content

Commit e82eb7d

Browse files
committed
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.
1 parent 7f31123 commit e82eb7d

File tree

2 files changed

+9
-1
lines changed

2 files changed

+9
-1
lines changed

src/util/replace_symbol.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "replace_symbol.h"
1010

1111
#include "base_type.h"
12+
#include "expr_util.h"
1213
#include "invariant.h"
1314
#include "namespace.h"
1415
#include "std_types.h"
@@ -420,7 +421,7 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr(
420421

421422
const exprt &e = it->second;
422423

423-
if(require_lvalue && e.is_constant()) // Would give non l-value.
424+
if(require_lvalue && !is_lvalue(e))
424425
return true;
425426

426427
static_cast<exprt &>(s) = e;

unit/util/replace_symbol.cpp

+7
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,13 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
8282
to_index_expr(to_address_of_expr(binary.op1()).object());
8383
REQUIRE(to_array_type(index_expr.array().type()).size() == c);
8484
REQUIRE(index_expr.index() == c);
85+
86+
address_of_exprt address_of(s1);
87+
r.erase("a");
88+
r.insert("a", address_of);
89+
90+
REQUIRE(r.replace(binary) == true);
91+
REQUIRE(binary.op0() == address_of_exprt(s1));
8592
}
8693

8794
TEST_CASE("Replace always", "[core][util][replace_symbol]")

0 commit comments

Comments
 (0)