|
| 1 | +class CbmcAT6100 < 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.10.0", |
| 6 | + revision: "7483d0de40b2f39850f4f5ba5dd9c6e38f959e31" |
| 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_tahoe: "46e5946cb90b806b1ecbf1c3cf256815d96889b0d21adc11a0c8c5b108c653ad" |
| 12 | + sha256 cellar: :any_skip_relocation, arm64_sequoia: "beb731873f6f287d49e095ce6d19d2b9d194631c83c1e46517571b0e7c9b8c0c" |
| 13 | + sha256 cellar: :any_skip_relocation, arm64_sonoma: "38ae92b029f8b60744246361fc2674a29fd6e2d9c411dc327686c87a2b1bfc86" |
| 14 | + sha256 cellar: :any_skip_relocation, sonoma: "e1c4abf4abb3826ef30f36ca828edfcd4bc6d02bdbb1f9f9fb752ebf0a95ae07" |
| 15 | + sha256 cellar: :any, arm64_linux: "a321763e33e1d6a7f0a84c0b5198ad1be7e842ad5c7474849e65bcc9f0493f8d" |
| 16 | + sha256 cellar: :any, x86_64_linux: "e07859081c6696685dd14fcd3773c67a397f9818c9d6f8a709ca3a44f5b2df65" |
| 17 | + end |
| 18 | + |
| 19 | + depends_on "cmake" => :build |
| 20 | + depends_on "maven" => :build |
| 21 | + depends_on "openjdk@21" => :build |
| 22 | + depends_on "rust" => :build |
| 23 | + |
| 24 | + uses_from_macos "bison" => :build |
| 25 | + uses_from_macos "flex" => :build |
| 26 | + |
| 27 | + def install |
| 28 | + # Fixes: *** No rule to make target 'bin/goto-gcc', |
| 29 | + # needed by '/tmp/cbmc-20240525-215493-ru4krx/regression/goto-gcc/archives/libour_archive.a'. Stop. |
| 30 | + ENV.deparallelize |
| 31 | + ENV["JAVA_HOME"] = formula_opt_prefix("openjdk@21") |
| 32 | + |
| 33 | + system "cmake", "-S", ".", "-B", "build", "-Dsat_impl=minisat2;cadical", *std_cmake_args |
| 34 | + system "cmake", "--build", "build" |
| 35 | + system "cmake", "--install", "build" |
| 36 | + |
| 37 | + # lib contains only `jar` files |
| 38 | + libexec.install lib |
| 39 | + end |
| 40 | + |
| 41 | + test do |
| 42 | + # Find a pointer out of bounds error |
| 43 | + (testpath/"main.c").write <<~C |
| 44 | + #include <stdlib.h> |
| 45 | + int main() { |
| 46 | + char *ptr = malloc(10); |
| 47 | + char c = ptr[10]; |
| 48 | + } |
| 49 | + C |
| 50 | + assert_match "VERIFICATION FAILED", |
| 51 | + shell_output("#{bin}/cbmc --pointer-check main.c", 10) |
| 52 | + end |
| 53 | +end |
0 commit comments