|
| 1 | +class CbmcAT640 < Formula |
| 2 | + desc "C Bounded Model Checker" |
| 3 | + homepage "https://www.cprover.org/cbmc/" |
| 4 | + url "https://github.com/diffblue/cbmc.git", |
| 5 | + tag: "cbmc-6.4.0", |
| 6 | + revision: "cbmc-4f56b6a911911fe89c73e2b6b58c96852e8b233d" |
| 7 | + license "BSD-4-Clause" |
| 8 | + |
| 9 | + bottle do |
| 10 | + root_url "https://github.com/diffblue/homebrew-cbmc/releases/download/bag-of-goodies" |
| 11 | + sha256 cellar: :any_skip_relocation, arm64_sonoma: "1afe625f9beba019f9b615ca81430b4ade5a41d4c5d011217b8f63d50b50f198" |
| 12 | + sha256 cellar: :any_skip_relocation, arm64_ventura: "a9f77303f241f6050ed86f3a6fb81a9ea3eb3595f5bfc70861961932f74d9f0a" |
| 13 | + sha256 cellar: :any_skip_relocation, sonoma: "bfbf8341d5af86a3eb512d3c818e6c318c9a3e24f4e83a4d89f4ab68ae12163d" |
| 14 | + sha256 cellar: :any_skip_relocation, ventura: "a6f2b900703c227d5d2e767eea7184f0a04abe2177864bae6441b9cd1ebced63" |
| 15 | + sha256 cellar: :any_skip_relocation, x86_64_linux: "a28da9bf0494960e632b2cc6ebeac1b6760c2550dbebd5b2ef24b4516c913aaa" |
| 16 | + end |
| 17 | + |
| 18 | + depends_on "cmake" => :build |
| 19 | + depends_on "maven" => :build |
| 20 | + depends_on "openjdk" => :build |
| 21 | + depends_on "rust" => :build |
| 22 | + |
| 23 | + uses_from_macos "bison" => :build |
| 24 | + uses_from_macos "flex" => :build |
| 25 | + |
| 26 | + fails_with gcc: "5" |
| 27 | + |
| 28 | + def install |
| 29 | + system "cmake", "-S", ".", "-B", "build", "-Dsat_impl=minisat2;cadical", *std_cmake_args |
| 30 | + system "cmake", "--build", "build" |
| 31 | + system "cmake", "--install", "build" |
| 32 | + |
| 33 | + # lib contains only `jar` files |
| 34 | + libexec.install lib |
| 35 | + end |
| 36 | + |
| 37 | + test do |
| 38 | + # Find a pointer out of bounds error |
| 39 | + (testpath/"main.c").write <<~EOS |
| 40 | + #include <stdlib.h> |
| 41 | + int main() { |
| 42 | + char *ptr = malloc(10); |
| 43 | + char c = ptr[10]; |
| 44 | + } |
| 45 | + EOS |
| 46 | + assert_match "VERIFICATION FAILED", |
| 47 | + shell_output("#{bin}/cbmc --pointer-check main.c", 10) |
| 48 | + end |
| 49 | +end |
0 commit comments