Skip to content

Commit

Permalink
cbmc 6.3.0
Browse files Browse the repository at this point in the history 
- Revert 6.2.0 patch

The problem has been addressed upstream (the patch itself was a
cherry-pick from upstream).

Co-authored-by: Michael Tautschnig <[email protected]>
  • Loading branch information
@db-ci-cprover @tautschnig @carlocab
2 people authored and carlocab committed Sep 19, 2024
1 parent 67ffc43 commit d5d3359
Showing 1 changed file with 2 additions and 9 deletions.
11 changes: 2 additions & 9 deletions Formula/c/cbmc.rb
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@ class Cbmc < Formula
desc "C Bounded Model Checker"
homepage "https://www.cprover.org/cbmc/"
url "https://github.com/diffblue/cbmc.git",
tag: "cbmc-6.2.0",
revision: "27b845c975c6bbdfb2ccc6f40bdfae6793d12277"
tag: "cbmc-6.3.0",
revision: "5bd494a1a961762a038ba8e055bc1e4a12dbba3b"
license "BSD-4-Clause"

bottle do
Expand All @@ -25,13 +25,6 @@ class Cbmc < Formula

fails_with gcc: "5"

# Backport fix for CMake Error at jbmc/unit/CMakeLists.txt
# Cannot find source file: /tmp/unit/unit_tests.cpp
patch do
url "https://github.com/diffblue/cbmc/commit/faf92c5354e3aaca6c70013bb75b26a271c6f63d.patch?full_index=1"
sha256 "7dd49f1364a24b914e13e3e16de7611db10467f1235e308d1c7fa77291171de6"
end

def install

Check failure on line 28 in Formula/c/cbmc.rb

View workflow job for this annotation

GitHub Actions / macOS 15-arm64

`brew install --verbose --formula --build-bottle cbmc` failed on macOS Sequoia (15) on Apple Silicon! 

Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/mman.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/netdb.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/process.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/pthread_lib.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/pwd.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/random.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/semaphore.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/setjmp.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/signal.c
Checking /tmp/cbmc-20240919-11841-kdnfyv/src/ansi-c/library/stdio.c
__libcheck.c:1138:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1138 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
      |                                                    ~~~^~~~~~~~
__libcheck.c:1139:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1139 |         __CPROVER_OBJECT_SIZE(arg.__stack))
      |                               ~~~^~~~~~~~
__libcheck.c:1196:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1196 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
      |                                                    ~~~^~~~~~~~
__libcheck.c:1197:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1197 |         __CPROVER_OBJECT_SIZE(arg.__stack))
      |                               ~~~^~~~~~~~
__libcheck.c:1342:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1342 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
      |                                                    ~~~^~~~~~~~
__libcheck.c:1343:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1343 |         __CPROVER_OBJECT_SIZE(arg.__stack))
      |                               ~~~^~~~~~~~
__libcheck.c:1386:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1386 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
      |                                                    ~~~^~~~~~~~
__libcheck.c:1387:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1387 |         __CPROVER_OBJECT_SIZE(arg.__stack))
      |                               ~~~^~~~~~~~
__libcheck.c:1831:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1831 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
      |                                                    ~~^~~~~~~~
__libcheck.c:1832:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1832 |         __CPROVER_OBJECT_SIZE(ap.__stack))
      |                               ~~^~~~~~~~
__libcheck.c:1837:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1837 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
      |                                                                 ~~^~~~~~~~
__libcheck.c:1891:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1891 |   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
      |                                                    ~~^~~~~~~~
__libcheck.c:1892:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1892 |         __CPROVER_OBJECT_SIZE(ap.__stack))
      |                               ~~^~~~~~~~
__libcheck.c:1897:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
 1897 |       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
      |                                                                 ~~^~~~~~~~
14 errors genera

Check failure on line 28 in Formula/c/cbmc.rb

View workflow job for this annotation

GitHub Actions / macOS 14-arm64

`brew install --verbose --formula --build-bottle cbmc` failed on macOS Sonoma (14) on Apple Silicon! 

Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/mman.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/netdb.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/process.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/pthread_lib.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/pwd.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/random.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/semaphore.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/setjmp.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/signal.c
Checking /tmp/cbmc-20240919-17402-1v4qt0/src/ansi-c/library/stdio.c
__libcheck.c:1138:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1139:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1196:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1197:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1342:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1343:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1386:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1387:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1831:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
                                                   ~~^~~~~~~~
__libcheck.c:1832:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(ap.__stack))
                              ~~^~~~~~~~
__libcheck.c:1837:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
                                                                ~~^~~~~~~~
__libcheck.c:1891:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
                                                   ~~^~~~~~~~
__libcheck.c:1892:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(ap.__stack))
                              ~~^~~~~~~~
__libcheck.c:1897:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
                                                                ~~^~~~~~~~
14 errors generated.
rm: __libcheck.s: No such file or directory
make[2]: *** [src/ansi-c/library-check.stamp] Error 1
make[1]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
make: *** [all] Error 2


==> Formula
Path: /opt/homebr

Check failure on line 28 in Formula/c/cbmc.rb

View workflow job for this annotation

GitHub Actions / macOS 13-arm64

`brew install --verbose --formula --build-bottle cbmc` failed on macOS Ventura (13) on Apple Silicon! 

Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/mman.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/netdb.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/process.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/pthread_lib.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/pwd.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/random.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/semaphore.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/setjmp.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/signal.c
Checking /tmp/cbmc-20240919-17427-zkf8jq/src/ansi-c/library/stdio.c
__libcheck.c:1138:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1139:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1196:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1197:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1342:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1343:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1386:55: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
                                                   ~~~^~~~~~~~
__libcheck.c:1387:34: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(arg.__stack))
                              ~~~^~~~~~~~
__libcheck.c:1831:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
                                                   ~~^~~~~~~~
__libcheck.c:1832:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(ap.__stack))
                              ~~^~~~~~~~
__libcheck.c:1837:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
                                                                ~~^~~~~~~~
__libcheck.c:1891:54: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
                                                   ~~^~~~~~~~
__libcheck.c:1892:33: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
        __CPROVER_OBJECT_SIZE(ap.__stack))
                              ~~^~~~~~~~
__libcheck.c:1897:67: error: member reference base type 'va_list' (aka 'char *') is not a structure or union
      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
                                                                ~~^~~~~~~~
14 errors generated.
rm: __libcheck.s: No such file or directory
make[2]: *** [src/ansi-c/library-check.stamp] Error 1
make[1]: *** [src/ansi-c/CMakeFiles/ansi-c.dir/all] Error 2
make: *** [all] Error 2


==> Formula
Path: /opt/homebr
# Fixes: *** No rule to make target 'bin/goto-gcc',
# needed by '/tmp/cbmc-20240525-215493-ru4krx/regression/goto-gcc/archives/libour_archive.a'. Stop.
Expand Down

0 comments on commit d5d3359

Please sign in to comment.