From e2df18faafaa69297d6f63420b336ec540eccab9 Mon Sep 17 00:00:00 2001
From: davedets <daviddetlefs@gmail.com>
Date: Wed, 22 Jul 2026 10:28:13 -0700
Subject: [PATCH] Test PR for disabling semicolon warnings (#10169)

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.

https://github.com/Z3Prover/z3/pull/10020 deleted a number of
unnecessary (and, by a strict interpretation, illegal) semicolons. These
were detected by adding -Wextra-semi to CLANG_ONLY_WARNINGS during
testing. The PR did not eliminate all such unnecessary/illegal
semi-colons; Nikolaj Bjorner argued that some IDEs would be confused by
doing so for macro invocations, which otherwise look like function
calls. So it left those, and did not include adding -Wextra-semi to
CLANG_ONLY_WARNINGS in the PR.

I'm worried that not having -Wextra-semi will allow instances of the
semis we'd like to eliminate to creep back in. This PR introduces a
mechanism to disable the warnings for regions with such macro
invocations, and uses that mechanism for one file. If accepted, a
subsequent PR would use this mechanism in all the remaining places, so
that there is a clean clang build with -Wextra-semi.

I verified that:
* It compiles cleanly for if the enable/disable macros have null
definitions, as they would for non-clang compilations.
* It compiles cleanly for a clang build without -Wextra-semis.
* It compiles successfully, albeit with *many* warnings, for a clang
build with-Wextra-semis -- but none of those errors are for the regions
in ast.h where the warning is disabled.
---
 src/ast/ast.h              |  5 ++++
 src/util/manage_warnings.h | 60 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 65 insertions(+)
 create mode 100644 src/util/manage_warnings.h

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 03713ee4b8..4c68fdcea7 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -47,6 +47,7 @@ Revision History:
 #include "util/z3_exception.h"
 #include "util/dependency.h"
 #include "util/rlimit.h"
+#include "util/manage_warnings.h"
 #include <variant>
 #include <span>
 #include <initializer_list>
@@ -2168,6 +2169,7 @@ public:
 
 public:
 
+    START_DISABLE_EXTRA_SEMI_WARNING;
     MATCH_UNARY(is_not);
     MATCH_BINARY(is_eq);
     MATCH_BINARY(is_implies);
@@ -2176,6 +2178,7 @@ public:
     MATCH_BINARY(is_xor);
     MATCH_TERNARY(is_and);
     MATCH_TERNARY(is_or);
+    END_DISABLE_WARNING;
 
     bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); } 
 
@@ -2311,9 +2314,11 @@ public:
     bool is_apply_def(expr const * e) const { return is_app_of(e, basic_family_id, PR_APPLY_DEF); }
     bool is_skolemize(expr const * e) const { return is_app_of(e, basic_family_id, PR_SKOLEMIZE); }
 
+    START_DISABLE_EXTRA_SEMI_WARNING;
     MATCH_UNARY(is_asserted);
     MATCH_UNARY(is_hypothesis);
     MATCH_UNARY(is_lemma);
+    END_DISABLE_WARNING;
 
     bool has_fact(proof const * p) const {
         SASSERT(is_proof(p));
diff --git a/src/util/manage_warnings.h b/src/util/manage_warnings.h
new file mode 100644
index 0000000000..adc6059646
--- /dev/null
+++ b/src/util/manage_warnings.h
@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    build_warnings.h
+
+Abstract:
+
+    Macros to control compiler build warnings.
+
+Author:
+
+    Dave Detlefs 2026-07-20.
+
+Revision History:
+
+--*/
+#pragma once
+
+// #define PRAGMA_MACRO(s) _Pragma(s)
+
+// In some cases, we wish to be able to terminate macros with semicolons,
+// even when the semi is (strictly speaking) illegal when following the
+// expansion of the macro.  (The macro invocations can look like function
+// invocations to some IDE's, and the lack of a trailing semi can confuse them.)
+// In those cases, we add this DUMMY_DECL to the macro; it "consumes" the trailing
+// semi, making it legal.
+
+// Standard preprocessor concatenation gymnastics
+#define CONCAT_IMPL(x, y) x##y
+#define CONCAT(x, y) CONCAT_IMPL(x, y)
+
+#define DUMMY_DECL using CONCAT(__dummy_decl_, __COUNTER__) = int
+
+#define DO_PRAGMA(x) _Pragma(#x)
+
+#ifdef __clang__
+
+#define START_DISABLE_WARNING(s)		\
+  _Pragma("clang diagnostic push")		\
+  DO_PRAGMA(clang diagnostic ignored #s)
+
+
+#define END_DISABLE_WARNING			\
+  _Pragma("clang diagnostic pop")		\
+  DUMMY_DECL
+
+#define START_DISABLE_EXTRA_SEMI_WARNING START_DISABLE_WARNING(-Wextra-semi)
+
+#else
+
+#define START_DISABLE_EXTRA_SEMI_WARNING
+#define END_DISABLE_WARNING
+
+#endif
+
+
+
+