From 44cc1e0c98254cd124c556ad576278586a98d9c2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 12:10:10 +0530 Subject: [PATCH 1/3] verify: Verify a .h input as C++, and stop a file whose command line has an error. --- clang/tools/cpp-verify/Main.cpp | 46 ++++++++++++++++++++++++++++++++- 1 file changed, 45 insertions(+), 1 deletion(-) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 32e12ac7d2..1df21d485e 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -10,7 +10,9 @@ #include "clang/AST/ASTConsumer.h" #include "clang/AST/ASTContext.h" #include "clang/Frontend/CompilerInstance.h" +#include "clang/Frontend/CompilerInvocation.h" #include "clang/Frontend/FrontendAction.h" +#include "clang/Frontend/TextDiagnosticPrinter.h" #include "clang/Tooling/CommonOptionsParser.h" #include "clang/Tooling/Tooling.h" #include "llvm/ADT/STLExtras.h" @@ -20,6 +22,7 @@ #include "llvm/Support/InitLLVM.h" #include "llvm/Support/JSON.h" #include "llvm/Support/MemoryBuffer.h" +#include "llvm/Support/Path.h" #include "llvm/Support/Process.h" #include "llvm/Support/raw_ostream.h" #include @@ -361,6 +364,33 @@ class VerifyAction : public ASTFrontendAction { } }; +/// Verifies each file whose command line clang accepts. An argument error +/// stops the file, as it stops clang; tooling would print it and go on. +class VerifyActionFactory : public FrontendActionFactory { +public: + explicit VerifyActionFactory(const DiagnosticConsumer &Arguments) + : Arguments(Arguments) {} + std::unique_ptr create() override { + return std::make_unique(); + } + bool runInvocation(std::shared_ptr Invocation, + FileManager *Files, + std::shared_ptr PCHContainerOps, + DiagnosticConsumer *) override { + if (Arguments.getNumErrors() != ArgumentErrors) { + ArgumentErrors = Arguments.getNumErrors(); + return false; + } + // The file reports with its own diagnostic options. + return FrontendActionFactory::runInvocation( + std::move(Invocation), Files, std::move(PCHContainerOps), nullptr); + } + +private: + const DiagnosticConsumer &Arguments; + unsigned ArgumentErrors = 0; +}; + // Replay proves each module alone: the contracts and spec facts its proof // rests on, its qualifiers, and its vacuity belong to the source run. static constexpr const char ReplayProofNote[] = @@ -860,13 +890,27 @@ int main(int argc, const char **argv) { OptionsParser.getSourcePathList()); Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster( {"-fverify-contracts", "-std=c++17"}, ArgumentInsertPosition::BEGIN)); + // Clang takes a .h file for C; here every input is C++. + Tool.appendArgumentsAdjuster( + [](const CommandLineArguments &Args, StringRef Filename) { + if (llvm::sys::path::extension(Filename) != ".h") + return Args; + CommandLineArguments Adjusted = Args; + Adjusted.insert(Adjusted.begin() + 1, "-xc++-header"); + return Adjusted; + }); #if defined(__APPLE__) if (const char *SDK = std::getenv("SDKROOT"); SDK && SDK[0]) Tool.appendArgumentsAdjuster(getInsertArgumentAdjuster( {"-isysroot", SDK}, ArgumentInsertPosition::BEGIN)); #endif - int RC = Tool.run(newFrontendActionFactory().get()); + std::unique_ptr ArgumentOptions = + CreateAndPopulateDiagOpts({"cpp-verify"}); + TextDiagnosticPrinter ArgumentDiagnostics(llvm::errs(), *ArgumentOptions); + Tool.setDiagnosticConsumer(&ArgumentDiagnostics); + VerifyActionFactory Factory(ArgumentDiagnostics); + int RC = Tool.run(&Factory); if (RC != 0) return RC; if (ObligationFile) { From 56d19b7e0d003d2151a26835d28bd37ea02349ea Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 12:10:11 +0530 Subject: [PATCH 2/3] test: Check a header input, a C input, and an unknown flag. --- clang/test/Verify/suite/input_errors.cpp | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 clang/test/Verify/suite/input_errors.cpp diff --git a/clang/test/Verify/suite/input_errors.cpp b/clang/test/Verify/suite/input_errors.cpp new file mode 100644 index 0000000000..8e7bc59e89 --- /dev/null +++ b/clang/test/Verify/suite/input_errors.cpp @@ -0,0 +1,20 @@ +// RUN: rm -rf %t && mkdir -p %t +// RUN: cp %s %t/input.h +// RUN: %cpp-verify %t/input.h -- 2>&1 | FileCheck %s --check-prefix=HEADER --implicit-check-not=error: +// RUN: cp %s %t/input.c +// RUN: not %cpp-verify %t/input.c -- 2>&1 | FileCheck %s --check-prefix=C --implicit-check-not=Verified +// RUN: not %cpp-verify %s -- -fbogus-flag 2>&1 | FileCheck %s --check-prefix=FLAG --implicit-check-not=Verified +// +// A header given as input is C++, and an error in a command line stops its +// file, as it stops clang. + +inline int twice_small(int x) + cppverify::pre(x >= 0 && x < 100) + cppverify::post(cppverify::result == 2 * x) +{ + return 2 * x; +} + +// HEADER: Verified: twice_small [backend=z3] +// C: error: invalid argument '-std=c++17' not allowed with 'C' +// FLAG: error: unknown argument: '-fbogus-flag' From 4094d0385799674351354cef46e852d1fddd7c97 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 14 Oct 2026 12:10:11 +0530 Subject: [PATCH 3/3] docs: State how headers and command-line errors are handled. --- website/source/language/tooling.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 0fcf753ef3..38a83a963e 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -34,7 +34,8 @@ Other compiler flags come from the ``compile_commands.json`` beside the file or above it, or in the directory ``-p DIR`` names; a file the database does not list gets the flags of a listed neighbour. Without a database the file is compiled with those two flags alone. Flags after ``--`` replace the database, and ``--extra-arg=FLAG`` adds one flag either -way. +way. A ``.h`` file given as input is a C++ header. A compiler error, in a command line or in +the file, stops that file without verifying it, and ``cpp-verify`` then exits with status 1. ``cpp-verify --version`` shows the cpp-verify release and repository revision, the LLVM release it is built on, and each backend: the Z3 linked into it, and the cvc5 and Lean