Skip to content

Commit 44e53c8

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #8036 from thomasspriggs/tas/nonodiscard
Use the C++17 standard `[[nodiscard]]` attribute directly
2 parents ee33bc8 + 0857208 commit 44e53c8

19 files changed

+125
-180
lines changed

‎jbmc/src/java_bytecode/java_utils.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -577,7 +577,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
577577
symbol.type.set(ID_C_class, declaring_class);
578578
}
579579

580-
NODISCARD optionalt<std::string>
580+
[[nodiscard]] optionalt<std::string>
581581
class_name_from_method_name(const std::string &method_name)
582582
{
583583
const auto signature_index = method_name.rfind(":");

‎jbmc/src/java_bytecode/java_utils.h‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
1111

1212
#include <unordered_set>
1313

14-
#include <util/nodiscard.h>
1514
#include <util/pointer_expr.h>
1615

1716
#include <goto-programs/resolve_inherited_component.h>
@@ -185,7 +184,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
185184
/// Get JVM type name of the class in which \p method_name is defined.
186185
/// Returns an empty optional if the class name cannot be retrieved,
187186
/// e.g. method_name is an internal function.
188-
NODISCARD optionalt<std::string>
187+
[[nodiscard]] optionalt<std::string>
189188
class_name_from_method_name(const std::string &method_name);
190189

191190
#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

‎src/cprover/bv_pointers_wide.h‎

Lines changed: 8 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ Author: Daniel Kroening, kroening@kroening.com
99
#ifndef CPROVER_CPROVER_BV_POINTERS_WIDE_H
1010
#define CPROVER_CPROVER_BV_POINTERS_WIDE_H
1111

12-
#include <util/nodiscard.h>
1312
#include <util/pointer_expr.h>
1413

1514
#include <solvers/flattening/boolbv.h>
@@ -51,13 +50,12 @@ class bv_pointers_widet : public boolbvt
5150
// NOLINTNEXTLINE(readability/identifiers)
5251
typedef boolbvt SUB;
5352

54-
NODISCARD
55-
bvt encode(const mp_integer &object, const pointer_typet &) const;
53+
[[nodiscard]] bvt
54+
encode(const mp_integer &object, const pointer_typet &) const;
5655

5756
virtual bvt convert_pointer_type(const exprt &);
5857

59-
NODISCARD
60-
virtual bvt add_addr(const exprt &);
58+
[[nodiscard]] virtual bvt add_addr(const exprt &);
6159

6260
// overloading
6361
literalt convert_rest(const exprt &) override;
@@ -66,19 +64,16 @@ class bv_pointers_widet : public boolbvt
6664
exprt
6765
bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
6866

69-
NODISCARD
70-
optionalt<bvt> convert_address_of_rec(const exprt &);
67+
[[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
7168

72-
NODISCARD
73-
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
74-
NODISCARD
75-
bvt offset_arithmetic(
69+
[[nodiscard]] bvt
70+
offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
71+
[[nodiscard]] bvt offset_arithmetic(
7672
const pointer_typet &,
7773
const bvt &,
7874
const mp_integer &factor,
7975
const exprt &index);
80-
NODISCARD
81-
bvt offset_arithmetic(
76+
[[nodiscard]] bvt offset_arithmetic(
8277
const pointer_typet &,
8378
const bvt &,
8479
const mp_integer &factor,

‎src/goto-programs/link_goto_model.h‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
1212
#ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
1313
#define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
1414

15-
#include <util/nodiscard.h>
1615
#include <util/replace_symbol.h>
1716

1817
class goto_modelt;
@@ -23,7 +22,7 @@ class message_handlert;
2322
/// which need to be applied using \ref finalize_linking.
2423
/// \return nullopt if linking fails, else a (possibly empty) collection of
2524
/// replacements to be applied.
26-
NODISCARD optionalt<replace_symbolt::expr_mapt>
25+
[[nodiscard]] optionalt<replace_symbolt::expr_mapt>
2726
link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
2827

2928
/// Apply \p type_updates to \p dest, where \p type_updates were constructed

‎src/goto-symex/field_sensitivity.h‎

Lines changed: 6 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ 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>
1312
#include <util/ssa_expr.h>
1413

1514
class namespacet;
@@ -158,13 +157,11 @@ class field_sensitivityt
158157
/// \param expr: an expression to be (recursively) transformed.
159158
/// \param write: set to true if the expression is to be used as an lvalue.
160159
/// \return the transformed expression
161-
NODISCARD
162-
exprt
160+
[[nodiscard]] exprt
163161
apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
164162
const;
165163
/// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
166-
NODISCARD
167-
exprt apply(
164+
[[nodiscard]] exprt apply(
168165
const namespacet &ns,
169166
goto_symex_statet &state,
170167
ssa_exprt expr,
@@ -182,8 +179,7 @@ class field_sensitivityt
182179
/// \return Expanded expression; for example, for a \p ssa_expr of some struct
183180
/// type, a `struct_exprt` with each component now being an SSA expression
184181
/// is built.
185-
NODISCARD
186-
exprt get_fields(
182+
[[nodiscard]] exprt get_fields(
187183
const namespacet &ns,
188184
goto_symex_statet &state,
189185
const ssa_exprt &ssa_expr,
@@ -198,8 +194,8 @@ class field_sensitivityt
198194
/// (`true`)
199195
/// \return False, if and only if, \p expr would be a single field-sensitive
200196
/// SSA expression.
201-
NODISCARD
202-
bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
197+
[[nodiscard]] bool
198+
is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
203199

204200
private:
205201
const std::size_t max_field_sensitivity_array_size;
@@ -214,8 +210,7 @@ class field_sensitivityt
214210
symex_targett &target,
215211
bool allow_pointer_unsoundness) const;
216212

217-
NODISCARD
218-
exprt simplify_opt(exprt e, const namespacet &ns) const;
213+
[[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
219214
};
220215

221216
#endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

‎src/goto-symex/goto_symex.h‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -112,8 +112,7 @@ class goto_symext
112112
/// \param fields The shadow memory field declarations
113113
/// \return A symbol table holding the symbols added during symbolic
114114
/// execution.
115-
NODISCARD
116-
virtual symbol_tablet symex_from_entry_point_of(
115+
[[nodiscard]] virtual symbol_tablet symex_from_entry_point_of(
117116
const get_goto_functiont &get_goto_function,
118117
const shadow_memory_field_definitionst &fields);
119118

@@ -138,8 +137,7 @@ class goto_symext
138137
/// \param saved_equation: The equation as previously built up
139138
/// \return A symbol table holding the symbols added during symbolic
140139
/// execution.
141-
NODISCARD
142-
virtual symbol_tablet resume_symex_from_saved_state(
140+
[[nodiscard]] virtual symbol_tablet resume_symex_from_saved_state(
143141
const get_goto_functiont &get_goto_function,
144142
const statet &saved_state,
145143
symex_target_equationt *saved_equation);
@@ -156,8 +154,7 @@ class goto_symext
156154
/// execute
157155
/// \return A symbol table holding the symbols added during symbolic
158156
/// execution.
159-
NODISCARD
160-
virtual symbol_tablet
157+
[[nodiscard]] virtual symbol_tablet
161158
symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
162159

163160
/// \brief Set when states are pushed onto the workqueue

‎src/goto-symex/goto_symex_state.h‎

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
1414

1515
#include <util/invariant.h>
16-
#include <util/nodiscard.h>
1716
#include <util/ssa_expr.h>
1817
#include <util/std_expr.h>
1918
#include <util/symbol_table.h>
@@ -98,21 +97,21 @@ class goto_symex_statet final : public goto_statet
9897
/// A full explanation of SSA (which is why we do this renaming) is in
9998
/// the SSA section of background-concepts.md.
10099
template <levelt level = L2>
101-
NODISCARD renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
100+
[[nodiscard]] renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
102101

103102
/// Version of rename which is specialized for SSA exprt.
104103
/// Implementation only exists for level L0 and L1.
105104
template <levelt level>
106-
NODISCARD renamedt<ssa_exprt, level>
105+
[[nodiscard]] renamedt<ssa_exprt, level>
107106
rename_ssa(ssa_exprt ssa, const namespacet &ns);
108107

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

112-
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
111+
[[nodiscard]] exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
113112

114113
/// \return lhs renamed to level 2
115-
NODISCARD renamedt<ssa_exprt, L2> assignment(
114+
[[nodiscard]] renamedt<ssa_exprt, L2> assignment(
116115
ssa_exprt lhs, // L0/L1
117116
const exprt &rhs, // L2
118117
const namespacet &ns,
@@ -130,7 +129,7 @@ class goto_symex_statet final : public goto_statet
130129

131130
/// Update values up to \c level.
132131
template <levelt level>
133-
NODISCARD renamedt<ssa_exprt, level>
132+
[[nodiscard]] renamedt<ssa_exprt, level>
134133
set_indices(ssa_exprt expr, const namespacet &ns);
135134

136135
// this maps L1 names to (L2) types

‎src/goto-symex/symex_clean_expr.cpp‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <util/byte_operators.h>
1616
#include <util/c_types.h>
1717
#include <util/expr_iterator.h>
18-
#include <util/nodiscard.h>
1918
#include <util/pointer_offset_size.h>
2019
#include <util/simplify_expr.h>
2120

@@ -228,7 +227,7 @@ void goto_symext::lift_lets(statet &state, exprt &rhs)
228227
}
229228
}
230229

231-
NODISCARD exprt
230+
[[nodiscard]] exprt
232231
goto_symext::clean_expr(exprt expr, statet &state, const bool write)
233232
{
234233
replace_nondet(expr, path_storage.build_symex_nondet);

‎src/solvers/flattening/bv_pointers.h‎

Lines changed: 9 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
1010
#ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
1111
#define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
1212

13-
#include <util/nodiscard.h>
14-
1513
#include "boolbv.h"
1614
#include "pointer_logic.h"
1715

@@ -39,13 +37,12 @@ class bv_pointerst:public boolbvt
3937
// NOLINTNEXTLINE(readability/identifiers)
4038
typedef boolbvt SUB;
4139

42-
NODISCARD
43-
bvt encode(const mp_integer &object, const pointer_typet &) const;
40+
[[nodiscard]] bvt
41+
encode(const mp_integer &object, const pointer_typet &) const;
4442

4543
virtual bvt convert_pointer_type(const exprt &);
4644

47-
NODISCARD
48-
virtual bvt add_addr(const exprt &);
45+
[[nodiscard]] virtual bvt add_addr(const exprt &);
4946

5047
// overloading
5148
literalt convert_rest(const exprt &) override;
@@ -54,25 +51,21 @@ class bv_pointerst:public boolbvt
5451
exprt
5552
bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
5653

57-
NODISCARD
58-
optionalt<bvt> convert_address_of_rec(const exprt &);
54+
[[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
5955

60-
NODISCARD
61-
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
62-
NODISCARD
63-
bvt offset_arithmetic(
56+
[[nodiscard]] bvt
57+
offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
58+
[[nodiscard]] bvt offset_arithmetic(
6459
const pointer_typet &,
6560
const bvt &,
6661
const mp_integer &factor,
6762
const exprt &index);
68-
NODISCARD
69-
bvt offset_arithmetic(
63+
[[nodiscard]] bvt offset_arithmetic(
7064
const pointer_typet &type,
7165
const bvt &bv,
7266
const exprt &factor,
7367
const exprt &index);
74-
NODISCARD
75-
bvt offset_arithmetic(
68+
[[nodiscard]] bvt offset_arithmetic(
7669
const pointer_typet &,
7770
const bvt &,
7871
const mp_integer &factor,

‎src/solvers/flattening/bv_utils.h‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
1111
#define CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
1212

1313
#include <util/mp_arith.h>
14-
#include <util/nodiscard.h>
1514

1615
#include <solvers/prop/prop.h>
1716

@@ -224,16 +223,16 @@ class bv_utilst
224223

225224
/// Return the sum and carry-out when adding \p op0 and \p op1 under initial
226225
/// carry \p carry_in.
227-
NODISCARD std::pair<bvt, literalt>
226+
[[nodiscard]] std::pair<bvt, literalt>
228227
adder(const bvt &op0, const bvt &op1, literalt carry_in);
229228

230-
NODISCARD bvt adder_no_overflow(
229+
[[nodiscard]] bvt adder_no_overflow(
231230
const bvt &op0,
232231
const bvt &op1,
233232
bool subtract,
234233
representationt rep);
235234

236-
NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1);
235+
[[nodiscard]] bvt adder_no_overflow(const bvt &op0, const bvt &op1);
237236

238237
bvt unsigned_multiplier_no_overflow(
239238
const bvt &op0, const bvt &op1);

0 commit comments

Comments
 (0)