From 4ee79af337590311ddf87afe6c717a5f11ab4d40 Mon Sep 17 00:00:00 2001 From: davedets Date: Fri, 31 Jul 2026 19:34:08 -0700 Subject: [PATCH] Disable "-Wnoctad-maybe-unsupported", add and fix "-Wdeprecated-copy-with-user-provided-copy". (#10332) This is another PR towards the goal of getting Z3 to compile cleanly when included via FetchContents into clang-tidy, which uses a pretty strict set of warnings. (2 more flags after this!) The first of these was -Wctad-maybe-unsupported. That has to do with "class template argument deduction" -- the flag requires template deduction guides to be explicitly provided if templated types are used in situations that requires argument deduction. This fired for various uses of templated types in the utils directory. I decided that this should be a case of if it ain't broke, don't fix it, and explicitly disabled the warning in the Z3 build (which will override the setting if the flag is enabled in a larger build including Z3, like clang). ----- The second flag has to do with the C++ "rule of 3". Here is Google's AI summary (inf_s_integer is a class in Z3 that triggered the warning): _This warning means your inf_s_integer class defines a custom copy assignment operator but lacks a user-defined copy constructor, which the C++ standard deprecates to encourage the "Rule of Three". To fix this, explicitly declare and = default the copy constructor in your class definition._ _...example of how to fix..._ _This updates your code to modern C++ standards, cleanly silencing the warning._ This seemed like a good standard to follow, and didn't require too many changes, so I propose them. --- cmake/compiler_warnings.cmake | 2 ++ src/ast/seq_decl_plugin.h | 1 + src/math/lp/dense_matrix.h | 1 + src/math/subpaving/subpaving_t.h | 4 +++- src/tactic/aig/aig.cpp | 1 + src/util/inf_s_integer.h | 1 + src/util/params.cpp | 3 ++- src/util/ref_buffer.h | 4 +++- 8 files changed, 14 insertions(+), 3 deletions(-) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index ebabc71dba..3b9ae912ef 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -28,6 +28,8 @@ set(CLANG_ONLY_WARNINGS "-Wimplicit-fallthrough" "-Wextra-semi" "-Wignored-qualifiers" + "-Wnoctad-maybe-unsupported" + "-Wdeprecated-copy-with-user-provided-copy" ) set(MSVC_WARNINGS "/W3") diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index bfe400c57e..8566173f2b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -458,6 +458,7 @@ public: Default constructor of invalid info. */ info() = default; + info(const info&) = default; /* Used for constructing either an invalid info that is only used to indicate uninitialized entry, or valid but unknown info value. diff --git a/src/math/lp/dense_matrix.h b/src/math/lp/dense_matrix.h index 2d9d6c2358..40bba66f97 100644 --- a/src/math/lp/dense_matrix.h +++ b/src/math/lp/dense_matrix.h @@ -45,6 +45,7 @@ public: unsigned m_n; // number of const vector m_values; dense_matrix(unsigned m, unsigned n); + dense_matrix(const dense_matrix &) = default; dense_matrix operator*=(matrix const & a) { SASSERT(column_count() == a.row_count()); diff --git a/src/math/subpaving/subpaving_t.h b/src/math/subpaving/subpaving_t.h index 3a6081f409..abc96df676 100644 --- a/src/math/subpaving/subpaving_t.h +++ b/src/math/subpaving/subpaving_t.h @@ -120,7 +120,9 @@ public: justification(justification const & source) { m_data = source.m_data; } explicit justification(clause * c) { m_data = TAG(void*, c, CLAUSE); } explicit justification(var x) { m_data = BOXTAGINT(void*, x, VAR_DEF); } - + + justification &operator=(justification const &) = default; + kind get_kind() const { return static_cast(GET_TAG(m_data)); } bool is_clause() const { return get_kind() == CLAUSE; } bool is_axiom() const { return get_kind() == AXIOM; } diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index a0b7d05382..fe72073410 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -32,6 +32,7 @@ class aig_lit { public: aig_lit(aig * n = nullptr):m_ref(n) {} aig_lit(aig_ref const & r):m_ref(static_cast(r.m_ref)) {} + aig_lit(const aig_lit &) = default; bool is_inverted() const { return (reinterpret_cast(m_ref) & static_cast(1)) == static_cast(1); } void invert() { m_ref = reinterpret_cast(reinterpret_cast(m_ref) ^ static_cast(1)); } aig * ptr() const { return reinterpret_cast(reinterpret_cast(m_ref) & ~static_cast(1)); } diff --git a/src/util/inf_s_integer.h b/src/util/inf_s_integer.h index 873ad2bdec..12b2c08d0c 100644 --- a/src/util/inf_s_integer.h +++ b/src/util/inf_s_integer.h @@ -45,6 +45,7 @@ class inf_s_integer { std::string to_string() const; inf_s_integer() = default; + inf_s_integer(const inf_s_integer&) = default; explicit inf_s_integer(int n):m_first(n), m_second(0) {} explicit inf_s_integer(int n, int d): m_first(n), m_second(0) { SASSERT(d == 1); } diff --git a/src/util/params.cpp b/src/util/params.cpp index 751789c34f..4a997b11a4 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -361,7 +361,8 @@ class params { rational * m_rat_value; }; value() : m_kind(CPK_BOOL), m_bool_value(false) {} - value& operator=(value const& other) { + value(const value &) = default; + value &operator=(value const &other) { m_kind = other.m_kind; switch (m_kind) { case CPK_BOOL: m_bool_value = other.m_bool_value; break; diff --git a/src/util/ref_buffer.h b/src/util/ref_buffer.h index d82b0bd538..269d10ea62 100644 --- a/src/util/ref_buffer.h +++ b/src/util/ref_buffer.h @@ -174,7 +174,9 @@ public: super(ref_manager_wrapper(other.m_manager)) { SASSERT(this->m_buffer.size() == 0); append(other); - } + } + + ref_buffer &operator=(const ref_buffer &) = default; }; /**