From bd359a9e98cfc50dfc339b3942733ce4c6a656c3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:09:38 +0530 Subject: [PATCH 1/6] verify: Turn off AssertMacros.h's names without underscores on Apple targets, which expand cppverify::check. --- clang/lib/Frontend/InitPreprocessor.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/clang/lib/Frontend/InitPreprocessor.cpp b/clang/lib/Frontend/InitPreprocessor.cpp index e82b43f5f9..478d090a77 100644 --- a/clang/lib/Frontend/InitPreprocessor.cpp +++ b/clang/lib/Frontend/InitPreprocessor.cpp @@ -1659,10 +1659,18 @@ void clang::InitializePreprocessor(Preprocessor &PP, InitOpts.ImplicitPCHInclude); // CppVerify: the namespace cppverify needs no #include. - if (PP.getLangOpts().VerifyContracts && PP.getLangOpts().CPlusPlus) + if (PP.getLangOpts().VerifyContracts && PP.getLangOpts().CPlusPlus) { + // Apple's defines check(assertion) unless this is 0, + // which would expand cppverify::check. + if (PP.getTargetInfo().getTriple().isOSDarwin()) + Builder.append( + "#ifndef __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES\n" + "#define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 0\n" + "#endif"); Builder.append("#if __has_include()\n" "#include \n" "#endif"); + } // Process -include directives. for (unsigned i = 0, e = InitOpts.Includes.size(); i != e; ++i) { From f0e516c022d75699aa18adf8110de027d1fde876 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:09:38 +0530 Subject: [PATCH 2/6] test: Add the part of Apple's AssertMacros.h that defines check. --- clang/test/Verify/Inputs/apple/AssertMacros.h | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 clang/test/Verify/Inputs/apple/AssertMacros.h diff --git a/clang/test/Verify/Inputs/apple/AssertMacros.h b/clang/test/Verify/Inputs/apple/AssertMacros.h new file mode 100644 index 0000000000..c891fa46ba --- /dev/null +++ b/clang/test/Verify/Inputs/apple/AssertMacros.h @@ -0,0 +1,15 @@ +// The part of Apple's that collides with cppverify::check: +// unless __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES is 0, it defines +// check(assertion) as __Check(assertion), which production code defines empty. + +#ifndef __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES +#define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 1 +#endif + +#define __Check(assertion) + +#if __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES +#ifndef check +#define check(assertion) __Check(assertion) +#endif +#endif From c7144bee6014923a599542462453dccfaf2a5776 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:09:38 +0530 Subject: [PATCH 3/6] test: cppverify::check works beside Apple's AssertMacros.h on Apple targets. --- clang/test/Verify/assert_macros_darwin.cpp | 28 ++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 clang/test/Verify/assert_macros_darwin.cpp diff --git a/clang/test/Verify/assert_macros_darwin.cpp b/clang/test/Verify/assert_macros_darwin.cpp new file mode 100644 index 0000000000..bbd758aeb3 --- /dev/null +++ b/clang/test/Verify/assert_macros_darwin.cpp @@ -0,0 +1,28 @@ +// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -fsyntax-only -verify -isystem %S/Inputs/apple %s +// RUN: %clang_cc1 -triple arm64-apple-ios17.0 -std=c++17 -fverify-contracts -fsyntax-only -verify -isystem %S/Inputs/apple %s +// RUN: not %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -fsyntax-only -D__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES=1 -isystem %S/Inputs/apple %s 2>&1 | FileCheck %s --check-prefix=OLD +// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=OFF +// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=ON +// RUN: %clang_cc1 -triple x86_64-unknown-linux-gnu -std=c++17 -fverify-contracts -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=ON +// +// Apple's defines check(assertion) unless +// __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES is 0, which would expand +// cppverify::check. -fverify-contracts sets it to 0 on Apple targets unless +// the command line defines it. + +#include + +namespace cv = cppverify; + +int positive(int x) + cv::pre(x > 0) +{ + cv::check(x > 0); + cppverify::check(x != 0); + return x; +} + +// expected-no-diagnostics +// OLD: error: expected unqualified-id +// OFF: #define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 0 +// ON: #define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 1 From fb5eb68084e25c405ef8303b167e4b204b38031a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:09:39 +0530 Subject: [PATCH 4/6] docs: Explain macros named like a construct and Apple's AssertMacros.h switch. --- website/source/language/syntax.rst | 59 ++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/website/source/language/syntax.rst b/website/source/language/syntax.rst index f6c128a580..3138c5820f 100644 --- a/website/source/language/syntax.rst +++ b/website/source/language/syntax.rst @@ -191,3 +191,62 @@ Full table: * - ``cppverify::valid(p, n)`` - In ``cppverify::pre`` - ``p`` points to ``n`` objects + +Macros named like a construct +----------------------------- + +The preprocessor runs before the parser sees a construct, so a function-like +macro named like a construct expands inside the qualified name. A header that +defines ``check(condition)`` breaks every ``cppverify::check`` after it: + +.. cppverify-example: rejects + +.. code-block:: cpp + + #define check(condition) ((void)0) + + int positive(int x) + cv::pre(x > 0) + { + cv::check(x > 0); + return x; + } + +.. code-block:: text + + macros.cpp:6:7: error: expected unqualified-id + +``#undef check`` after the header's ``#include`` restores the construct: + +.. code-block:: cpp + + #define check(condition) ((void)0) + #undef check + + int positive(int x) + cv::pre(x > 0) + { + cv::check(x > 0); + return x; + } + +.. code-block:: text + + Verified: positive [backend=z3] + +An object-like macro has the same effect on a construct written without +parentheses, such as ``cv::result``. + +On Apple platforms (macOS, iOS, and the others), ````, which +some of Apple's framework headers include, defines ``check(assertion)`` unless +``__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES`` is ``0``. With +``-fverify-contracts`` on an Apple target, the compiler therefore defines it +to ``0`` before any header, unless the command line defines it, and +``cppverify::check`` works next to that header. The header then defines only +its ``__Check``, ``__Require``, and ``__Verify`` macros, the names Apple +recommends. A file that uses the old names (``check``, ``require``, +``verify``, and their variants) can switch to the ``__`` names, or keep the +old ones with ``-D__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES=1`` on +the command line; ``cppverify::check`` then works only after an ``#undef +check``. Defining it to ``1`` with ``#define`` in the source also works, with +a ``-Wmacro-redefined`` warning. From e4fed0c54281caa9fedb824cfbf00f31e3f40819 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 19:09:39 +0530 Subject: [PATCH 5/6] docs: Apple's AssertMacros.h switch in DESIGN. --- docs/DESIGN.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index d08bbc23dd..9976dbcb4a 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1530,6 +1530,11 @@ deleted functions (`void pre(bool condition) = delete;`) and the others as unavailable enumerators (`result`, `inductive`, `spec`, ...), so any use the parser does not take as a construct is an error. `InitPreprocessor` includes the header in every C++ translation unit compiled with `-fverify-contracts`. +On Darwin targets it first defines +`__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES` to 0 unless the command +line defines it: otherwise Apple's `` defines +`check(assertion)`, and a function-like macro expands inside +`cppverify::check(...)` before the parser can recognize the construct. Misuse is diagnosed where the parser would otherwise fail: a construct in the wrong position (`'cppverify::pre' follows a function's parameter list`), an From 3a27f1e069028eaeadb2a2076624a9debe81a6b4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 20 Oct 2026 23:13:20 +0530 Subject: [PATCH 6/6] docs: cppverify::check works beside Apple's AssertMacros.h, in the release notes. --- website/source/release-notes.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b8abf5d90b..10e360f33f 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -114,6 +114,13 @@ parameters did not compile. Its contracts now compile and instantiate, and are ignored with a ``-Wcontract-unsupported`` warning; a template without contracts no longer stops the file (:doc:`language/functions-loops`). +**Apple's assertion macros.** On Apple targets ```` defines a +``check(assertion)`` macro, which turned every ``cppverify::check(...)`` after +it into ``error: expected unqualified-id``. ``-fverify-contracts`` now defines +``__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES`` to ``0`` on Apple +targets unless the command line defines it, so the header defines only its +``__Check``, ``__Require``, and ``__Verify`` names (:doc:`language/syntax`). + Running cpp-verify ~~~~~~~~~~~~~~~~~~