Skip to content

Commit 8e15bbb

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 401a46c commit 8e15bbb

File tree

2 files changed

+9
-1
lines changed

2 files changed

+9
-1
lines changed

src/util/replace_symbol.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "replace_symbol.h"
1010

11+
#include "expr_util.h"
1112
#include "invariant.h"
1213
#include "std_expr.h"
1314
#include "std_types.h"
@@ -340,7 +341,7 @@ bool address_of_aware_replace_symbolt::replace_symbol_expr(
340341

341342
const exprt &e = it->second;
342343

343-
if(require_lvalue && e.is_constant()) // Would give non l-value.
344+
if(require_lvalue && !is_lvalue(e))
344345
return true;
345346

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

unit/util/replace_symbol.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,13 @@ TEST_CASE("Lvalue only", "[core][util][replace_symbol]")
7171
to_index_expr(to_address_of_expr(binary.op1()).object());
7272
REQUIRE(to_array_type(index_expr.array().type()).size() == c);
7373
REQUIRE(index_expr.index() == c);
74+
75+
address_of_exprt address_of(s1);
76+
r.erase("a");
77+
r.insert("a", address_of);
78+
79+
REQUIRE(r.replace(binary) == true);
80+
REQUIRE(binary.op0() == address_of_exprt(s1));
7481
}
7582

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

0 commit comments

Comments
 (0)