Skip to content

Commit dbee266

Browse files
committed
Symex rename functions: use NODISCARD
These used to have side-effects on their parameters, and will still compile if used that way, so let's use NODISCARD to enforce that their new return value is consulted when necessary.
1 parent a999fd6 commit dbee266

File tree

1 file changed

+7
-5
lines changed

1 file changed

+7
-5
lines changed

src/goto-symex/goto_symex_state.h

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,12 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include <analyses/guard.h>
2020

21+
#include <goto-programs/goto_function.h>
2122
#include <util/invariant.h>
22-
#include <util/std_expr.h>
23-
#include <util/ssa_expr.h>
2423
#include <util/make_unique.h>
25-
#include <goto-programs/goto_function.h>
24+
#include <util/nodiscard.h>
25+
#include <util/ssa_expr.h>
26+
#include <util/std_expr.h>
2627

2728
#include "call_stack.h"
2829
#include "field_sensitivity.h"
@@ -97,12 +98,13 @@ class goto_symex_statet final : public goto_statet
9798
/// A full explanation of SSA (which is why we do this renaming) is in
9899
/// the SSA section of background-concepts.md.
99100
template <levelt level = L2>
100-
renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
101+
NODISCARD renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
101102

102103
/// Version of rename which is specialized for SSA exprt.
103104
/// Implementation only exists for level L0 and L1.
104105
template <levelt level>
105-
renamedt<ssa_exprt, level> rename_ssa(ssa_exprt ssa, const namespacet &ns);
106+
NODISCARD renamedt<ssa_exprt, level>
107+
rename_ssa(ssa_exprt ssa, const namespacet &ns);
106108

107109
template <levelt level = L2>
108110
void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);

0 commit comments

Comments
 (0)