|
| 1 | +class CbmcAT5640 < 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-5.64.0", |
| 6 | + revision: "8fbba35f27b9b3efb78f3b875ba27bf4ea6fe641" |
| 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_monterey: "f8ad0d2998bd8c0912b44f934971a759f246bdd75cf262583264eae72a0e2e37" |
| 12 | + sha256 cellar: :any_skip_relocation, arm64_big_sur: "04747aa18a76adbaab78a67a817641f52a20e2a9f5ad0feb6fa50f14dbfc84ab" |
| 13 | + sha256 cellar: :any_skip_relocation, monterey: "7223211e59041b35a5fbbea35845f491b9c30174a65c5459d95c98473cc850bf" |
| 14 | + sha256 cellar: :any_skip_relocation, big_sur: "80e0fffe41745e2e2538803173381255c5960d6af0f28b37d6023a2eae797334" |
| 15 | + sha256 cellar: :any_skip_relocation, catalina: "b2ffe640a432284e7be95300365df31a53eb32a0826563804b874a9d4c289b94" |
| 16 | + sha256 cellar: :any_skip_relocation, x86_64_linux: "0797247f218de07871aec44b28155faadf2e0e55c650c9b10947eb09e344c161" |
| 17 | + end |
| 18 | + |
| 19 | + depends_on "cmake" => :build |
| 20 | + depends_on "maven" => :build |
| 21 | + depends_on "openjdk" => :build |
| 22 | + |
| 23 | + uses_from_macos "bison" => :build |
| 24 | + uses_from_macos "flex" => :build |
| 25 | + |
| 26 | + on_linux do |
| 27 | + depends_on "gcc" |
| 28 | + end |
| 29 | + |
| 30 | + fails_with gcc: "5" |
| 31 | + |
| 32 | + def install |
| 33 | + system "cmake", "-S", ".", "-B", "build", *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 <<~EOS |
| 44 | + #include <stdlib.h> |
| 45 | + int main() { |
| 46 | + char *ptr = malloc(10); |
| 47 | + char c = ptr[10]; |
| 48 | + } |
| 49 | + EOS |
| 50 | + assert_match "VERIFICATION FAILED", |
| 51 | + shell_output("#{bin}/cbmc --pointer-check main.c", 10) |
| 52 | + end |
| 53 | +end |
0 commit comments