Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

cbmc 6.3.0 #191209

Closed
wants to merge 1 commit into from
Closed

cbmc 6.3.0 #191209

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 2 additions & 9 deletions Formula/c/cbmc.rb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
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,14 +25,7 @@

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.
ENV.deparallelize
Expand Down
Loading