Use the C++17 standard [[nodiscard]] attribute directly

jbmc/src/java_bytecode/java_utils.cpp

@@ -577,7 +577,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
   symbol.type.set(ID_C_class, declaring_class);
 }
 
-NODISCARD optionalt<std::string>
+[[nodiscard]] optionalt<std::string>
 class_name_from_method_name(const std::string &method_name)
 {
   const auto signature_index = method_name.rfind(":");

jbmc/src/java_bytecode/java_utils.h

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <unordered_set>
 
-#include <util/nodiscard.h>
 #include <util/pointer_expr.h>
 
 #include <goto-programs/resolve_inherited_component.h>
@@ -185,7 +184,7 @@ void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
 /// Get JVM type name of the class in which \p method_name is defined.
 /// Returns an empty optional if the class name cannot be retrieved,
 /// e.g. method_name is an internal function.
-NODISCARD optionalt<std::string>
+[[nodiscard]] optionalt<std::string>
 class_name_from_method_name(const std::string &method_name);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

src/cprover/bv_pointers_wide.h

@@ -9,7 +9,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_CPROVER_BV_POINTERS_WIDE_H
 #define CPROVER_CPROVER_BV_POINTERS_WIDE_H
 
-#include <util/nodiscard.h>
 #include <util/pointer_expr.h>
 
 #include <solvers/flattening/boolbv.h>
@@ -51,13 +50,12 @@ class bv_pointers_widet : public boolbvt
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
-  NODISCARD
-  bvt encode(const mp_integer &object, const pointer_typet &) const;
+  [[nodiscard]] bvt
+  encode(const mp_integer &object, const pointer_typet &) const;
 
   virtual bvt convert_pointer_type(const exprt &);
 
-  NODISCARD
-  virtual bvt add_addr(const exprt &);
+  [[nodiscard]] virtual bvt add_addr(const exprt &);
 
   // overloading
   literalt convert_rest(const exprt &) override;
@@ -66,19 +64,16 @@ class bv_pointers_widet : public boolbvt
   exprt
   bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
 
-  NODISCARD
-  optionalt<bvt> convert_address_of_rec(const exprt &);
+  [[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
 
-  NODISCARD
-  bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt
+  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,

src/goto-programs/link_goto_model.h

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 #define CPROVER_GOTO_PROGRAMS_LINK_GOTO_MODEL_H
 
-#include <util/nodiscard.h>
 #include <util/replace_symbol.h>
 
 class goto_modelt;
@@ -23,7 +22,7 @@ class message_handlert;
 /// which need to be applied using \ref finalize_linking.
 /// \return nullopt if linking fails, else a (possibly empty) collection of
 ///   replacements to be applied.
-NODISCARD optionalt<replace_symbolt::expr_mapt>
+[[nodiscard]] optionalt<replace_symbolt::expr_mapt>
 link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &);
 
 /// Apply \p type_updates to \p dest, where \p type_updates were constructed

src/goto-symex/field_sensitivity.h

@@ -9,7 +9,6 @@ Author: Michael Tautschnig
 #ifndef CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 #define CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H
 
-#include <util/nodiscard.h>
 #include <util/ssa_expr.h>
 
 class namespacet;
@@ -158,13 +157,11 @@ 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
+  [[nodiscard]] exprt
   apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
     const;
   /// \copydoc apply(const namespacet&,goto_symex_statet&,exprt,bool) const
-  NODISCARD
-  exprt apply(
+  [[nodiscard]] exprt apply(
     const namespacet &ns,
     goto_symex_statet &state,
     ssa_exprt expr,
@@ -182,8 +179,7 @@ class field_sensitivityt
   /// \return Expanded expression; for example, for a \p ssa_expr of some struct
   ///   type, a `struct_exprt` with each component now being an SSA expression
   ///   is built.
-  NODISCARD
-  exprt get_fields(
+  [[nodiscard]] exprt get_fields(
     const namespacet &ns,
     goto_symex_statet &state,
     const ssa_exprt &ssa_expr,
@@ -198,8 +194,8 @@ class field_sensitivityt
   ///   (`true`)
   /// \return False, if and only if, \p expr would be a single field-sensitive
   /// SSA expression.
-  NODISCARD
-  bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
+  [[nodiscard]] bool
+  is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const;
 
 private:
   const std::size_t max_field_sensitivity_array_size;
@@ -214,8 +210,7 @@ class field_sensitivityt
     symex_targett &target,
     bool allow_pointer_unsoundness) const;
 
-  NODISCARD
-  exprt simplify_opt(exprt e, const namespacet &ns) const;
+  [[nodiscard]] exprt simplify_opt(exprt e, const namespacet &ns) const;
 };
 
 #endif // CPROVER_GOTO_SYMEX_FIELD_SENSITIVITY_H

src/goto-symex/goto_symex.h

@@ -112,8 +112,7 @@ class goto_symext
   /// \param fields The shadow memory field declarations
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet symex_from_entry_point_of(
+  [[nodiscard]] virtual symbol_tablet symex_from_entry_point_of(
     const get_goto_functiont &get_goto_function,
     const shadow_memory_field_definitionst &fields);
 
@@ -138,8 +137,7 @@ class goto_symext
   /// \param saved_equation: The equation as previously built up
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet resume_symex_from_saved_state(
+  [[nodiscard]] virtual symbol_tablet resume_symex_from_saved_state(
     const get_goto_functiont &get_goto_function,
     const statet &saved_state,
     symex_target_equationt *saved_equation);
@@ -156,8 +154,7 @@ class goto_symext
   ///   execute
   /// \return A symbol table holding the symbols added during symbolic
   ///   execution.
-  NODISCARD
-  virtual symbol_tablet
+  [[nodiscard]] virtual symbol_tablet
   symex_with_state(statet &state, const get_goto_functiont &get_goto_functions);
 
   /// \brief Set when states are pushed onto the workqueue

src/goto-symex/goto_symex_state.h

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H
 
 #include <util/invariant.h>
-#include <util/nodiscard.h>
 #include <util/ssa_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
@@ -98,21 +97,21 @@ class goto_symex_statet final : public goto_statet
   /// A full explanation of SSA (which is why we do this renaming) is in
   /// the SSA section of background-concepts.md.
   template <levelt level = L2>
-  NODISCARD renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
+  [[nodiscard]] renamedt<exprt, level> rename(exprt expr, const namespacet &ns);
 
   /// Version of rename which is specialized for SSA exprt.
   /// Implementation only exists for level L0 and L1.
   template <levelt level>
-  NODISCARD renamedt<ssa_exprt, level>
+  [[nodiscard]] renamedt<ssa_exprt, level>
   rename_ssa(ssa_exprt ssa, const namespacet &ns);
 
   template <levelt level = L2>
   void rename(typet &type, const irep_idt &l1_identifier, const namespacet &ns);
 
-  NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
+  [[nodiscard]] exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns);
 
   /// \return lhs renamed to level 2
-  NODISCARD renamedt<ssa_exprt, L2> assignment(
+  [[nodiscard]] renamedt<ssa_exprt, L2> assignment(
     ssa_exprt lhs,    // L0/L1
     const exprt &rhs, // L2
     const namespacet &ns,
@@ -130,7 +129,7 @@ class goto_symex_statet final : public goto_statet
 
   /// Update values up to \c level.
   template <levelt level>
-  NODISCARD renamedt<ssa_exprt, level>
+  [[nodiscard]] renamedt<ssa_exprt, level>
   set_indices(ssa_exprt expr, const namespacet &ns);
 
   // this maps L1 names to (L2) types

src/goto-symex/symex_clean_expr.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/expr_iterator.h>
-#include <util/nodiscard.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
 
@@ -228,7 +227,7 @@ void goto_symext::lift_lets(statet &state, exprt &rhs)
   }
 }
 
-NODISCARD exprt
+[[nodiscard]] exprt
 goto_symext::clean_expr(exprt expr, statet &state, const bool write)
 {
   replace_nondet(expr, path_storage.build_symex_nondet);

src/solvers/flattening/bv_pointers.h

@@ -10,8 +10,6 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 
-#include <util/nodiscard.h>
-
 #include "boolbv.h"
 #include "pointer_logic.h"
 
@@ -39,13 +37,12 @@ class bv_pointerst:public boolbvt
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
-  NODISCARD
-  bvt encode(const mp_integer &object, const pointer_typet &) const;
+  [[nodiscard]] bvt
+  encode(const mp_integer &object, const pointer_typet &) const;
 
   virtual bvt convert_pointer_type(const exprt &);
 
-  NODISCARD
-  virtual bvt add_addr(const exprt &);
+  [[nodiscard]] virtual bvt add_addr(const exprt &);
 
   // overloading
   literalt convert_rest(const exprt &) override;
@@ -54,25 +51,21 @@ class bv_pointerst:public boolbvt
   exprt
   bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override;
 
-  NODISCARD
-  optionalt<bvt> convert_address_of_rec(const exprt &);
+  [[nodiscard]] optionalt<bvt> convert_address_of_rec(const exprt &);
 
-  NODISCARD
-  bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt
+  offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &);
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &type,
     const bvt &bv,
     const exprt &factor,
     const exprt &index);
-  NODISCARD
-  bvt offset_arithmetic(
+  [[nodiscard]] bvt offset_arithmetic(
     const pointer_typet &,
     const bvt &,
     const mp_integer &factor,

src/solvers/flattening/bv_utils.h

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_FLATTENING_BV_UTILS_H
 
 #include <util/mp_arith.h>
-#include <util/nodiscard.h>
 
 #include <solvers/prop/prop.h>
 
@@ -224,16 +223,16 @@ class bv_utilst
 
   /// Return the sum and carry-out when adding \p op0 and \p op1 under initial
   /// carry \p carry_in.
-  NODISCARD std::pair<bvt, literalt>
+  [[nodiscard]] std::pair<bvt, literalt>
   adder(const bvt &op0, const bvt &op1, literalt carry_in);
 
-  NODISCARD bvt adder_no_overflow(
+  [[nodiscard]] bvt adder_no_overflow(
     const bvt &op0,
     const bvt &op1,
     bool subtract,
     representationt rep);
 
-  NODISCARD bvt adder_no_overflow(const bvt &op0, const bvt &op1);
+  [[nodiscard]] bvt adder_no_overflow(const bvt &op0, const bvt &op1);
 
   bvt unsigned_multiplier_no_overflow(
     const bvt &op0, const bvt &op1);

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -6,7 +6,6 @@
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/namespace.h>
-#include <util/nodiscard.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -663,8 +662,8 @@ void smt2_incremental_decision_proceduret::pop()
   UNIMPLEMENTED_FEATURE("`pop`.");
 }
 
-NODISCARD
-static decision_proceduret::resultt lookup_decision_procedure_result(
+[[nodiscard]] static decision_proceduret::resultt
+lookup_decision_procedure_result(
   const smt_check_sat_response_kindt &response_kind)
 {
   if(response_kind.cast<smt_sat_responset>())

src/solvers/smt2_incremental/smt_response_validation.h

@@ -3,12 +3,10 @@
 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_RESPONSE_VALIDATION_H
 
-#include <util/nodiscard.h>
-
 #include <solvers/smt2_incremental/ast/smt_responses.h> // IWYU pragma: keep
 #include <solvers/smt2_incremental/response_or_error.h>
 
-NODISCARD response_or_errort<smt_responset> validate_smt_response(
+[[nodiscard]] response_or_errort<smt_responset> validate_smt_response(
   const irept &parse_tree,
   const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table);
 

src/solvers/strings/string_dependencies.h

@@ -14,8 +14,6 @@ Author: Diffblue Ltd.
 
 #include <memory>
 
-#include <util/nodiscard.h>
-
 #include "string_builtin_function.h"
 
 /// Keep track of dependencies between strings.
@@ -115,7 +113,7 @@ class string_dependenciest
   /// For all builtin call on which a test (or an unsupported buitin)
   /// result depends, add the corresponding constraints. For the other builtin
   /// only add constraints on the length.
-  NODISCARD string_constraintst add_constraints(
+  [[nodiscard]] string_constraintst add_constraints(
     string_constraint_generatort &generatort,
     message_handlert &message_handler);
 

src/util/interval_union.h

@@ -14,7 +14,6 @@ Author: Diffblue Limited
 
 #include <util/interval_template.h>
 #include <util/mp_arith.h>
-#include <util/nodiscard.h>
 #include <util/optional.h>
 #include <vector>
 
@@ -44,12 +43,12 @@ class interval_uniont
 
   /// Return a new interval_uniontt object representing the set of intergers in
   /// the intersection of this object and \p other.
-  NODISCARD interval_uniont
+  [[nodiscard]] interval_uniont
   make_intersection(const interval_uniont &other) const;
 
   /// Return a new interval_uniontt object representing the set of intergers in
   /// the union of this object and \p other.
-  NODISCARD interval_uniont make_union(const interval_uniont &other) const;
+  [[nodiscard]] interval_uniont make_union(const interval_uniont &other) const;
 
   bool is_empty() const;