|
| 1 | +class CbmcAT5951 < 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.95.1", |
| 6 | + revision: "731338d5d82ac86fc447015e0bd24cdf7a74c442" |
| 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: "92bb1f8cc02bad88bd71845a615a311747c44c20449860543e05742268e06449" |
| 12 | + sha256 cellar: :any_skip_relocation, arm64_ventura: "103f86dde81bc92368e10ab5ec0fcb6addd771dd85839f490fcde72fd512cefb" |
| 13 | + sha256 cellar: :any_skip_relocation, arm64_monterey: "ec0b3ad59689b24a9d003b0f4d15994018989da3fce5fd4d7713b37383bbaefe" |
| 14 | + sha256 cellar: :any_skip_relocation, sonoma: "b81523cf245ba04dc8e17152f27f91397f65712c279b0dec569014726bd35923" |
| 15 | + sha256 cellar: :any_skip_relocation, ventura: "35258a857e982e4b3b6aa365c70d6dba213e1900c185412651ce429ef1af4fc6" |
| 16 | + sha256 cellar: :any_skip_relocation, monterey: "94a2e38a53ad76739e41981ae4097ce4a3aee732988e589fd71287f621836c77" |
| 17 | + sha256 cellar: :any_skip_relocation, x86_64_linux: "a8e785b5f7b674f40d3ef03f40d3a94b191b42348c07555b1548b55b37550c6c" |
| 18 | + end |
| 19 | + |
| 20 | + depends_on "cmake" => :build |
| 21 | + depends_on "maven" => :build |
| 22 | + depends_on "openjdk" => :build |
| 23 | + depends_on "rust" => :build |
| 24 | + |
| 25 | + uses_from_macos "bison" => :build |
| 26 | + uses_from_macos "flex" => :build |
| 27 | + |
| 28 | + fails_with gcc: "5" |
| 29 | + |
| 30 | + def install |
| 31 | + system "cmake", "-S", ".", "-B", "build", "-Dsat_impl=minisat2;cadical", *std_cmake_args |
| 32 | + system "cmake", "--build", "build" |
| 33 | + system "cmake", "--install", "build" |
| 34 | + |
| 35 | + # lib contains only `jar` files |
| 36 | + libexec.install lib |
| 37 | + end |
| 38 | + |
| 39 | + test do |
| 40 | + # Find a pointer out of bounds error |
| 41 | + (testpath/"main.c").write <<~EOS |
| 42 | + #include <stdlib.h> |
| 43 | + int main() { |
| 44 | + char *ptr = malloc(10); |
| 45 | + char c = ptr[10]; |
| 46 | + } |
| 47 | + EOS |
| 48 | + assert_match "VERIFICATION FAILED", |
| 49 | + shell_output("#{bin}/cbmc --pointer-check main.c", 10) |
| 50 | + end |
| 51 | +end |
0 commit comments