Skip to content

Commit 538b735

Browse files
Fix discarding of field_sensitivity::apply result
Not using the result is certainly a bug, so we mark it as NODISCARD.
1 parent 44d4e46 commit 538b735

File tree

2 files changed

+5
-1
lines changed

2 files changed

+5
-1
lines changed

src/goto-symex/field_sensitivity.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@ Author: Michael Tautschnig
99
#ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
1010
#define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
1111

12+
#include <util/nodiscard.h>
13+
1214
class exprt;
1315
class ssa_exprt;
1416
class namespacet;
@@ -82,6 +84,7 @@ class field_sensitivityt
8284
/// \param expr: an expression to be (recursively) transformed.
8385
/// \param write: set to true if the expression is to be used as an lvalue.
8486
/// \return the transformed expression
87+
NODISCARD
8588
exprt
8689
apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
8790
const;

src/goto-symex/symex_assign.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -259,7 +259,8 @@ static assignmentt rewrite_with_to_field_symbols(
259259
update.new_value().type());
260260
}
261261

262-
state.field_sensitivity.apply(ns, state, field_sensitive_lhs, true);
262+
field_sensitive_lhs = state.field_sensitivity.apply(
263+
ns, state, std::move(field_sensitive_lhs), true);
263264

264265
if(field_sensitive_lhs.id() != ID_symbol)
265266
break;

0 commit comments

Comments
 (0)