Add formula for CBMC 6.3.1

Formula/cbmc@6.3.1.rb

@@ -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: "6c91ca6ec7686de0aa65cd68c7c2dfc873503a9b380db85feafd3742b58c9574"
+ sha256 cellar: :any_skip_relocation, arm64_ventura: "7f0064518878e48ba635b18443e28b79264eb8d24687b4726adbd493776cd473"
+ sha256 cellar: :any_skip_relocation, sonoma: "b20765fa29fee591fc4fba490209afb0465b2dae5d0e1c0acd3b128a7dd97548"
+ sha256 cellar: :any_skip_relocation, ventura: "f3b6b2975e3ae7dd20974713df29f2b9fb25b796dcba32f9b83ac11fb7ba6872"
+ sha256 cellar: :any_skip_relocation, x86_64_linux: "c25332008da4a3c4d5dd787b67907da6601c24d0fbfb24c8a28f32dafea54686"
+ 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