From 28d6848ff253b16e1dade21bfadaf2f6e6ad1b2e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 21 Jun 2019 09:18:41 +0100 Subject: [PATCH] Fix discarding of field_sensitivity::apply result Not using the result is certainly a bug, so we mark it as NODISCARD. --- src/goto-symex/field_sensitivity.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 1503a71e8cc..3beff934804 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -10,6 +10,7 @@ Author: Michael Tautschnig #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H #include +#include class exprt; class ssa_exprt; @@ -116,6 +117,7 @@ class field_sensitivityt /// \param expr: an expression to be (recursively) transformed. /// \param write: set to true if the expression is to be used as an lvalue. /// \return the transformed expression + NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const;