Index | Thread | Search

From:
Yozo TODA <yozo@v007.vaio.ne.jp>
Subject:
Re: UPDATE: cbmc-6.7.1
To:
Rafael Sadowski <rafael@sizeofvoid.org>
Cc:
Mages Simon <mages.simon@googlemail.com>, ports@openbsd.org
Date:
Wed, 16 Jul 2025 04:36:34 +0900

Download raw body.

Thread
> Date: Fri, 11 Jul 2025 21:29:19 +0200
> From: Rafael Sadowski <rafael@sizeofvoid.org>
> Subject: UPDATE: cbmc-6.7.1
> Message-ID: <yjx2wmp4xb5zjtg6yksjkell264cn3afj3s73snpe2xyyw7qz3@hn4gpg3xn6w2>
> 
> Update cbmc-6.7.1. Tested on amd64. The motivation was to fix the
> build with upcoming libc++19. Looks like upstream fixed it by:
> https://github.com/diffblue/cbmc/pull/5277
>
> So I decided to update the port instead backporting the fixes.

I found the diff misses to package cbmc executable.
maybe the problem is here...

> --- Makefile	21 Sep 2023 09:49:49 -0000	1.16
> +++ Makefile	11 Jul 2025 19:26:42 -0000
> @@ -2,13 +2,12 @@ COMMENT =	Bounded Model Checker for C an
>  
........
> +BIN_LIST =	crangler goto-analyzer goto-cc goto-diff goto-harness \
> +		goto-inspect goto-instrument goto-synthesizer
> +

"cbmc" should be added to this list.

    +BIN_LIST =	crangler goto-analyzer goto-cc goto-diff goto-harness \
    +		goto-inspect goto-instrument goto-synthesizer cbmc
    +

with PLIST updated, I confirmed on amd64 that the package includes cbmc executable
and man page cbmc.1, and it works on some simple programs.

and one more comment, I found "test" target fails.
${WRKDIST}/regression/ appears to contain test files and
I suppose "do-test" target should be added:

    do-test:
    	cd ${WRKDIST}/regression/ && ${GMAKE} ${TEST_TARGET}

(sorry I don't confirm this do-test target works or not...)

-- yozo.