Add formula for CBMC 6.3.1

Author: tautschnig

Formula/[email protected]

@@ -0,0 +1,49 @@
+class CbmcAT631 < Formula
+  desc "C Bounded Model Checker"
+  homepage "https://www.cprover.org/cbmc/"
+  url "https://github.com/diffblue/cbmc.git",
+      tag:      "cbmc-6.3.1",
+      revision: "cbmc-d2b4455a109383562735cfb8b52ed8a6d2b6e197"
+  license "BSD-4-Clause"
+
+  bottle do
+    root_url "https://github.com/diffblue/homebrew-cbmc/releases/download/bag-of-goodies"
+  sha256 cellar: :any_skip_relocation, arm64_sonoma:        "eb9a036d14b68a5f531fc134bae66178ef780b81406ed7664d2cf3d655c6bff7"
+  sha256 cellar: :any_skip_relocation, arm64_ventura:       "cf6ce2452d773152d1ca5e40876176a7d29482be33189bd8ea6955ab67e0040d"
+  sha256 cellar: :any_skip_relocation, sonoma:              "0349025e92bf7cd155f2145024daf9163aa03eae344f0c7a907a3cc04fa015e1"
+  sha256 cellar: :any_skip_relocation, ventura:             "e3afc36341a6769c8d7019e3ab1eb1159e562bf39d80902707d704a601044369"
+  sha256 cellar: :any_skip_relocation, x86_64_linux:        "5479cbcce605574b23746ceaca1c9d12dd9d94e47d2e6c9551757b8d2af169b1"
+  end
+
+  depends_on "cmake" => :build
+  depends_on "maven" => :build
+  depends_on "openjdk" => :build
+  depends_on "rust" => :build
+
+  uses_from_macos "bison" => :build
+  uses_from_macos "flex" => :build
+
+  fails_with gcc: "5"
+
+  def install
+    system "cmake", "-S", ".", "-B", "build", "-Dsat_impl=minisat2;cadical", *std_cmake_args
+    system "cmake", "--build", "build"
+    system "cmake", "--install", "build"
+
+    # lib contains only `jar` files
+    libexec.install lib
+  end
+
+  test do
+    # Find a pointer out of bounds error
+    (testpath/"main.c").write <<~EOS
+      #include <stdlib.h>
+      int main() {
+        char *ptr = malloc(10);
+        char c = ptr[10];
+      }
+    EOS
+    assert_match "VERIFICATION FAILED",
+                 shell_output("#{bin}/cbmc --pointer-check main.c", 10)
+  end
+end