|
| 1 | +class CbmcAT5650 < 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.65.0", |
| 6 | + revision: "4e907dd68fc11b189b916e2736a5b3ded54d4c86" |
| 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: "09a2a842c567c48f5471d26385e785ff097a09ea889c7dc1d6b76459e8d6b95f" |
| 12 | + sha256 cellar: :any_skip_relocation, arm64_big_sur: "dc9e9b5b778dc608a7d7e148a6027618dd92edd7e9261659412c74e33cb574e5" |
| 13 | + sha256 cellar: :any_skip_relocation, monterey: "71904aa86fa2f59ff62b1f538585886342afcc4b511dedb3a155e77733cf1ad3" |
| 14 | + sha256 cellar: :any_skip_relocation, big_sur: "bdb5b8ea687776239315cca888265cd72f65e22e64457e6f4e7858503f5d9516" |
| 15 | + sha256 cellar: :any_skip_relocation, catalina: "d60c72d765737b43651c84473565cf8c5381c6e5a3433c345349178d6fdec0fb" |
| 16 | + sha256 cellar: :any_skip_relocation, x86_64_linux: "72e17845eccd5bcee96e0d5b8f6b6c780fde959191a07b4e3d7e2c73488601ed" |
| 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