SwayamInSync · Oct 29, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026 · Oct 28, 2026
diff --git a/clang/include/clang/Frontend/FrontendOptions.h b/clang/include/clang/Frontend/FrontendOptions.h
@@ -529,6 +529,24 @@ class FrontendOptions {
   /// assumes from other files, for cpp-verify --check-contracts.
   std::string VerifyContractsOut;
 
+  /// The solver CppVerify verifies a compilation with (-fverify-backend=).
+  enum class CppVerifyBackend { Z3, CVC5, Portfolio, Race, BMC };
+  CppVerifyBackend VerifyBackend = CppVerifyBackend::Z3;
+
+  /// The milliseconds each CppVerify solver query may take, cpp-verify's
+  /// default unless given; 0 disables the limit (-fverify-timeout=).
+  unsigned VerifyTimeoutMs = 30000;
+
+  /// The solver jobs CppVerify runs for this compilation (-fverify-jobs=).
+  unsigned VerifyJobs = 1;
+
+  /// Where CppVerify keeps its proofs across compilations (-fverify-cache=).
+  std::string VerifyCache;
+
+  /// Where CppVerify writes this compilation's results as JSON Lines
+  /// (-fverify-report=).
+  std::string VerifyReport;
+
   /// Auxiliary triple for CUDA/HIP/SYCL compilation.
   std::string AuxTriple;
 

diff --git a/clang/include/clang/Options/Options.td b/clang/include/clang/Options/Options.td
@@ -2537,6 +2537,41 @@ def fverify_contracts_out_EQ : Joined<["-"], "fverify-contracts-out=">,
   HelpText<"Write the contracts CppVerify verifies in this file and those it "
            "assumes from other files, for cpp-verify --check-contracts">,
   MarshallingInfoString<FrontendOpts<"VerifyContractsOut">>;
+def fverify_backend_EQ : Joined<["-"], "fverify-backend=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  HelpText<"The solver CppVerify verifies with: z3 (default), cvc5, portfolio "
+           "(z3 and cvc5 must agree), race (the first decisive answer of z3 "
+           "and cvc5), or bmc">,
+  Values<"z3,cvc5,portfolio,race,bmc">,
+  NormalizedValuesScope<"FrontendOptions::CppVerifyBackend">,
+  NormalizedValues<["Z3", "CVC5", "Portfolio", "Race", "BMC"]>,
+  MarshallingInfoEnum<FrontendOpts<"VerifyBackend">, "Z3">;
+def fverify_timeout_EQ : Joined<["-"], "fverify-timeout=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<ms>">,
+  HelpText<"Milliseconds each CppVerify solver query may take (default 30000; "
+           "0 disables)">,
+  MarshallingInfoInt<FrontendOpts<"VerifyTimeoutMs">, "30000">;
+def fverify_jobs_EQ : Joined<["-"], "fverify-jobs=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<n>">,
+  HelpText<"Solver jobs CppVerify runs for each compilation (default 1)">,
+  MarshallingInfoInt<FrontendOpts<"VerifyJobs">, "1">;
+def fverify_cache_EQ : Joined<["-"], "fverify-cache=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<dir>">,
+  HelpText<"Keep CppVerify's proofs in <dir>, shared by compilations, so that "
+           "an unchanged obligation is not solved again">,
+  MarshallingInfoString<FrontendOpts<"VerifyCache">>;
+def fverify_report : Flag<["-"], "fverify-report">, Group<f_clang_Group>,
+  Visibility<[ClangOption]>,
+  HelpText<"Write CppVerify's results as JSON Lines beside the object file, "
+           "in <object>.cppverify.json">;
+def fverify_report_EQ : Joined<["-"], "fverify-report=">,
+  Group<f_clang_Group>, Visibility<[ClangOption, CC1Option]>,
+  MetaVarName<"<file>">,
+  HelpText<"Write CppVerify's results as JSON Lines to <file>">,
+  MarshallingInfoString<FrontendOpts<"VerifyReport">>;
 def fno_verify : Flag<["-"], "fno-verify">, Group<f_clang_Group>,
   Visibility<[ClangOption, CC1Option]>,
   HelpText<"Check contract syntax and semantics but skip CppVerify SMT verification "

diff --git a/clang/lib/CodeGen/CodeGenAction.cpp b/clang/lib/CodeGen/CodeGenAction.cpp
@@ -244,8 +244,7 @@ bool BackendConsumer::LinkInModules(llvm::Module *M) {
 void BackendConsumer::HandleTranslationUnit(ASTContext &C) {
   std::optional<std::future<verify::CppVerifyAsyncResult>> VerifyFuture;
   if (verify::shouldRunCppVerify(CI))
-    VerifyFuture =
-        verify::startCppVerifyAsync(C, CI.getFrontendOpts().VerifyContractsOut);
+    VerifyFuture = verify::startCppVerifyAsync(C, CI.getFrontendOpts());
 
   {
     llvm::TimeTraceScope TimeScope("Frontend");

diff --git a/clang/lib/Driver/ToolChains/Clang.cpp b/clang/lib/Driver/ToolChains/Clang.cpp
@@ -6699,6 +6699,24 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   // language, so when neither -f/-fno-verify-contracts was given it implies
   // -fverify-contracts, yielding a syntax/semantics-only "light check".
   Args.AddLastArg(CmdArgs, options::OPT_fverify_contracts_out_EQ);
+  for (OptSpecifier Opt :
+       {options::OPT_fverify_backend_EQ, options::OPT_fverify_timeout_EQ,
+        options::OPT_fverify_jobs_EQ, options::OPT_fverify_cache_EQ})
+    Args.AddLastArg(CmdArgs, Opt);
+  // -fverify-report writes beside the object, as -ftime-trace does.
+  if (Arg *A = Args.getLastArg(options::OPT_fverify_report,
+                               options::OPT_fverify_report_EQ)) {
+    SmallString<128> Report;
+    if (A->getOption().matches(options::OPT_fverify_report_EQ))
+      Report = A->getValue();
+    else if (Output.isFilename())
+      Report = Output.getFilename();
+    else
+      Report = llvm::sys::path::stem(Input.getBaseInput());
+    if (!A->getOption().matches(options::OPT_fverify_report_EQ))
+      Report += ".cppverify.json";
+    CmdArgs.push_back(Args.MakeArgString("-fverify-report=" + Report));
+  }
   if (Args.hasArg(options::OPT_fno_verify)) {
     CmdArgs.push_back("-fno-verify");
     if (!Args.hasArg(options::OPT_fverify_contracts) &&

diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.cpp b/clang/lib/Verify/Driver/CppVerifyIntegration.cpp
@@ -3,6 +3,8 @@
 #include "Verifier.h"
 #include "clang/Basic/DiagnosticFrontend.h"
 #include "clang/Frontend/CompilerInstance.h"
+#include "clang/Frontend/FrontendOptions.h"
+#include <limits>
 #include "llvm/Support/raw_ostream.h"
 #include <thread>
 
@@ -19,16 +21,48 @@ bool verify::shouldRunCppVerify(const CompilerInstance &CI) {
   return true;
 }
 
+VerifyOptions verify::compilationOptions(const FrontendOptions &Options) {
+  VerifyOptions Opts;
+  switch (Options.VerifyBackend) {
+  case FrontendOptions::CppVerifyBackend::Z3:
+    Opts.Backend = BackendKind::Z3;
+    break;
+  case FrontendOptions::CppVerifyBackend::CVC5:
+    Opts.Backend = BackendKind::CVC5;
+    break;
+  case FrontendOptions::CppVerifyBackend::Portfolio:
+    Opts.Backend = BackendKind::Portfolio;
+    break;
+  case FrontendOptions::CppVerifyBackend::Race:
+    Opts.Backend = BackendKind::Race;
+    break;
+  case FrontendOptions::CppVerifyBackend::BMC:
+    Opts.Backend = BackendKind::BMC;
+    break;
+  }
+  const unsigned Timeout = Options.VerifyTimeoutMs;
+  const unsigned Max = std::numeric_limits<unsigned>::max();
+  Opts.SolverTimeoutMs = Timeout;
+  Opts.CollectionTimeoutMs = Timeout > Max / 2 ? 0 : 2 * Timeout;
+  Opts.FunctionTimeoutMs = Timeout > Max / 10 ? 0 : 10 * Timeout;
+  Opts.Jobs = std::max(1u, Options.VerifyJobs);
+  Opts.ProofCachePath = Options.VerifyCache;
+  Opts.ReportPath = Options.VerifyReport;
+  Opts.ContractsOut = Options.VerifyContractsOut;
+  Opts.QuietWithoutFunctions = true;
+  return Opts;
+}
+
 std::future<CppVerifyAsyncResult>
-verify::startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut) {
-  return std::async(std::launch::async, [&Ctx, ContractsOut]() {
-    CppVerifyAsyncResult Result;
-    VerifyOptions Opts;
-    Opts.ContractsOut = ContractsOut;
-    Opts.Parts = &Result.Parts;
-    Result.Ok = verifyTranslationUnit(Ctx, llvm::nulls(), Opts);
-    return Result;
-  });
+verify::startCppVerifyAsync(ASTContext &Ctx, const FrontendOptions &Options) {
+  return std::async(std::launch::async,
+                    [&Ctx, Opts = compilationOptions(Options)]() mutable {
+                      CppVerifyAsyncResult Result;
+                      Opts.Parts = &Result.Parts;
+                      Result.Ok =
+                          verifyTranslationUnit(Ctx, llvm::nulls(), Opts);
+                      return Result;
+                    });
 }
 
 bool verify::finishCppVerify(CompilerInstance &CI,

diff --git a/clang/lib/Verify/Driver/CppVerifyIntegration.h b/clang/lib/Verify/Driver/CppVerifyIntegration.h
@@ -3,13 +3,15 @@
 #define LLVM_CLANG_VERIFY_DRIVER_CPPVERIFY_INTEGRATION_H
 
 #include "DiagnosticPart.h"
+#include "Verifier.h"
 #include <future>
 #include <string>
 #include <vector>
 
 namespace clang {
 class ASTContext;
 class CompilerInstance;
+class FrontendOptions;
 
 namespace verify {
 
@@ -19,15 +21,23 @@ struct CppVerifyAsyncResult {
   std::vector<VerifyDiagnosticPart> Parts;
 };
 
+/// The verifier's options for a compilation with \p Options' -fverify-*
+/// options, as cpp-verify's options of the same names set them: a query
+/// timeout also scales the collection and function timeouts. A file without
+/// a function to verify says nothing.
+VerifyOptions compilationOptions(const FrontendOptions &Options);
+
 /// Returns true if CppVerify SMT should run for this compilation.
 bool shouldRunCppVerify(const CompilerInstance &CI);
 
-/// Start SMT verification on \p Ctx in a background thread. The AST must not be
-/// mutated while the future is pending (safe during codegen IR generation).
-/// With \p ContractsOut, contracts declared without a definition are assumed
-/// and recorded there with those verified, for cpp-verify --check-contracts.
+/// Start SMT verification on \p Ctx in a background thread, with the
+/// -fverify-* options of \p Options. The AST must not be mutated while the
+/// future is pending (safe during codegen IR generation). With
+/// -fverify-contracts-out, contracts declared without a definition are
+/// assumed and recorded there with those verified, for cpp-verify
+/// --check-contracts.
 std::future<CppVerifyAsyncResult>
-startCppVerifyAsync(ASTContext &Ctx, std::string ContractsOut = "");
+startCppVerifyAsync(ASTContext &Ctx, const FrontendOptions &Options);
 
 /// Join \p Future and report its results through the compiler's diagnostics:
 /// failures as errors with notes, warnings in -Wcppverify, and proofs as

diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
@@ -3389,8 +3389,9 @@ class Verifier {
                          "obligation"});
         return false;
       }
-      Diags.push_back(
-          {VerifyDiagnostic::Warning, "no verifiable functions found"});
+      if (!Opts.QuietWithoutFunctions)
+        Diags.push_back(
+            {VerifyDiagnostic::Warning, "no verifiable functions found"});
       return true;
     }
     Converted = std::chrono::steady_clock::now();
@@ -6662,6 +6663,27 @@ class Verifier {
                           D.K == VerifyDiagnostic::Trusted);
   }
 
+  /// Writes every result the run reports to Path as a JSON Lines record, and
+  /// then the summary record; a file that cannot be written is an error.
+  bool writeReport(const std::string &Path) {
+    std::error_code EC;
+    llvm::raw_fd_ostream Report(Path, EC, llvm::sys::fs::OF_Text);
+    if (EC) {
+      Diags.push_back({VerifyDiagnostic::Error,
+                       "cannot write the report " + Path + ": " + EC.message()});
+      return false;
+    }
+    VerifySummary Summary;
+    for (const VerifyDiagnostic &D : Diags) {
+      if (!reported(D))
+        continue;
+      count(D, Summary);
+      printJSONDiagnostic(D, Report);
+    }
+    Report << llvm::json::Value(summaryRecord(Summary)) << "\n";
+    return true;
+  }
+
   void printDiagnostics(llvm::raw_ostream &OS) const {
     for (const auto &[Loc, Line] : Listing) {
       PresumedLoc PLoc = Ctx.getSourceManager().getPresumedLoc(
@@ -6995,6 +7017,24 @@ class Verifier {
 
 } // namespace
 
+llvm::json::Object verify::summaryRecord(const VerifySummary &Summary) {
+  llvm::json::Object Record;
+  Record["schema"] = SummarySchema;
+  Record["verified"] = Summary.Verified;
+  Record["failed"] = Summary.Failed;
+  Record["unresolved"] = Summary.Unresolved;
+  llvm::json::Object Reasons;
+  for (const auto &[Reason, N] : Summary.Reasons)
+    Reasons[Reason] = N;
+  Record["reasons"] = std::move(Reasons);
+  Record["bounded_safe"] = Summary.BoundedSafe;
+  Record["trusted"] = Summary.Trusted;
+  Record["lowered"] = Summary.Lowered;
+  Record["exported"] = Summary.Exported;
+  Record["interrupted"] = Summary.Interrupted;
+  return Record;
+}
+
 bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                                    const VerifyOptions &Opts) {
   Verifier V(Ctx, Opts, OS);
@@ -7010,6 +7050,8 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
   }
   if (!Opts.ContractsOut.empty())
     Ok = V.recordContracts() && Ok;
+  if (!Opts.ReportPath.empty())
+    Ok = V.writeReport(Opts.ReportPath) && Ok;
   V.printDiagnostics(OS);
   if (Opts.TimeReport)
     V.printTimeReport(OS);

diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h
@@ -4,6 +4,7 @@
 
 #include "../Backend/VerifyBackend.h"
 #include "DiagnosticPart.h"
+#include "llvm/Support/JSON.h"
 #include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <memory>
@@ -153,6 +154,12 @@ struct VerifyOptions {
   /// without a definition holds for now, and a proof that rests on it says
   /// so ([assumes=...]): the check of the files together settles it.
   std::string ContractsOut;
+  /// Where to write the results as JSON Lines records, besides the output,
+  /// ending with the summary record.
+  std::string ReportPath;
+  /// A file with no function to verify says nothing, as in a compilation,
+  /// where most files have none.
+  bool QuietWithoutFunctions = false;
 };
 
 /// One run over several files. A contract that a file declares without a
@@ -191,6 +198,11 @@ unsigned checkContracts(const std::vector<std::string> &Paths,
 bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS,
                            const VerifyOptions &Opts = VerifyOptions());
 
+/// The cppverify.summary/1 record of \p Summary: the counts of the summary
+/// line, by name, without the time, so that records do not depend on the
+/// run.
+llvm::json::Object summaryRecord(const VerifySummary &Summary);
+
 /// What exporting the modules of an archive to a Lean project gives: a
 /// result for each module, in order, with the goals cppverify_auto proves of
 /// it, and what the project warns of; or why the project was not written.

diff --git a/clang/test/Verify/Inputs/no_contracts.cpp b/clang/test/Verify/Inputs/no_contracts.cpp
@@ -0,0 +1 @@
+int add(int a, int b) { return a + b; }
diff --git a/clang/test/Verify/compile_options.cpp b/clang/test/Verify/compile_options.cpp
@@ -0,0 +1,48 @@
+// RUN: rm -rf %t && mkdir -p %t
+// RUN: %clang -### -std=c++17 -fverify-contracts -fverify-backend=cvc5 -fverify-timeout=5000 -fverify-jobs=2 -fverify-cache=%t/cache -fverify-report -c %s -o %t/x.o 2>&1 | FileCheck %s --check-prefix=DRIVER
+// RUN: %clang -### -std=c++17 -fverify-contracts -fverify-report=%t/named.json -c %s -o %t/x.o 2>&1 | FileCheck %s --check-prefix=NAMED
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-backend=lean -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s --check-prefix=BACKEND
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-timeout=soon -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s --check-prefix=TIMEOUT
+// RUN: %clang_cc1 -std=c++17 -fverify-contracts -emit-obj -o %t/plain.o %S/Inputs/no_contracts.cpp 2>&1 | count 0
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -Rcppverify -fverify-backend=bmc -fverify-report=%t/report.json -emit-obj -o %t/x.o %s 2>&1 | FileCheck %s
+// RUN: FileCheck %s --check-prefix=REPORT < %t/report.json
+// RUN: not %clang_cc1 -std=c++17 -fverify-contracts -fverify-cache=%t/cache -emit-obj -o %t/x.o %s
+// RUN: ls %t/cache | FileCheck %s --check-prefix=CACHE
+//
+// The -fverify-* options of a compilation: the driver forwards them, naming
+// a bare -fverify-report's file after the object; the compiler rejects an
+// invalid value; a file without a function to verify says nothing; and each
+// option reaches the verifier.
+
+namespace cv = cppverify;
+
+int inc(int x)
+  cv::pre(x < 100)
+  cv::post(cv::result == x + 1)
+{
+  return x + 1;
+}
+
+int dec(int x)
+  cv::post(cv::result == x - 1)
+{
+  return x - 1;
+}
+
+// DRIVER: "-cc1"
+// DRIVER-SAME: "-fverify-backend=cvc5" "-fverify-timeout=5000" "-fverify-jobs=2" "-fverify-cache={{[^"]*}}cache" "-fverify-report={{[^"]*}}x.o.cppverify.json"
+
+// NAMED: "-fverify-report={{[^"]*}}named.json"
+// NAMED-NOT: cppverify.json
+
+// BACKEND: error: invalid value 'lean' in '-fverify-backend=lean'
+// TIMEOUT: error: invalid integral value 'soon' in '-fverify-timeout=soon'
+
+// CHECK: remark: Verified: inc [backend=bmc, bound=0]
+// CHECK: error: verification failed: dec [overflow] [backend=bmc{{.*}}]
+
+// REPORT: "function":"inc",{{.*}}"status":"verified"
+// REPORT: "function":"dec",{{.*}}"status":"failed"
+// REPORT: {"bounded_safe":0,{{.*}}"failed":1,{{.*}}"schema":"cppverify.summary/1",{{.*}}"verified":1}
+
+// CACHE: llvmcache-cppverify-
diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
@@ -423,24 +423,10 @@ static void printSummary(std::chrono::steady_clock::time_point Start) {
                                  : llvm::join(Parts, ", "))
                << llvm::formatv(" in {0:f1} s", Seconds) << "\n";
 }
-/// The summary as a record: the counts of the text line, by name. It has no
-/// time, so that records do not depend on the run; --time-report gives it.
+/// The summary as a record; --time-report gives the time.
 static void printSummaryRecord() {
-  llvm::json::Object Record;
-  Record["schema"] = verify::SummarySchema;
-  Record["verified"] = gSummary.Verified;
-  Record["failed"] = gSummary.Failed;
-  Record["unresolved"] = gSummary.Unresolved;
-  llvm::json::Object Reasons;
-  for (const auto &[Reason, N] : gSummary.Reasons)
-    Reasons[Reason] = N;
-  Record["reasons"] = std::move(Reasons);
-  Record["bounded_safe"] = gSummary.BoundedSafe;
-  Record["trusted"] = gSummary.Trusted;
-  Record["lowered"] = gSummary.Lowered;
-  Record["exported"] = gSummary.Exported;
-  Record["interrupted"] = gSummary.Interrupted;
-  out() << llvm::formatv("{0}\n", llvm::json::Value(std::move(Record)));
+  out() << llvm::formatv("{0}\n",
+                         llvm::json::Value(verify::summaryRecord(gSummary)));
 }
 
 static std::vector<std::string> gArguments;