verify: Stop a file whose command line has an error, and verify a .h input as C++

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'

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 <cstdlib>
@@ -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<FrontendAction> create() override {
+    return std::make_unique<VerifyAction>();
+  }
+  bool runInvocation(std::shared_ptr<CompilerInvocation> Invocation,
+                     FileManager *Files,
+                     std::shared_ptr<PCHContainerOperations> 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<VerifyAction>().get());
+  std::unique_ptr<DiagnosticOptions> 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) {

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