[SwayamInSync]

Plan item E11 (headers shared with other compilers): contracted code compiled only with this Clang and -fverify-contracts, and nothing told a header which compiler read it.

On the base

A header that GCC, MSVC, or upstream Clang also compiles could not keep its contracts: cppverify::pre(...) after a declarator is a syntax error for them (expected function body after function declarator), and no macro distinguished this compiler with the flag from any other. __cppverify__ was proposed in the syntax study (namespaced-syntax.md) and never defined.

With this PR

With -fverify-contracts, in C++, the compiler predefines:

Macro	Value
__cppverify__	1
__cppverify_major__, __cppverify_minor__, __cppverify_patchlevel__	0, 2, 0 for 0.2.0
__cppverify_version__	"0.2.0-dev", the string cpp-verify --version prints

A shared header wraps each construct in a macro that is empty without them:

#ifdef __cppverify__
#define CPPVERIFY(...) __VA_ARGS__
#else
#define CPPVERIFY(...)
#endif

inline int clamp(int x, int lo, int hi)
  CPPVERIFY(cppverify::pre(lo <= hi))
  CPPVERIFY(cppverify::post(lo <= cppverify::result && cppverify::result <= hi))
{
  return x < lo ? lo : x > hi ? hi : x;
}

Verified: clamp [backend=z3]

The test's header (Inputs/shared_header.h: a spec in an #ifdef block, clauses, a loop's clauses, a cppverify::check, and a ghost block, all wrapped) compiles without a warning under -Wall -Wextra -pedantic -Werror with GCC 13.3 and upstream Clang 18, in C++11 and C++20.

Design

• Like __cplusplus, not like __clang__. The macros say that the constructs are recognized here, a property of the language the file is compiled in, so they are defined with the standard macros, which -undef keeps, and before the command line's, so -U__cppverify__ removes them. They are not defined in C, where the constructs are not recognized, nor without the flag.
• One release, one place. The release moves from clang/lib/Verify/CMakeLists.txt to clang/CMakeLists.txt, which splits it into its numbers and configures all of it into clang/Basic/Version.inc beside Clang's own (CLANG_VERSION_MAJOR and the rest), the header InitPreprocessor already reads for __clang_major__. --version reads it from there too, so the macros and --version cannot disagree; the website's conf.py and build-site.sh read the new place.
• The pattern, from the references. Frama-C's libc does the same with its predefined __FRAMAC__: share/libc/features.h defines __PUSH_FC_STDLIB to a Frama-C pragma under it and to nothing otherwise. A variadic macro takes the commas of a clause, so one macro covers every construct written in a function; declarations only verification uses (specs, proof functions, a namespace alias) go in an #ifdef block.

Locations in macros

Guarded clauses are macro arguments, so where a location in a macro is shown matters now. The text error was already at the argument (Clang's renderer maps it), but the JSON record and the obligation's ID used getPresumedLoc, which takes a macro location to the macro's use, and the counterexample's notes were mapped there on purpose:

On main:  JSON "source": 44:3 to 44:57;      ID postcondition@44:3;  note: counterexample at 44:3
Now:      JSON "source": 44:29 to 44:55;     ID postcondition@44:51; note: counterexample at 44:51

Every location the verifier prints now goes through SourceManager::getFileLoc, Clang's rule: a token of a macro's argument where it is written, any other token of a macro where the macro is used. A range written in one place, such as one argument, is that place (Lexer::makeFileCharRange), and any other keeps the macro's use. A clause written in a macro's body (#define NONNEGATIVE cppverify::post(cppverify::result >= 0)) is still shown at the use, with Clang's "expanded from macro" note:

shared_header.h:56:3: error: verification failed: decrement [postcondition] [backend=z3] [reason=counterexample]
   56 |   NONNEGATIVE
      |   ^~~~~~~~~~~
shared_header.h:50:55: note: expanded from macro 'NONNEGATIVE'
   50 | #define NONNEGATIVE cppverify::post(cppverify::result >= 0)
      |                                     ~~~~~~~~~~~~~~~~~~^~~~

The release moved, so releaseVersion() (#105) reads CPPVERIFY_VERSION_STRING too.

Tests

• predefined_macros.cpp (new): the macros with the flag, through %clang_cc1 and the driver, and with -undef; none without the flag or in C; -U__cppverify__ removes the first; and the version the macros spell is the one cpp-verify --version prints (FileCheck captures the parts from the preprocessed file and matches them in --version's output).
• shared_header.cpp (new) with Inputs/shared_header.h: cpp-verify verifies the guarded contracts (two proofs, a failure in a macro's argument, and one in a macro's body), with each location in the text and in JSON; the same file compiles without the flag as plain C++ under -Wall -Wextra -pedantic, and with -fverify-contracts -fno-verify its IR has no trace of the spec.

On the base both tests fail: no macro is defined, so the guarded contracts vanish and nothing is verified.

Mutants

Each mutant below, applied alone and rebuilt, is caught (10 of 10):

Mutant	Change	Caught by
M1	no macros (the base)	both
M2	defined without the flag	both
M3	defined in C too	predefined_macros.cpp
M4	removed by -undef	predefined_macros.cpp
M5	defined after the command line, so -U cannot remove it	predefined_macros.cpp
M6	major and minor swapped	predefined_macros.cpp
M7	a version string that is not --version's	predefined_macros.cpp
L1	an obligation's anchor keeps its macro's use	shared_header.cpp
L2	the range written in an argument is ignored	shared_header.cpp
L3	the counterexample's notes go to the macro's use	shared_header.cpp

Docs

• Syntax reference: "Headers shared with other compilers", the macros, the pattern for each kind of construct, and two checked examples with their output;
• the toolchain chapter: "Code that other compilers build";
• the tooling page: the supported compiler and the editors that do not use this parser;
• release notes; DESIGN; ARCHITECTURE (where a location in a macro is attributed).

check-doc-examples.py passes on every changed page (40 examples).