Date: Fri, 02 Feb 2024 01:05:00 +0100 From: Daniel Engberg <daniel.engberg.lists@pyret.net> To: Olivier Cochard <olivier@FreeBSD.org> Cc: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: Re: git: 7f087b720e52 - main - devel/cbmc: add new port Message-ID: <379c7ddb410058469dcda4f67b45caa9@mail.infomaniak.com> In-Reply-To: <202402011755.411Ht9G8016149@gitrepo.freebsd.org> References: <202402011755.411Ht9G8016149@gitrepo.freebsd.org>
next in thread | previous in thread | raw e-mail | index | archive | help
--_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_ Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable On 2024-02-01T18:55:09.000+01:00, Olivier Cochard <olivier@FreeBSD.org> w= rote: >=C2=A0The=C2=A0branch=C2=A0main=C2=A0has=C2=A0been=C2=A0updated= =C2=A0by=C2=A0olivier: >=C2=A0 >=C2=A0URL:=C2=A0https://cgit.FreeBSD.or= g/ports/commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef >=C2=A0 >= =C2=A0commit=C2=A07f087b720e52d51b22db0da2d7565418a0e428ef >=C2=A0 >= =C2=A0Author:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivi= er@FreeBSD.org> >=C2=A0 >=C2=A0AuthorDate:=C2=A02024-02-01=C2=A017:50:0= 2=C2=A0+0000 >=C2=A0 >=C2=A0Commit:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivie= r=C2=A0Cochard=C2=A0<olivier@FreeBSD.org> >=C2=A0 >=C2=A0CommitDate:= =C2=A02024-02-01=C2=A017:53:55=C2=A0+0000 >=C2=A0 >=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0devel/cbmc:=C2=A0add=C2=A0new=C2=A0port >=C2=A0 >=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Boun= ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs= >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbm= c >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 >=C2=A0 >=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0Sponsored=C2=A0by:=C2=A0=C2=A0=C2=A0Netflix >=C2=A0 >= =C2=A0--- >=C2=A0 >=C2=A0=C2=A0devel/Makefile=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A01= =C2=A0+ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/Makefile=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A046=C2=A0+++++++++++++++++ >=C2=A0 = >=C2=A0=C2=A0devel/cbmc/distinfo=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0|=C2=A0=C2=A05=C2=A0++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-= 2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0|=C2=A020=C2=A0++++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-mini= sat-2.2.1_minisat_core_SolverTypes.h=C2=A0|=C2=A059=C2=A0++++++++++++++++++= ++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_mtl_IntTypes.= h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A012=C2=A0+++++ >=C2=A0 >=C2=A0= =C2=A0.../files/patch-minisat-2.2.1_minisat_mtl_Vec.h=C2=A0=C2=A0=C2=A0= =C2=A0|=C2=A016=C2=A0++++++ >=C2=A0 >=C2=A0=C2=A0.../files/patch-minisa= t-2.2.1_minisat_mtl_XAlloc.h=C2=A0|=C2=A019=C2=A0+++++++ >=C2=A0 >= =C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_simp_SimpSolver.cc=C2=A0[http:/= /SimpSolver.cc]=C2=A0|=C2=A037=C2=A0++++++++++++++ >=C2=A0 >=C2=A0= =C2=A0.../patch-minisat-2.2.1_minisat_utils_Options.cc=C2=A0[http://Options= .cc]=C2=A0=C2=A0=C2=A0|=C2=A015=C2=A0++++++ >=C2=A0 >=C2=A0=C2=A0.../pa= tch-minisat-2.2.1_minisat_utils_Options.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A030= =C2=A0+++++++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_= utils_ParseUtils.h=C2=A0|=C2=A033=C2=A0++++++++++++ >=C2=A0 >=C2=A0= =C2=A0.../patch-minisat-2.2.1_minisat_utils_System.h=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0|=C2=A011=C2=A0++++ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/files/p= atch-src_common=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0++++ >= =C2=A0 >=C2=A0=C2=A0.../files/patch-src_solvers_sat_external__sat.cpp= =C2=A0=C2=A0|=C2=A013=C2=A0+++++ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/files/= patch-src_util_optional.h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0|=C2=A029=C2=A0+++++++++++ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/pkg= -descr=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A07=C2=A0+++ >= =C2=A0 >=C2=A0=C2=A0devel/cbmc/pkg-plist=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0|=C2=A023=C2=A0+++++++++ >=C2=A0 >=C2=A0=C2=A018=C2=A0files= =C2=A0changed,=C2=A0387=C2=A0insertions(+) >=C2=A0 >=C2=A0diff=C2=A0--g= it=C2=A0a/devel/Makefile=C2=A0b/devel/Makefile >=C2=A0 >=C2=A0index= =C2=A04da71e0953a1..51481c8a3aca=C2=A0100644 >=C2=A0 >=C2=A0---=C2= =A0a/devel/Makefile >=C2=A0 >=C2=A0+++=C2=A0b/devel/Makefile >=C2= =A0 >=C2=A0@@=C2=A0-351,6=C2=A0+351,7=C2=A0@@ >=C2=A0 >=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0catch2 >=C2=A0 >=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbang >=C2=A0 >= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbfmt >=C2= =A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbmc >=C2= =A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cbrowser= >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0cc6= 5 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+=3D=C2= =A0ccache >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/Makefile= =C2=A0b/devel/cbmc/Makefile >=C2=A0 >=C2=A0new=C2=A0file=C2=A0mode= =C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000000000000..c7f7b3650e63 >= =C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc= /Makefile >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,46=C2=A0@@ >=C2=A0 >= =C2=A0+PORTNAME=3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc >=C2=A0 >=C2=A0+PORTVERS= ION=3D=C2=A0=C2=A0=C2=A0=C2=A05.95.1 >=C2=A0 >=C2=A0+DISTVERSIONPREFIX= =3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc- >=C2=A0 >=C2=A0+CATEGORIES=3D=C2=A0= =C2=A0=C2=A0=C2=A0devel >=C2=A0 >=C2=A0+MASTER_SITES=3D=C2=A0=C2=A0= =C2=A0=C2=A0DEBIAN/pool/main/m/minisat2:minisat >=C2=A0 >=C2=A0+DISTFIL= ES=3D=C2=A0=C2=A0=C2=A0=C2=A0minisat2_2.2.1.orig.tar.gz:minisat >=C2= =A0 >=C2=A0+ >=C2=A0 >=C2=A0+MAINTAINER=3D=C2=A0=C2=A0=C2=A0=C2=A0oli= vier@FreeBSD.org >=C2=A0 >=C2=A0+COMMENT=3D=C2=A0=C2=A0=C2=A0=C2=A0Boun= ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs= >=C2=A0 >=C2=A0+WWW=3D=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0https://github.com/diffblue/cbmc >=C2=A0 >=C2=A0+ >=C2=A0 >= =C2=A0+LICENSE=3D=C2=A0=C2=A0=C2=A0=C2=A0BSD4CLAUSE >=C2=A0 >=C2=A0+LIC= ENSE_FILE=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/LICENSE >=C2=A0 >=C2= =A0+ >=C2=A0 >=C2=A0+BUILD_DEPENDS=3D=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBAS= E}/bin/flex:textproc/flex >=C2=A0 >=C2=A0+RUN_DEPENDS=3D=C2=A0=C2=A0= =C2=A0=C2=A0${LOCALBASE}/bin/cvc5:math/cvc5=C2=A0\ >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/z3:math/z3= >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+USES=3D=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0gmake=C2=A0bison=C2=A0python=C2=A0shebangfix >= =C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+USE_GITHUB=3D=C2=A0=C2=A0=C2=A0=C2= =A0yes >=C2=A0 >=C2=A0+GH_ACCOUNT=3D=C2=A0=C2=A0=C2=A0=C2=A0diffblue = >=C2=A0 >=C2=A0+SHEBANG_FILES=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/scripts= /ls_parse.py=C2=A0[http://parse.py] >=C2=A0 >=C2=A0+WRKSRC_minisat=3D= =C2=A0=C2=A0=C2=A0=C2=A0${WRKDIR}/minisat2-2.2.1 >=C2=A0 >=C2=A0+ >= =C2=A0 >=C2=A0+post-patch: >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2= =A0@${REINPLACE_CMD}=C2=A0-e=C2=A0's|.*git=C2=A0describe=C2=A0--tags.*|GIT_= INFO=C2=A0=3D=C2=A0${PORTNAME}-${PORTVERSION}|'=C2=A0\ >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC}/src/util/Make= file >=C2=A0 >=C2=A0+post-extract: >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0@${MV}=C2=A0${WRKSRC_minisat}=C2=A0${WRKSRC}/minisat-2.2.1 >= =C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+do-build: >=C2=A0 >=C2=A0+=C2= =A0=C2=A0=C2=A0=C2=A0@${MKDIR}=C2=A0${STAGEDIR} >=C2=A0 >=C2=A0+=C2= =A0=C2=A0=C2=A0=C2=A0cd=C2=A0${WRKSRC}=C2=A0&&=C2=A0${GMAKE}=C2=A0-C=C2= =A0src=C2=A0-j${MAKE_JOBS_NUMBER} >=C2=A0 >=C2=A0+ >=C2=A0 >=C2= =A0+do-install: >=C2=A0 >=C2=A0+.=C2=A0=C2=A0for=C2=A0x=C2=A0in=C2= =A0cbmc=C2=A0crangler=C2=A0goto-analyzer=C2=A0goto-cc=C2=A0goto-diff=C2= =A0goto-instrument=C2=A0\ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0goto-= inspect=C2=A0goto-harness=C2=A0goto-synthesizer=C2=A0symtab2gb >=C2=A0 = >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_PROGRAM}=C2=A0${WRKSRC}/src/${x}/= ${x}=C2=A0${STAGEDIR}${PREFIX}/bin/ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0${INSTALL_MAN}=C2=A0${WRKSRC}/doc/man/${x}.1=C2=A0${STAGEDIR}${PRE= FIX}/share/man/man1/ >=C2=A0 >=C2=A0+.=C2=A0=C2=A0endfor >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}= ${PREFIX}/bin/goto-gcc >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}= =C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}${PREFIX}/bin/goto-ld >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_SCRIPT}=C2=A0${WRKSRC}/scripts/ls_= parse.py=C2=A0[http://parse.py]=C2=A0${STAGEDIR}${PREFIX}/bin/ >=C2=A0 = >=C2=A0+ >=C2=A0 >=C2=A0+.include=C2=A0<bsd.port.mk>=C2=A0[http://bsd.p= ort.mk>]; >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/distinfo= =C2=A0b/devel/cbmc/distinfo >=C2=A0 >=C2=A0new=C2=A0file=C2=A0mode= =C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000000000000..f3e6d1161c6a >= =C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc= /distinfo >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,5=C2=A0@@ >=C2=A0 >= =C2=A0+TIMESTAMP=C2=A0=3D=C2=A01706723199 >=C2=A0 >=C2=A0+SHA256=C2= =A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D=C2=A0e54afa3c192c1753bc8075c0c7e12= 6d5c495d9066e3f90a2588091149ac9ca40 >=C2=A0 >=C2=A0+SIZE=C2=A0(minisat2= _2.2.1.orig.tar.gz)=C2=A0=3D=C2=A044229 >=C2=A0 >=C2=A0+SHA256=C2=A0(di= ffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)=C2=A0=3D=C2=A0fdc1e862752430f8d069eb2f9= c33dcd05078cf955bbc900e2cc840bcb01b3783 >=C2=A0 >=C2=A0+SIZE=C2=A0(diff= blue-cbmc-cbmc-5.95.1_GH0.tar.gz)=C2=A0=3D=C2=A09073428 >=C2=A0 >=C2= =A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core= _Solver.cc=C2=A0[http://Solver.cc]=C2=A0b/devel/cbmc/files/patch-minisat-2.= 2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc] >=C2=A0 >=C2=A0new= =C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000000000000= ..c15c2f12fb0a >=C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++= =C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2= =A0[http://Solver.cc] >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,20=C2=A0@@ = >=C2=A0 >=C2=A0+---=C2=A0minisat-2.2.1/minisat/core/Solver.cc.orig=C2= =A0[http://Solver.cc.orig]=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17= =C2=A0UTC >=C2=A0 >=C2=A0++++=C2=A0minisat-2.2.1/minisat/core/Solver.cc= =C2=A0[http://Solver.cc] >=C2=A0 >=C2=A0+@@=C2=A0-210,7=C2=A0+210,7= =C2=A0@@=C2=A0void=C2=A0Solver::cancelUntil(int=C2=A0level)=C2=A0{ >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for= =C2=A0(int=C2=A0c=C2=A0=3D=C2=A0trail.size()-1;=C2=A0c=C2=A0>=3D=C2= =A0trail_lim[level];=C2=A0c--){ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Var=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0x=C2=A0=C2=A0=3D=C2=A0var(trail[c]); >=C2= =A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0assigns=C2=A0[x]=C2=A0=3D=C2=A0l_Undef; >=C2=A0 >= =C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0if=C2=A0(phase_saving=C2=A0>=C2=A01=C2=A0||=C2=A0(phase_saving= =C2=A0=3D=3D=C2=A01)=C2=A0&&=C2=A0c=C2=A0>=C2=A0trail_lim.last()) >=C2= =A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0if=C2=A0(phase_saving=C2=A0>=C2=A01=C2=A0||=C2=A0((phase_sav= ing=C2=A0=3D=3D=C2=A01)=C2=A0&&=C2=A0c=C2=A0>=C2=A0trail_lim.last())) >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0polarity[x]=C2=A0=3D=C2= =A0sign(trail[c]); >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0insertVarOrder(x);=C2=A0} >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0qhea= d=C2=A0=3D=C2=A0trail_lim[level]; >=C2=A0 >=C2=A0+@@=C2=A0-666,7=C2= =A0+666,7=C2=A0@@=C2=A0lbool=C2=A0Solver::search(int=C2=A0nof_conflicts) = >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0}else{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NO= =C2=A0CONFLICT >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(nof_conflicts=C2=A0>=3D= =C2=A00=C2=A0&&=C2=A0conflictC=C2=A0>=3D=C2=A0nof_conflicts=C2=A0||= =C2=A0!withinBudget()){ >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0((nof_conflicts=C2= =A0>=3D=C2=A00=C2=A0&&=C2=A0conflictC=C2=A0>=3D=C2=A0nof_conflicts)= =C2=A0||=C2=A0!withinBudget()){ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0//=C2=A0Reached=C2=A0bound=C2=A0on=C2=A0number=C2=A0of=C2=A0con= flicts: >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0progress_estima= te=C2=A0=3D=C2=A0progressEstimate(); >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0cancelUntil(0); >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/de= vel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h=C2=A0b/devel/= cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h >=C2=A0 >= =C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000= 000000000..fa26c6372b36 >=C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >= =C2=A0+++=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTy= pes.h >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,59=C2=A0@@ >=C2=A0 >= =C2=A0+---=C2=A0minisat-2.2.1/minisat/core/SolverTypes.h.orig=C2=A0=C2= =A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC >=C2=A0 >=C2=A0++++= =C2=A0minisat-2.2.1/minisat/core/SolverTypes.h >=C2=A0 >=C2=A0+@@=C2= =A0-47,7=C2=A0+47,7=C2=A0@@=C2=A0struct=C2=A0Lit=C2=A0{ >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0int=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0x; >= =C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0//=C2=A0Use=C2=A0this=C2=A0as=C2=A0a=C2=A0constructor: >=C2=A0 >= =C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0Lit=C2=A0mkLit(Var=C2=A0var,= =C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false); >=C2=A0 >=C2=A0++=C2=A0= =C2=A0=C2=A0=C2=A0//friend=C2=A0Lit=C2=A0mkLit(Var=C2=A0var,=C2=A0bool= =C2=A0sign=C2=A0=3D=C2=A0false); >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operator=C2=A0=3D=3D=C2= =A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2=A0=3D=3D=C2=A0p.x;= =C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operato= r=C2=A0!=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2=A0!= =3D=C2=A0p.x;=C2=A0} >=C2=A0 >=C2=A0+@@=C2=A0-55,7=C2=A0+55,7=C2=A0@@= =C2=A0struct=C2=A0Lit=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0}; >=C2=A0 >= =C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+-inline=C2= =A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Var=C2=A0var,= =C2=A0bool=C2=A0sign)=C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var= =C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0} >= =C2=A0 >=C2=A0++inline=C2=A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false)= =C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var=C2=A0+=C2=A0var=C2= =A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0} >=C2=A0 >=C2=A0+=C2= =A0inline=C2=A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0~(Lit=C2=A0p)=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^=C2=A01;=C2=A0return= =C2=A0q;=C2=A0} >=C2=A0 >=C2=A0+=C2=A0inline=C2=A0=C2=A0Lit=C2=A0=C2= =A0operator=C2=A0^(Lit=C2=A0p,=C2=A0bool=C2=A0b)=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^=C2=A0(unsi= gned=C2=A0int)b;=C2=A0return=C2=A0q;=C2=A0} >=C2=A0 >=C2=A0+=C2=A0inlin= e=C2=A0=C2=A0bool=C2=A0sign=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Lit=C2= =A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0{=C2=A0return=C2=A0p.x=C2=A0&=C2=A01;=C2=A0} >=C2=A0 = >=C2=A0+@@=C2=A0-127,7=C2=A0+127,10=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{= >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0unsigned=C2=A0has_extra=C2=A0:=C2=A01; >=C2=A0 >=C2=A0+=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0reloced=C2=A0= =C2=A0=C2=A0:=C2=A01; >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0size=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0:=C2=A027;=C2=A0}=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0header; >=C2=A0 >=C2=A0++#include=C2=A0<util/pr= agma_push.def> >=C2=A0 >=C2=A0++#include=C2=A0<util/pragma_wzero_length= _array.def> >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0union=C2= =A0{=C2=A0Lit=C2=A0lit;=C2=A0float=C2=A0act;=C2=A0uint32_t=C2=A0abs;=C2= =A0CRef=C2=A0rel;=C2=A0}=C2=A0data[0]; >=C2=A0 >=C2=A0++#include=C2= =A0<util/pragma_pop.def> >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0class=C2=A0ClauseAllocator; >= =C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+@@=C2=A0-142,11=C2=A0+145,12= =C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D= =C2=A00;=C2=A0i=C2=A0<=C2=A0ps.size();=C2=A0i++)=C2=A0 >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0ps[i]; >=C2=A0 >=C2=A0+=C2=A0 >= =C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2= =A0(header.has_extra) >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)=C2=A0{ >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0if=C2=A0(header.learnt) >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2=A00; >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0else >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0calcAb= straction(); >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0} >=C2= =A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//= =C2=A0NOTE:=C2=A0This=C2=A0constructor=C2=A0cannot=C2=A0be=C2=A0used=C2= =A0directly=C2=A0(doesn't=C2=A0allocate=C2=A0enough=C2=A0memory). >=C2= =A0 >=C2=A0+@@=C2=A0-157,11=C2=A0+161,12=C2=A0@@=C2=A0class=C2=A0Clause= =C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D=C2=A00;=C2=A0i=C2=A0<=C2=A0from.s= ize();=C2=A0i++) >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0from= [i]; >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra) >=C2=A0 >= =C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has= _extra)=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.learnt) >=C2= =A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D= =C2=A0from.data[header.size]=C2=A0[http://from.data[header.size]].act; >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0else=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0data[header.size].abs=C2=A0=3D=C2=A0from.data[header.size]= =C2=A0[http://from.data[header.size]].abs; >=C2=A0 >=C2=A0++=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0} >=C2=A0 >=C2=A0+=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0} >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+= =C2=A0public: >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/pa= tch-minisat-2.2.1_minisat_mtl_IntTypes.h=C2=A0b/devel/cbmc/files/patch-mini= sat-2.2.1_minisat_mtl_IntTypes.h >=C2=A0 >=C2=A0new=C2=A0file=C2=A0mode= =C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000000000000..d8c9ddedb701 >= =C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc= /files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h >=C2=A0 >=C2=A0@@= =C2=A0-0,0=C2=A0+1,12=C2=A0@@ >=C2=A0 >=C2=A0+---=C2=A0minisat-2.2.1/mi= nisat/mtl/IntTypes.h.orig=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17= =C2=A0UTC >=C2=A0 >=C2=A0++++=C2=A0minisat-2.2.1/minisat/mtl/IntTypes.h= >=C2=A0 >=C2=A0+@@=C2=A0-31,7=C2=A0+31,9=C2=A0@@=C2=A0OF=C2=A0OR=C2= =A0IN=C2=A0CONNECTION=C2=A0WITH=C2=A0THE=C2=A0SOFTWARE=C2=A0OR=C2=A0THE= =C2=A0USE=C2=A0OR=C2=A0OT >=C2=A0 >=C2=A0+=C2=A0#else >=C2=A0 >= =C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0#=C2=A0=C2=A0=C2=A0include=C2=A0<st= dint.h> >=C2=A0 >=C2=A0++#ifndef=C2=A0_MSC_VER >=C2=A0 >=C2=A0+= =C2=A0#=C2=A0=C2=A0=C2=A0include=C2=A0<inttypes.h> >=C2=A0 >=C2=A0++#en= dif >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0The=C2=A0branch= =C2=A0main=C2=A0has=C2=A0been=C2=A0updated=C2=A0by=C2=A0olivier: >=C2= =A0 >=C2=A0URL:=C2=A0https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b72= 0e52d51b22db0da2d7565418a0e428ef >=C2=A0 >=C2=A0commit=C2=A07f087b720e5= 2d51b22db0da2d7565418a0e428ef >=C2=A0 >=C2=A0Author:=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivier@FreeBSD.org> >=C2=A0 = >=C2=A0AuthorDate:=C2=A02024-02-01=C2=A017:50:02=C2=A0+0000 >=C2=A0 >= =C2=A0Commit:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Olivier=C2=A0Cochard=C2=A0<olivi= er@FreeBSD.org> >=C2=A0 >=C2=A0CommitDate:=C2=A02024-02-01=C2=A017:53:5= 5=C2=A0+0000 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0devel/cbmc:=C2= =A0add=C2=A0new=C2=A0port >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 >= =C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Bounded=C2=A0Model=C2=A0Checker= =C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs >=C2=A0 >=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbmc >=C2=A0 >=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0Spon= sored=C2=A0by:=C2=A0=C2=A0=C2=A0Netflix >=C2=A0 >=C2=A0--- >=C2=A0 = >=C2=A0=C2=A0devel/Makefile=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A01=C2=A0+ >=C2=A0 >=C2= =A0=C2=A0devel/cbmc/Makefile=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0|=C2=A046=C2=A0+++++++++++++++++ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/= distinfo=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A0=C2=A05= =C2=A0++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_core_Solv= er.cc=C2=A0[http://Solver.cc]=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A020=C2= =A0++++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_core_S= olverTypes.h=C2=A0|=C2=A059=C2=A0++++++++++++++++++++++ >=C2=A0 >=C2= =A0=C2=A0.../patch-minisat-2.2.1_minisat_mtl_IntTypes.h=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0|=C2=A012=C2=A0+++++ >=C2=A0 >=C2=A0=C2=A0.../files/patc= h-minisat-2.2.1_minisat_mtl_Vec.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A016=C2=A0+++= +++ >=C2=A0 >=C2=A0=C2=A0.../files/patch-minisat-2.2.1_minisat_mtl_XAll= oc.h=C2=A0|=C2=A019=C2=A0+++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat= -2.2.1_minisat_simp_SimpSolver.cc=C2=A0[http://SimpSolver.cc]=C2=A0|=C2= =A037=C2=A0++++++++++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_= minisat_utils_Options.cc=C2=A0[http://Options.cc]=C2=A0=C2=A0=C2=A0|=C2= =A015=C2=A0++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_= utils_Options.h=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A030=C2=A0+++++++++++ >=C2= =A0 >=C2=A0=C2=A0.../patch-minisat-2.2.1_minisat_utils_ParseUtils.h=C2= =A0|=C2=A033=C2=A0++++++++++++ >=C2=A0 >=C2=A0=C2=A0.../patch-minisat-2= .2.1_minisat_utils_System.h=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0+++= + >=C2=A0 >=C2=A0=C2=A0devel/cbmc/files/patch-src_common=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0|=C2=A011=C2=A0++++ >=C2=A0 >=C2=A0=C2=A0.../fi= les/patch-src_solvers_sat_external__sat.cpp=C2=A0=C2=A0|=C2=A013=C2=A0+++++= >=C2=A0 >=C2=A0=C2=A0devel/cbmc/files/patch-src_util_optional.h=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A029=C2=A0+++++++++= ++ >=C2=A0 >=C2=A0=C2=A0devel/cbmc/pkg-descr=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0|=C2=A0=C2=A07=C2=A0+++ >=C2=A0 >=C2=A0=C2=A0devel/cb= mc/pkg-plist=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0|=C2=A023=C2=A0++++++= +++ >=C2=A0 >=C2=A0=C2=A018=C2=A0files=C2=A0changed,=C2=A0387=C2=A0inse= rtions(+) >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/Makefile=C2=A0b/d= evel/Makefile >=C2=A0 >=C2=A0index=C2=A04da71e0953a1..51481c8a3aca= =C2=A0100644 >=C2=A0 >=C2=A0---=C2=A0a/devel/Makefile >=C2=A0 >= =C2=A0+++=C2=A0b/devel/Makefile >=C2=A0 >=C2=A0@@=C2=A0-351,6=C2=A0+351= ,7=C2=A0@@ >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR=C2=A0+= =3D=C2=A0catch2 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR= =C2=A0+=3D=C2=A0cbang >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBD= IR=C2=A0+=3D=C2=A0cbfmt >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0SUBDIR= =C2=A0+=3D=C2=A0cbmc >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0SUBDI= R=C2=A0+=3D=C2=A0cbrowser >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0SUBDIR=C2=A0+=3D=C2=A0cc65 >=C2=A0 >=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0SUBDIR=C2=A0+=3D=C2=A0ccache >=C2=A0 >=C2=A0diff=C2=A0--git= =C2=A0a/devel/cbmc/Makefile=C2=A0b/devel/cbmc/Makefile >=C2=A0 >=C2= =A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000000= 000000..c7f7b3650e63 >=C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >= =C2=A0+++=C2=A0b/devel/cbmc/Makefile >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2= =A0+1,46=C2=A0@@ >=C2=A0 >=C2=A0+PORTNAME=3D=C2=A0=C2=A0=C2=A0=C2=A0cbm= c >=C2=A0 >=C2=A0+PORTVERSION=3D=C2=A0=C2=A0=C2=A0=C2=A05.95.1 >= =C2=A0 >=C2=A0+DISTVERSIONPREFIX=3D=C2=A0=C2=A0=C2=A0=C2=A0cbmc- >= =C2=A0 >=C2=A0+CATEGORIES=3D=C2=A0=C2=A0=C2=A0=C2=A0devel >=C2=A0 >= =C2=A0+MASTER_SITES=3D=C2=A0=C2=A0=C2=A0=C2=A0DEBIAN/pool/main/m/minisat2:m= inisat >=C2=A0 >=C2=A0+DISTFILES=3D=C2=A0=C2=A0=C2=A0=C2=A0minisat2_2.2= .1.orig.tar.gz:minisat >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+MAINTAINER= =3D=C2=A0=C2=A0=C2=A0=C2=A0olivier@FreeBSD.org >=C2=A0 >=C2=A0+COMMENT= =3D=C2=A0=C2=A0=C2=A0=C2=A0Bounded=C2=A0Model=C2=A0Checker=C2=A0for=C2= =A0C=C2=A0and=C2=A0C++=C2=A0programs >=C2=A0 >=C2=A0+WWW=3D=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0https://github.com/diffblue/cbmc >= =C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+LICENSE=3D=C2=A0=C2=A0=C2=A0=C2=A0BSD= 4CLAUSE >=C2=A0 >=C2=A0+LICENSE_FILE=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKSRC= }/LICENSE >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+BUILD_DEPENDS=3D=C2= =A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/flex:textproc/flex >=C2=A0 >= =C2=A0+RUN_DEPENDS=3D=C2=A0=C2=A0=C2=A0=C2=A0${LOCALBASE}/bin/cvc5:math/cvc= 5=C2=A0\ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0${LOCALBASE}/bin/z3:math/z3 >=C2=A0 >=C2=A0+ >=C2=A0 >=C2= =A0+USES=3D=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0gmake=C2=A0bison= =C2=A0python=C2=A0shebangfix >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+USE_G= ITHUB=3D=C2=A0=C2=A0=C2=A0=C2=A0yes >=C2=A0 >=C2=A0+GH_ACCOUNT=3D=C2= =A0=C2=A0=C2=A0=C2=A0diffblue >=C2=A0 >=C2=A0+SHEBANG_FILES=3D=C2=A0= =C2=A0=C2=A0=C2=A0${WRKSRC}/scripts/ls_parse.py=C2=A0[http://parse.py] >= =C2=A0 >=C2=A0+WRKSRC_minisat=3D=C2=A0=C2=A0=C2=A0=C2=A0${WRKDIR}/minisat= 2-2.2.1 >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+post-patch: >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${REINPLACE_CMD}=C2=A0-e=C2=A0's|.*git= =C2=A0describe=C2=A0--tags.*|GIT_INFO=C2=A0=3D=C2=A0${PORTNAME}-${PORTVERSI= ON}|'=C2=A0\ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0${WRKSRC}/src/util/Makefile >=C2=A0 >=C2=A0+post-extract: >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${MV}=C2=A0${WRKSRC_minisat}= =C2=A0${WRKSRC}/minisat-2.2.1 >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+do-b= uild: >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0@${MKDIR}=C2=A0${STAGEDIR= } >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0cd=C2=A0${WRKSRC}=C2=A0&&= =C2=A0${GMAKE}=C2=A0-C=C2=A0src=C2=A0-j${MAKE_JOBS_NUMBER} >=C2=A0 >= =C2=A0+ >=C2=A0 >=C2=A0+do-install: >=C2=A0 >=C2=A0+.=C2=A0=C2= =A0for=C2=A0x=C2=A0in=C2=A0cbmc=C2=A0crangler=C2=A0goto-analyzer=C2=A0goto-= cc=C2=A0goto-diff=C2=A0goto-instrument=C2=A0\ >=C2=A0 >=C2=A0+=C2=A0= =C2=A0=C2=A0=C2=A0goto-inspect=C2=A0goto-harness=C2=A0goto-synthesizer= =C2=A0symtab2gb >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_PROGR= AM}=C2=A0${WRKSRC}/src/${x}/${x}=C2=A0${STAGEDIR}${PREFIX}/bin/ >=C2= =A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL_MAN}=C2=A0${WRKSRC}/doc/man= /${x}.1=C2=A0${STAGEDIR}${PREFIX}/share/man/man1/ >=C2=A0 >=C2=A0+.= =C2=A0=C2=A0endfor >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2= =A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}${PREFIX}/bin/goto-gcc >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${LN}=C2=A0-sf=C2=A0goto-cc=C2=A0${STAGEDIR}= ${PREFIX}/bin/goto-ld >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0${INSTALL= _SCRIPT}=C2=A0${WRKSRC}/scripts/ls_parse.py=C2=A0[http://parse.py]=C2=A0${S= TAGEDIR}${PREFIX}/bin/ >=C2=A0 >=C2=A0+ >=C2=A0 >=C2=A0+.include= =C2=A0<bsd.port.mk>=C2=A0[http://bsd.port.mk>]; >=C2=A0 >=C2=A0diff= =C2=A0--git=C2=A0a/devel/cbmc/distinfo=C2=A0b/devel/cbmc/distinfo >=C2= =A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index= =C2=A0000000000000..f3e6d1161c6a >=C2=A0 >=C2=A0---=C2=A0/dev/null >= =C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/distinfo >=C2=A0 >=C2=A0@@=C2= =A0-0,0=C2=A0+1,5=C2=A0@@ >=C2=A0 >=C2=A0+TIMESTAMP=C2=A0=3D=C2=A017067= 23199 >=C2=A0 >=C2=A0+SHA256=C2=A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D= =C2=A0e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40 >= =C2=A0 >=C2=A0+SIZE=C2=A0(minisat2_2.2.1.orig.tar.gz)=C2=A0=3D=C2=A044229= >=C2=A0 >=C2=A0+SHA256=C2=A0(diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)= =C2=A0=3D=C2=A0fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b= 3783 >=C2=A0 >=C2=A0+SIZE=C2=A0(diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz)= =C2=A0=3D=C2=A09073428 >=C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc= /files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc]= =C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver.cc=C2= =A0[http://Solver.cc] >=C2=A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A010064= 4 >=C2=A0 >=C2=A0index=C2=A0000000000000..c15c2f12fb0a >=C2=A0 >= =C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/files/pat= ch-minisat-2.2.1_minisat_core_Solver.cc=C2=A0[http://Solver.cc] >=C2= =A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,20=C2=A0@@ >=C2=A0 >=C2=A0+---=C2= =A0minisat-2.2.1/minisat/core/Solver.cc.orig=C2=A0[http://Solver.cc.orig]= =C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC >=C2=A0 >= =C2=A0++++=C2=A0minisat-2.2.1/minisat/core/Solver.cc=C2=A0[http://Solver.cc= ] >=C2=A0 >=C2=A0+@@=C2=A0-210,7=C2=A0+210,7=C2=A0@@=C2=A0void=C2=A0Sol= ver::cancelUntil(int=C2=A0level)=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0c=C2=A0=3D= =C2=A0trail.size()-1;=C2=A0c=C2=A0>=3D=C2=A0trail_lim[level];=C2=A0c--){= >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0Var=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0x=C2= =A0=C2=A0=3D=C2=A0var(trail[c]); >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0assigns=C2= =A0[x]=C2=A0=3D=C2=A0l_Undef; >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(phase_saving= =C2=A0>=C2=A01=C2=A0||=C2=A0(phase_saving=C2=A0=3D=3D=C2=A01)=C2=A0&&=C2= =A0c=C2=A0>=C2=A0trail_lim.last()) >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(phase_sav= ing=C2=A0>=C2=A01=C2=A0||=C2=A0((phase_saving=C2=A0=3D=3D=C2=A01)=C2=A0&&= =C2=A0c=C2=A0>=C2=A0trail_lim.last())) >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0polarity[x]=C2=A0=3D=C2=A0sign(trail[c]); >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0insertVarOrder(x);=C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0qhead=C2=A0=3D=C2=A0trail_lim[= level]; >=C2=A0 >=C2=A0+@@=C2=A0-666,7=C2=A0+666,7=C2=A0@@=C2=A0lbool= =C2=A0Solver::search(int=C2=A0nof_conflicts) >=C2=A0 >=C2=A0+=C2=A0 >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0}els= e{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NO=C2=A0CONFLICT >=C2=A0 >=C2= =A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0if=C2=A0(nof_conflicts=C2=A0>=3D=C2=A00=C2=A0&&=C2=A0conflictC= =C2=A0>=3D=C2=A0nof_conflicts=C2=A0||=C2=A0!withinBudget()){ >=C2= =A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0if=C2=A0((nof_conflicts=C2=A0>=3D=C2=A00=C2=A0&&=C2=A0con= flictC=C2=A0>=3D=C2=A0nof_conflicts)=C2=A0||=C2=A0!withinBudget()){ >= =C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0Reached=C2=A0bound= =C2=A0on=C2=A0number=C2=A0of=C2=A0conflicts: >=C2=A0 >=C2=A0+=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0progress_estimate=C2=A0=3D=C2=A0progressEstimate();= >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0cancelUntil(0); >= =C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1= _minisat_core_SolverTypes.h=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_min= isat_core_SolverTypes.h >=C2=A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A0100= 644 >=C2=A0 >=C2=A0index=C2=A0000000000000..fa26c6372b36 >=C2=A0 >= =C2=A0---=C2=A0/dev/null >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/files/pat= ch-minisat-2.2.1_minisat_core_SolverTypes.h >=C2=A0 >=C2=A0@@=C2=A0-0,0= =C2=A0+1,59=C2=A0@@ >=C2=A0 >=C2=A0+---=C2=A0minisat-2.2.1/minisat/core= /SolverTypes.h.orig=C2=A0=C2=A0=C2=A0=C2=A02011-02-21=C2=A013:31:17=C2= =A0UTC >=C2=A0 >=C2=A0++++=C2=A0minisat-2.2.1/minisat/core/SolverTypes.= h >=C2=A0 >=C2=A0+@@=C2=A0-47,7=C2=A0+47,7=C2=A0@@=C2=A0struct=C2=A0Lit= =C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0int=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0x; >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0Use=C2=A0this=C2=A0as=C2=A0a=C2=A0con= structor: >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0friend=C2=A0Lit= =C2=A0mkLit(Var=C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false); >= =C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0//friend=C2=A0Lit=C2=A0mkLit(Var= =C2=A0var,=C2=A0bool=C2=A0sign=C2=A0=3D=C2=A0false); >=C2=A0 >=C2=A0+= =C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0bool=C2=A0operator= =C2=A0=3D=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{=C2=A0return=C2=A0x=C2= =A0=3D=3D=C2=A0p.x;=C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0bool=C2=A0operator=C2=A0!=3D=C2=A0(Lit=C2=A0p)=C2=A0const=C2=A0{= =C2=A0return=C2=A0x=C2=A0!=3D=C2=A0p.x;=C2=A0} >=C2=A0 >=C2=A0+@@=C2= =A0-55,7=C2=A0+55,7=C2=A0@@=C2=A0struct=C2=A0Lit=C2=A0{ >=C2=A0 >=C2= =A0+=C2=A0}; >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0 >= =C2=A0 >=C2=A0+-inline=C2=A0=C2=A0Lit=C2=A0=C2=A0mkLit=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign)=C2=A0{=C2=A0Lit=C2=A0p;= =C2=A0p.x=C2=A0=3D=C2=A0var=C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0ret= urn=C2=A0p;=C2=A0} >=C2=A0 >=C2=A0++inline=C2=A0=C2=A0Lit=C2=A0=C2= =A0mkLit=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0(Var=C2=A0var,=C2=A0bool=C2=A0sign= =C2=A0=3D=C2=A0false)=C2=A0{=C2=A0Lit=C2=A0p;=C2=A0p.x=C2=A0=3D=C2=A0var= =C2=A0+=C2=A0var=C2=A0+=C2=A0(int)sign;=C2=A0return=C2=A0p;=C2=A0} >= =C2=A0 >=C2=A0+=C2=A0inline=C2=A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0~(Lit= =C2=A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2=A0p.x=C2=A0^= =C2=A01;=C2=A0return=C2=A0q;=C2=A0} >=C2=A0 >=C2=A0+=C2=A0inline=C2= =A0=C2=A0Lit=C2=A0=C2=A0operator=C2=A0^(Lit=C2=A0p,=C2=A0bool=C2=A0b)=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{=C2=A0Lit=C2=A0q;=C2=A0q.x=C2=A0=3D=C2= =A0p.x=C2=A0^=C2=A0(unsigned=C2=A0int)b;=C2=A0return=C2=A0q;=C2=A0} >= =C2=A0 >=C2=A0+=C2=A0inline=C2=A0=C2=A0bool=C2=A0sign=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0(Lit=C2=A0p)=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{=C2=A0return=C2=A0p.x=C2= =A0&=C2=A01;=C2=A0} >=C2=A0 >=C2=A0+@@=C2=A0-127,7=C2=A0+127,10=C2= =A0@@=C2=A0class=C2=A0Clause=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2=A0has_extra=C2=A0:=C2= =A01; >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0unsigned=C2=A0reloced=C2=A0=C2=A0=C2=A0:=C2=A01; >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0unsigned=C2= =A0size=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0:=C2=A027;=C2=A0}=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0header; >= =C2=A0 >=C2=A0++#include=C2=A0<util/pragma_push.def> >=C2=A0 >=C2= =A0++#include=C2=A0<util/pragma_wzero_length_array.def> >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0union=C2=A0{=C2=A0Lit=C2=A0lit;=C2=A0floa= t=C2=A0act;=C2=A0uint32_t=C2=A0abs;=C2=A0CRef=C2=A0rel;=C2=A0}=C2=A0data[0]= ; >=C2=A0 >=C2=A0++#include=C2=A0<util/pragma_pop.def> >=C2=A0 >= =C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0friend= =C2=A0class=C2=A0ClauseAllocator; >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >= =C2=A0+@@=C2=A0-142,11=C2=A0+145,12=C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{= >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0for=C2=A0(int=C2=A0i=C2=A0=3D=C2=A00;=C2=A0i=C2=A0<=C2=A0ps.size();= =C2=A0i++)=C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[i].lit=C2=A0=3D=C2=A0ps[i= ]; >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra) >=C2=A0 >=C2= =A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_ex= tra)=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.learnt) >=C2=A0 = >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2= =A00; >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0else >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0calcAbstraction(); >=C2=A0 >=C2=A0++=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0} >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0//=C2=A0NOTE:=C2=A0This=C2=A0constructor=C2= =A0cannot=C2=A0be=C2=A0used=C2=A0directly=C2=A0(doesn't=C2=A0allocate=C2= =A0enough=C2=A0memory). >=C2=A0 >=C2=A0+@@=C2=A0-157,11=C2=A0+161,12= =C2=A0@@=C2=A0class=C2=A0Clause=C2=A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0for=C2=A0(int=C2=A0i=C2=A0=3D= =C2=A00;=C2=A0i=C2=A0<=C2=A0from.size();=C2=A0i++) >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0data[i].lit=C2=A0=3D=C2=A0from[i]; >=C2=A0 >=C2=A0+=C2=A0 >= =C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0if=C2= =A0(header.has_extra) >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0if=C2=A0(header.has_extra)=C2=A0{ >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0if=C2=A0(header.learnt) >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0data[header.size].act=C2=A0=3D=C2=A0from.data[header.size]= =C2=A0[http://from.data[header.size]].act; >=C2=A0 >=C2=A0+=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0else= =C2=A0 >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0data[header.size].= abs=C2=A0=3D=C2=A0from.data[header.size]=C2=A0[http://from.data[header.size= ]].abs; >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0} >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0} >=C2=A0 >= =C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0public: >=C2=A0 >=C2=A0diff= =C2=A0--git=C2=A0a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntType= s.h=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h >= =C2=A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0inde= x=C2=A0000000000000..d8c9ddedb701 >=C2=A0 >=C2=A0---=C2=A0/dev/null >= =C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl= _IntTypes.h >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,12=C2=A0@@ >=C2=A0 = >=C2=A0+---=C2=A0minisat-2.2.1/minisat/mtl/IntTypes.h.orig=C2=A0=C2=A0= =C2=A0=C2=A02011-02-21=C2=A013:31:17=C2=A0UTC >=C2=A0 >=C2=A0++++=C2= =A0minisat-2.2.1/minisat/mtl/IntTypes.h >=C2=A0 >=C2=A0+@@=C2=A0-31,7= =C2=A0+31,9=C2=A0@@=C2=A0OF=C2=A0OR=C2=A0IN=C2=A0CONNECTION=C2=A0WITH=C2= =A0THE=C2=A0SOFTWARE=C2=A0OR=C2=A0THE=C2=A0USE=C2=A0OR=C2=A0OT >=C2=A0 = >=C2=A0+=C2=A0#else >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2= =A0#=C2=A0=C2=A0=C2=A0include=C2=A0<stdint.h> >=C2=A0 >=C2=A0++#ifndef= =C2=A0_MSC_VER >=C2=A0 >=C2=A0+=C2=A0#=C2=A0=C2=A0=C2=A0include=C2= =A0<inttypes.h> >=C2=A0 >=C2=A0++#endif >=C2=A0 >=C2=A0+=C2=A0 >= =C2=A0 >=C2=A0+=C2=A0#endiffile=C2=A0mode=C2=A0100644 >=C2=A0 >=C2= =A0index=C2=A0000000000000..f0dd61cd9963 >=C2=A0 >=C2=A0---=C2=A0/dev/n= ull >=C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/files/patch-src_solvers_sat_ex= ternal__sat.cpp >=C2=A0 >=C2=A0@@=C2=A0-0,0=C2=A0+1,13=C2=A0@@ >= =C2=A0 >=C2=A0+---=C2=A0src/solvers/sat/external_sat.cpp.orig=C2=A0=C2= =A0=C2=A0=C2=A02023-10-30=C2=A012:11:18=C2=A0UTC >=C2=A0 >=C2=A0++++= =C2=A0src/solvers/sat/external_sat.cpp >=C2=A0 >=C2=A0+@@=C2=A0-119,8= =C2=A0+119,8=C2=A0@@=C2=A0external_satt::resultt=C2=A0external_satt::parse_= result(std >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0{ >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0try >=C2=A0 >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0{ >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0signed=C2=A0long=C2=A0long=C2=A0as_long=C2=A0=3D= =C2=A0std::stol(assignment_string); >=C2=A0 >=C2=A0+-=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0size_t=C2=A0index=C2=A0=3D= =C2=A0std::labs(as_long); >=C2=A0 >=C2=A0++=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0signed=C2=A0long=C2=A0long=C2=A0as_long= =C2=A0=3D=C2=A0std::stoll(assignment_string); >=C2=A0 >=C2=A0++=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0size_t=C2=A0index= =C2=A0=3D=C2=A0std::llabs(as_long); >=C2=A0 >=C2=A0+=C2=A0 >=C2=A0 = >=C2=A0+=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0if(index=C2=A0>=3D=C2=A0number_of_variables) >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0{ >= =C2=A0 >=C2=A0diff=C2=A0--git=C2=A0a/devel/cbmc/files/patch-src_util_opti= onal.h=C2=A0b/devel/cbmc/files/patch-src_util_optional.h >=C2=A0 >= =C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index=C2=A0000= 000000000..4507ce0ade2b >=C2=A0 >=C2=A0---=C2=A0/dev/null >=C2=A0 >= =C2=A0+++=C2=A0b/devel/cbmc/files/patch-src_util_optional.h >=C2=A0 >= =C2=A0@@=C2=A0-0,0=C2=A0+1,29=C2=A0@@ >=C2=A0 >=C2=A0+---=C2=A0src/util= /optional.h.orig=C2=A0=C2=A0=C2=A0=C2=A02023-10-30=C2=A012:11:18=C2=A0UTC= >=C2=A0 >=C2=A0++++=C2=A0src/util/optional.h >=C2=A0 >=C2=A0+@@= =C2=A0-11,20=C2=A0+11,20=C2=A0@@=C2=A0Author:=C2=A0Diffblue=C2=A0Ltd. >= =C2=A0 >=C2=A0+=C2=A0#define=C2=A0CPROVER_UTIL_OPTIONAL_H >=C2=A0 >= =C2=A0+=C2=A0 >=C2=A0 >=C2=A0+=C2=A0#if=C2=A0defined=C2=A0__clang__ >= =C2=A0 >=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0push= =C2=A0ignore=C2=A0"-Wall" >=C2=A0 >=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0cla= ng=C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-Wpedantic" >=C2=A0 >= =C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0push >=C2= =A0 >=C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0ignored= =C2=A0"-Wall" >=C2=A0 >=C2=A0++=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diag= nostic=C2=A0ignored=C2=A0"-Wpedantic" >=C2=A0 >=C2=A0+=C2=A0#elif=C2= =A0defined=C2=A0__GNUC__ >=C2=A0 >=C2=A0+-=C2=A0=C2=A0#pragma=C2=A0GCC= =C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-Wall" >=C2=A0 >=C2=A0+-= =C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0push=C2=A0ignore=C2=A0"-W= pedantic" >=C2=A0 >=C2=A0++=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic= =C2=A0push >=C2=A0 >=C2=A0++=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnosti= c=C2=A0ignored=C2=A0"-Wall" >=C2=A0 >=C2=A0++=C2=A0=C2=A0#pragma=C2= =A0GCC=C2=A0diagnostic=C2=A0ignored=C2=A0"-Wpedantic" >=C2=A0 >=C2= =A0+=C2=A0#elif=C2=A0defined=C2=A0_MSC_VER >=C2=A0 >=C2=A0+=C2=A0=C2= =A0=C2=A0#pragma=C2=A0warning(push) >=C2=A0 >=C2=A0+=C2=A0#endif >= =C2=A0 >=C2=A0+=C2=A0#include=C2=A0<nonstd/optional.hpp> >=C2=A0 >= =C2=A0+=C2=A0#if=C2=A0defined=C2=A0=C2=A0__clang__ >=C2=A0 >=C2=A0+= =C2=A0=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0pop >=C2=A0 >= =C2=A0+-=C2=A0=C2=A0#pragma=C2=A0clang=C2=A0diagnostic=C2=A0pop >=C2= =A0 >=C2=A0+=C2=A0#elif=C2=A0defined=C2=A0=C2=A0__GNUC__ >=C2=A0 >= =C2=A0+-=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0pop >=C2=A0 >= =C2=A0+=C2=A0=C2=A0=C2=A0#pragma=C2=A0GCC=C2=A0diagnostic=C2=A0pop >= =C2=A0 >=C2=A0+=C2=A0#elif=C2=A0defined=C2=A0_MSC_VER >=C2=A0 >=C2= =A0+=C2=A0=C2=A0=C2=A0#pragma=C2=A0warning(pop) >=C2=A0 >=C2=A0diff= =C2=A0--git=C2=A0a/devel/cbmc/pkg-descr=C2=A0b/devel/cbmc/pkg-descr >= =C2=A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0inde= x=C2=A0000000000000..2004194d7c43 >=C2=A0 >=C2=A0---=C2=A0/dev/null >= =C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/pkg-descr >=C2=A0 >=C2=A0@@=C2= =A0-0,0=C2=A0+1,7=C2=A0@@ >=C2=A0 >=C2=A0+CBMC=C2=A0is=C2=A0a=C2=A0Boun= ded=C2=A0Model=C2=A0Checker=C2=A0for=C2=A0C=C2=A0and=C2=A0C++=C2=A0programs= . >=C2=A0 >=C2=A0+It=C2=A0supports=C2=A0C89,=C2=A0C99,=C2=A0most=C2= =A0of=C2=A0C11=C2=A0and=C2=A0most=C2=A0compiler=C2=A0extensions=C2=A0provid= ed=C2=A0by=C2=A0gcc >=C2=A0 >=C2=A0+and=C2=A0Visual=C2=A0Studio.=C2= =A0It=C2=A0allows=C2=A0verifying=C2=A0array=C2=A0bounds=C2=A0(buffer=C2= =A0overflows),=C2=A0pointer >=C2=A0 >=C2=A0+safety,=C2=A0exceptions= =C2=A0and=C2=A0user-specified=C2=A0assertions.=C2=A0Furthermore,=C2=A0it= =C2=A0can=C2=A0check=C2=A0C >=C2=A0 >=C2=A0+and=C2=A0C++=C2=A0for=C2= =A0consistency=C2=A0with=C2=A0other=C2=A0languages,=C2=A0such=C2=A0as=C2= =A0Verilog. >=C2=A0 >=C2=A0+The=C2=A0verification=C2=A0is=C2=A0performe= d=C2=A0by=C2=A0unwinding=C2=A0the=C2=A0loops=C2=A0in=C2=A0the=C2=A0program= =C2=A0and=C2=A0passing >=C2=A0 >=C2=A0+the=C2=A0resulting=C2=A0equation= =C2=A0to=C2=A0a=C2=A0decision=C2=A0procedure. >=C2=A0 >=C2=A0diff=C2= =A0--git=C2=A0a/devel/cbmc/pkg-plist=C2=A0b/devel/cbmc/pkg-plist >=C2= =A0 >=C2=A0new=C2=A0file=C2=A0mode=C2=A0100644 >=C2=A0 >=C2=A0index= =C2=A0000000000000..2d23b585ef57 >=C2=A0 >=C2=A0---=C2=A0/dev/null >= =C2=A0 >=C2=A0+++=C2=A0b/devel/cbmc/pkg-plist >=C2=A0 >=C2=A0@@=C2= =A0-0,0=C2=A0+1,23=C2=A0@@ >=C2=A0 >=C2=A0+bin/cbmc >=C2=A0 >=C2= =A0+bin/crangler >=C2=A0 >=C2=A0+bin/goto-analyzer >=C2=A0 >=C2= =A0+bin/goto-cc >=C2=A0 >=C2=A0+bin/goto-diff >=C2=A0 >=C2=A0+bin/g= oto-instrument >=C2=A0 >=C2=A0+bin/goto-inspect >=C2=A0 >=C2=A0+bin= /goto-harness >=C2=A0 >=C2=A0+bin/goto-synthesizer >=C2=A0 >=C2= =A0+bin/symtab2gb >=C2=A0 >=C2=A0+bin/ls_parse.py=C2=A0[http://parse.py= ] >=C2=A0 >=C2=A0+bin/goto-gcc >=C2=A0 >=C2=A0+bin/goto-ld >= =C2=A0 >=C2=A0+share/man/man1/cbmc.1.gz >=C2=A0 >=C2=A0+share/man/man= 1/crangler.1.gz >=C2=A0 >=C2=A0+share/man/man1/goto-analyzer.1.gz >= =C2=A0 >=C2=A0+share/man/man1/goto-cc.1.gz >=C2=A0 >=C2=A0+share/man/= man1/goto-diff.1.gz >=C2=A0 >=C2=A0+share/man/man1/goto-harness.1.gz = >=C2=A0 >=C2=A0+share/man/man1/goto-inspect.1.gz >=C2=A0 >=C2=A0+shar= e/man/man1/goto-instrument.1.gz >=C2=A0 >=C2=A0+share/man/man1/goto-syn= thesizer.1.gz >=C2=A0 >=C2=A0+share/man/man1/symtab2gb.1.gz Hi, = Are these patches upstreamed or backported? Best regards, Dani= el (diizzy@) --_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_ Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable <div>On 2024-02-01T18:55:09.000+01:00, Olivier Cochard <olivier@FreeBSD.= org> wrote:<br></div><div class=3D"ik_mail_quote answerContentMessage"><= blockquote class=3D"ws-ng-quote"><pre style=3D"white-space: normal;"><div>T= he branch main has been updated by olivier:<br></div><div><br></div><div>UR= L: <a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai= lLink" href=3D"https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b720e52d51b= 22db0da2d7565418a0e428ef" target=3D"_blank">https://cgit.FreeBSD.org/ports/= commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef</a><br></div><div><br= ></div><div>commit 7f087b720e52d51b22db0da2d7565418a0e428ef<br></div><div>A= uthor: Olivier Cochard <<a class=3D"defaultMailLink" href=3D"mailto:= olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div>AuthorDate: = 2024-02-01 17:50:02 +0000<br></div><div>Commit: Olivier Cochard <<a = class=3D"defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier@FreeB= SD.org</a>><br></div><div>CommitDate: 2024-02-01 17:53:55 +0000<br></div= ><div><br></div><div> devel/cbmc: add new port<br></div><div> <br></d= iv><div> Bounded Model Checker for C and C++ programs<br></div><div> = <a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLi= nk" href=3D"https://github.com/diffblue/cbmc" target=3D"_blank">https://git= hub.com/diffblue/cbmc</a><br></div><div> <br></div><div> Sponsored by= : Netflix<br></div><div>---<br></div><div> devel/Makefile = | 1 +<br></div><div> devel/cbmc/Makefile = | 46 +++++++++++++++++<br></div><div> devel/cbmc/distinf= o | 5 ++<br></div><div> .../patch-minisat-2= .2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" clas= s=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"_blank">Solver.cc= </a> | 20 ++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_core_= SolverTypes.h | 59 ++++++++++++++++++++++<br></div><div> .../patch-minisat-= 2.2.1_minisat_mtl_IntTypes.h | 12 +++++<br></div><div> .../files/patch-= minisat-2.2.1_minisat_mtl_Vec.h | 16 ++++++<br></div><div> .../files/pat= ch-minisat-2.2.1_minisat_mtl_XAlloc.h | 19 +++++++<br></div><div> .../patch= -minisat-2.2.1_minisat_simp_<a data-ik=3D"ik-secure" rel=3D"noopener norefe= rrer" class=3D"defaultMailLink" href=3D"http://SimpSolver.cc" target=3D"_bl= ank">SimpSolver.cc</a> | 37 ++++++++++++++<br></div><div> .../patch-minisat= -2.2.1_minisat_utils_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" c= lass=3D"defaultMailLink" href=3D"http://Options.cc" target=3D"_blank">Optio= ns.cc</a> | 15 ++++++<br></div><div> .../patch-minisat-2.2.1_minisat_util= s_Options.h | 30 +++++++++++<br></div><div> .../patch-minisat-2.2.1_mini= sat_utils_ParseUtils.h | 33 ++++++++++++<br></div><div> .../patch-minisat-2= .2.1_minisat_utils_System.h | 11 ++++<br></div><div> devel/cbmc/files/p= atch-src_common | 11 ++++<br></div><div> .../files/patch-s= rc_solvers_sat_external__sat.cpp | 13 +++++<br></div><div> devel/cbmc/file= s/patch-src_util_optional.h | 29 +++++++++++<br></div><div> devel/c= bmc/pkg-descr | 7 +++<br></div><div> devel/c= bmc/pkg-plist | 23 +++++++++<br></div><div> 1= 8 files changed, 387 insertions(+)<br></div><div><br></div><div>diff --git = a/devel/Makefile b/devel/Makefile<br></div><div>index 4da71e0953a1..51481c8= a3aca 100644<br></div><div>--- a/devel/Makefile<br></div><div>+++ b/devel/M= akefile<br></div><div>@@ -351,6 +351,7 @@<br></div><div> SUBDIR +=3D ca= tch2<br></div><div> SUBDIR +=3D cbang<br></div><div> SUBDIR +=3D cb= fmt<br></div><div>+ SUBDIR +=3D cbmc<br></div><div> SUBDIR +=3D cbro= wser<br></div><div> SUBDIR +=3D cc65<br></div><div> SUBDIR +=3D cca= che<br></div><div>diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br= ></div><div>new file mode 100644<br></div><div>index 000000000000..c7f7b365= 0e63<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/Makefile<br= ></div><div>@@ -0,0 +1,46 @@<br></div><div>+PORTNAME=3D=09cbmc<br></div><di= v>+PORTVERSION=3D=095.95.1<br></div><div>+DISTVERSIONPREFIX=3D=09cbmc-<br><= /div><div>+CATEGORIES=3D=09devel<br></div><div>+MASTER_SITES=3D=09DEBIAN/po= ol/main/m/minisat2:minisat<br></div><div>+DISTFILES=3D=09minisat2_2.2.1.ori= g.tar.gz:minisat<br></div><div>+<br></div><div>+MAINTAINER=3D=09<a class=3D= "defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</= a><br></div><div>+COMMENT=3D=09Bounded Model Checker for C and C++ programs= <br></div><div>+WWW=3D=09=09<a data-ik=3D"ik-secure" rel=3D"noopener norefe= rrer" class=3D"defaultMailLink" href=3D"https://github.com/diffblue/cbmc" t= arget=3D"_blank">https://github.com/diffblue/cbmc</a><br></div><div>+<br></= div><div>+LICENSE=3D=09BSD4CLAUSE<br></div><div>+LICENSE_FILE=3D=09${WRKSRC= }/LICENSE<br></div><div>+<br></div><div>+BUILD_DEPENDS=3D=09${LOCALBASE}/bi= n/flex:textproc/flex<br></div><div>+RUN_DEPENDS=3D=09${LOCALBASE}/bin/cvc5:= math/cvc5 \<br></div><div>+=09=09${LOCALBASE}/bin/z3:math/z3<br></div><div>= +<br></div><div>+USES=3D=09=09gmake bison python shebangfix<br></div><div>+= <br></div><div>+USE_GITHUB=3D=09yes<br></div><div>+GH_ACCOUNT=3D=09diffblue= <br></div><div>+SHEBANG_FILES=3D=09${WRKSRC}/scripts/ls_<a data-ik=3D"ik-se= cure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://= parse.py" target=3D"_blank">parse.py</a><br></div><div>+WRKSRC_minisat=3D= =09${WRKDIR}/minisat2-2.2.1<br></div><div>+<br></div><div>+post-patch:<br><= /div><div>+=09@${REINPLACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO =3D = ${PORTNAME}-${PORTVERSION}|' \<br></div><div>+=09=09${WRKSRC}/src/util/Make= file<br></div><div>+post-extract:<br></div><div>+=09@${MV} ${WRKSRC_minisat= } ${WRKSRC}/minisat-2.2.1<br></div><div>+<br></div><div>+do-build:<br></div= ><div>+=09@${MKDIR} ${STAGEDIR}<br></div><div>+=09cd ${WRKSRC} && $= {GMAKE} -C src -j${MAKE_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-inst= all:<br></div><div>+. for x in cbmc crangler goto-analyzer goto-cc goto-di= ff goto-instrument \<br></div><div>+=09goto-inspect goto-harness goto-synth= esizer symtab2gb<br></div><div>+=09${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${= x} ${STAGEDIR}${PREFIX}/bin/<br></div><div>+=09${INSTALL_MAN} ${WRKSRC}/doc= /man/${x}.1 ${STAGEDIR}${PREFIX}/share/man/man1/<br></div><div>+. endfor<b= r></div><div>+=09${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></d= iv><div>+=09${LN} -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><di= v>+=09${INSTALL_SCRIPT} ${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel= =3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://parse.py"= target=3D"_blank">parse.py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<b= r></div><div>+.include <<a data-ik=3D"ik-secure" rel=3D"noopener norefer= rer" class=3D"defaultMailLink" href=3D"http://bsd.port.mk>" target=3D"_blan= k">bsd.port.mk></a>;<br></div><div>diff --git a/devel/cbmc/distinfo b/de= vel/cbmc/distinfo<br></div><div>new file mode 100644<br></div><div>index 00= 0000000000..f3e6d1161c6a<br></div><div>--- /dev/null<br></div><div>+++ b/de= vel/cbmc/distinfo<br></div><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP = =3D 1706723199<br></div><div>+SHA256 (minisat2_2.2.1.orig.tar.gz) =3D e54af= a3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40<br></div><div>+= SIZE (minisat2_2.2.1.orig.tar.gz) =3D 44229<br></div><div>+SHA256 (diffblue= -cbmc-cbmc-5.95.1_GH0.tar.gz) =3D fdc1e862752430f8d069eb2f9c33dcd05078cf955= bbc900e2cc840bcb01b3783<br></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.= tar.gz) =3D 9073428<br></div><div>diff --git a/devel/cbmc/files/patch-minis= at-2.2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" = class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"_blank">Solve= r.cc</a> b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"= ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"ht= tp://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><div>new file mode= 100644<br></div><div>index 000000000000..c15c2f12fb0a<br></div><div>--- /d= ev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_co= re_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai= lLink" href=3D"http://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><= div>@@ -0,0 +1,20 @@<br></div><div>+--- minisat-2.2.1/minisat/core/<a data-= ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href= =3D"http://Solver.cc.orig" target=3D"_blank">Solver.cc.orig</a>=092011-02-2= 1 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/<a data-ik=3D"= ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"ht= tp://Solver.cc" target=3D"_blank">Solver.cc</a><br></div><div>+@@ -210,7 +2= 10,7 @@ void Solver::cancelUntil(int level) {<br></div><div>+ for (= int c =3D trail.size()-1; c &gt;=3D trail_lim[level]; c--){<br></div><d= iv>+ Var x =3D var(trail[c]);<br></div><div>+ = assigns [x] =3D l_Undef;<br></div><div>+- if (phase_saving >= 1 || (phase_saving =3D=3D 1) && c > trail_lim.last())<br></div>= <div>++ if (phase_saving > 1 || ((phase_saving =3D=3D 1) &= ;& c > trail_lim.last()))<br></div><div>+ polarity[x= ] =3D sign(trail[c]);<br></div><div>+ insertVarOrder(x); }<br><= /div><div>+ qhead =3D trail_lim[level];<br></div><div>+@@ -666,7 +6= 66,7 @@ lbool Solver::search(int nof_conflicts)<br></div><div>+ <br></div><= div>+ }else{<br></div><div>+ // NO CONFLICT<br></div><d= iv>+- if (nof_conflicts &gt;=3D 0 && conflictC &= gt;=3D nof_conflicts || !withinBudget()){<br></div><div>++ if ((= nof_conflicts &gt;=3D 0 && conflictC &gt;=3D nof_conflicts)= || !withinBudget()){<br></div><div>+ // Reached bound on n= umber of conflicts:<br></div><div>+ progress_estimate =3D p= rogressEstimate();<br></div><div>+ cancelUntil(0);<br></div= ><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_Solver= Types.h b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h<b= r></div><div>new file mode 100644<br></div><div>index 000000000000..fa26c63= 72b36<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/files/patc= h-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<b= r></div><div>+--- minisat-2.2.1/minisat/core/SolverTypes.h.orig=092011-02-2= 1 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/core/SolverTypes.h<= br></div><div>+@@ -47,7 +47,7 @@ struct Lit {<br></div><div>+ int x= ;<br></div><div>+ <br></div><div>+ // Use this as a constructor:<br></d= iv><div>+- friend Lit mkLit(Var var, bool sign =3D false);<br></div><div= >++ //friend Lit mkLit(Var var, bool sign =3D false);<br></div><div>+ <b= r></div><div>+ bool operator =3D=3D (Lit p) const { return x =3D=3D p.x= ; }<br></div><div>+ bool operator !=3D (Lit p) const { return x !=3D p.= x; }<br></div><div>+@@ -55,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></= div><div>+ <br></div><div>+ <br></div><div>+-inline Lit mkLit (Var va= r, bool sign) { Lit p; p.x =3D var + var + (int)sign; return p; }<br></div>= <div>++inline Lit mkLit (Var var, bool sign =3D false) { Lit p; p.x = =3D var + var + (int)sign; return p; }<br></div><div>+ inline Lit operato= r ~(Lit p) { Lit q; q.x =3D p.x ^ 1; return q; }<br></div><div= >+ inline Lit operator ^(Lit p, bool b) { Lit q; q.x =3D p.x ^ (unsi= gned int)b; return q; }<br></div><div>+ inline bool sign (Lit p) = { return p.x & 1; }<br></div><div>+@@ -127,7 +127,10 @@ class = Clause {<br></div><div>+ unsigned has_extra : 1;<br></div><div>+ = unsigned reloced : 1;<br></div><div>+ unsigned size : = 27; } header;<br></div><div>++#include <util/prag= ma_push.def><br></div><div>++#include <util/pragma_wzero_length_array= .def><br></div><div>+ union { Lit lit; float act; uint32_t abs; CRef= rel; } data[0];<br></div><div>++#include <util/pragma_pop.def><br></= div><div>+ <br></div><div>+ friend class ClauseAllocator;<br></div><div= >+ <br></div><div>+@@ -142,11 +145,12 @@ class Clause {<br></div><div>+ = for (int i =3D 0; i < ps.size(); i++) <br></div><div>+ = data[i].lit =3D ps[i];<br></div><div>+ <br></div><div>+- if (header.= has_extra)<br></div><div>++ if (header.has_extra) {<br></div><div>+ = if (header.learnt)<br></div><div>+ data[header.= size].act =3D 0;<br></div><div>+ else<br></div><div>+ = calcAbstraction();<br></div><div>++ }<br></div><div>+ }<b= r></div><div>+ <br></div><div>+ // NOTE: This constructor cannot be use= d directly (doesn't allocate enough memory).<br></div><div>+@@ -157,11 +161= ,12 @@ class Clause {<br></div><div>+ for (int i =3D 0; i < from= .size(); i++)<br></div><div>+ data[i].lit =3D from[i];<br></div= ><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++ = if (header.has_extra) {<br></div><div>+ if (header.learnt)<= br></div><div>+ data[header.size].act =3D <a data-ik=3D"ik-= secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http:= //from.data[header.size]" target=3D"_blank">from.data[header.size]</a>.act;= <br></div><div>+ else <br></div><div>+ data[hea= der.size].abs =3D <a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" clas= s=3D"defaultMailLink" href=3D"http://from.data[header.size]" target=3D"_bla= nk">from.data[header.size]</a>.abs;<br></div><div>++ }<br></div><div= >+ }<br></div><div>+ <br></div><div>+ public:<br></div><div>diff --git = a/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/= files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><div>new file mod= e 100644<br></div><div>index 000000000000..d8c9ddedb701<br></div><div>--- /= dev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_m= tl_IntTypes.h<br></div><div>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2= .1/minisat/mtl/IntTypes.h.orig=092011-02-21 13:31:17 UTC<br></div><div>++++= minisat-2.2.1/minisat/mtl/IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF O= R IN CONNECTION WITH THE SOFTWARE OR THE USE OR OT<br></div><div>+ #else<br= ></div><div>+ <br></div><div>+ # include <stdint.h><br></div><div>+= +#ifndef _MSC_VER<br></div><div>+ # include <inttypes.h><br></div><= div>++#endif<br></div><div>+ <br></div><div>+ The branch main has been upda= ted by olivier:<br></div><div><br></div><div>URL: <a data-ik=3D"ik-secure" = rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"https://cgit.= FreeBSD.org/ports/commit/?id=3D7f087b720e52d51b22db0da2d7565418a0e428ef" ta= rget=3D"_blank">https://cgit.FreeBSD.org/ports/commit/?id=3D7f087b720e52d51= b22db0da2d7565418a0e428ef</a><br></div><div><br></div><div>commit 7f087b720= e52d51b22db0da2d7565418a0e428ef<br></div><div>Author: Olivier Cochard &= lt;<a class=3D"defaultMailLink" href=3D"mailto:olivier@FreeBSD.org">olivier= @FreeBSD.org</a>><br></div><div>AuthorDate: 2024-02-01 17:50:02 +0000<br= ></div><div>Commit: Olivier Cochard <<a class=3D"defaultMailLink" hr= ef=3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a>><br></div><div= >CommitDate: 2024-02-01 17:53:55 +0000<br></div><div><br></div><div> dev= el/cbmc: add new port<br></div><div> <br></div><div> Bounded Model Ch= ecker for C and C++ programs<br></div><div> <a data-ik=3D"ik-secure" rel= =3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"https://github.c= om/diffblue/cbmc" target=3D"_blank">https://github.com/diffblue/cbmc</a><br= ></div><div> <br></div><div> Sponsored by: Netflix<br></div><div>--= -<br></div><div> devel/Makefile | 1 +<= br></div><div> devel/cbmc/Makefile | 46 ++++= +++++++++++++<br></div><div> devel/cbmc/distinfo = | 5 ++<br></div><div> .../patch-minisat-2.2.1_minisat_core_<a data-ik= =3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href= =3D"http://Solver.cc" target=3D"_blank">Solver.cc</a> | 20 ++++++++<br>= </div><div> .../patch-minisat-2.2.1_minisat_core_SolverTypes.h | 59 +++++++= +++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_mtl_IntTypes= .h | 12 +++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_mtl_= Vec.h | 16 ++++++<br></div><div> .../files/patch-minisat-2.2.1_minisat_m= tl_XAlloc.h | 19 +++++++<br></div><div> .../patch-minisat-2.2.1_minisat_sim= p_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMail= Link" href=3D"http://SimpSolver.cc" target=3D"_blank">SimpSolver.cc</a> | 3= 7 ++++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_<a da= ta-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" h= ref=3D"http://Options.cc" target=3D"_blank">Options.cc</a> | 15 ++++++<br= ></div><div> .../patch-minisat-2.2.1_minisat_utils_Options.h | 30 ++++++= +++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_ParseUtils.h | 3= 3 ++++++++++++<br></div><div> .../patch-minisat-2.2.1_minisat_utils_System.= h | 11 ++++<br></div><div> devel/cbmc/files/patch-src_common = | 11 ++++<br></div><div> .../files/patch-src_solvers_sat_external__s= at.cpp | 13 +++++<br></div><div> devel/cbmc/files/patch-src_util_optional.= h | 29 +++++++++++<br></div><div> devel/cbmc/pkg-descr = | 7 +++<br></div><div> devel/cbmc/pkg-plist = | 23 +++++++++<br></div><div> 18 files changed, 387 inser= tions(+)<br></div><div><br></div><div>diff --git a/devel/Makefile b/devel/M= akefile<br></div><div>index 4da71e0953a1..51481c8a3aca 100644<br></div><div= >--- a/devel/Makefile<br></div><div>+++ b/devel/Makefile<br></div><div>@@ -= 351,6 +351,7 @@<br></div><div> SUBDIR +=3D catch2<br></div><div> SU= BDIR +=3D cbang<br></div><div> SUBDIR +=3D cbfmt<br></div><div>+ SUB= DIR +=3D cbmc<br></div><div> SUBDIR +=3D cbrowser<br></div><div> SU= BDIR +=3D cc65<br></div><div> SUBDIR +=3D ccache<br></div><div>diff --g= it a/devel/cbmc/Makefile b/devel/cbmc/Makefile<br></div><div>new file mode = 100644<br></div><div>index 000000000000..c7f7b3650e63<br></div><div>--- /de= v/null<br></div><div>+++ b/devel/cbmc/Makefile<br></div><div>@@ -0,0 +1,46 = @@<br></div><div>+PORTNAME=3D=09cbmc<br></div><div>+PORTVERSION=3D=095.95.1= <br></div><div>+DISTVERSIONPREFIX=3D=09cbmc-<br></div><div>+CATEGORIES=3D= =09devel<br></div><div>+MASTER_SITES=3D=09DEBIAN/pool/main/m/minisat2:minis= at<br></div><div>+DISTFILES=3D=09minisat2_2.2.1.orig.tar.gz:minisat<br></di= v><div>+<br></div><div>+MAINTAINER=3D=09<a class=3D"defaultMailLink" href= =3D"mailto:olivier@FreeBSD.org">olivier@FreeBSD.org</a><br></div><div>+COMM= ENT=3D=09Bounded Model Checker for C and C++ programs<br></div><div>+WWW=3D= =09=09<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"default= MailLink" href=3D"https://github.com/diffblue/cbmc" target=3D"_blank">https= ://github.com/diffblue/cbmc</a><br></div><div>+<br></div><div>+LICENSE=3D= =09BSD4CLAUSE<br></div><div>+LICENSE_FILE=3D=09${WRKSRC}/LICENSE<br></div><= div>+<br></div><div>+BUILD_DEPENDS=3D=09${LOCALBASE}/bin/flex:textproc/flex= <br></div><div>+RUN_DEPENDS=3D=09${LOCALBASE}/bin/cvc5:math/cvc5 \<br></div= ><div>+=09=09${LOCALBASE}/bin/z3:math/z3<br></div><div>+<br></div><div>+USE= S=3D=09=09gmake bison python shebangfix<br></div><div>+<br></div><div>+USE_= GITHUB=3D=09yes<br></div><div>+GH_ACCOUNT=3D=09diffblue<br></div><div>+SHEB= ANG_FILES=3D=09${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel=3D"noopene= r noreferrer" class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"= _blank">parse.py</a><br></div><div>+WRKSRC_minisat=3D=09${WRKDIR}/minisat2-= 2.2.1<br></div><div>+<br></div><div>+post-patch:<br></div><div>+=09@${REINP= LACE_CMD} -e 's|.*git describe --tags.*|GIT_INFO =3D ${PORTNAME}-${PORTVERS= ION}|' \<br></div><div>+=09=09${WRKSRC}/src/util/Makefile<br></div><div>+po= st-extract:<br></div><div>+=09@${MV} ${WRKSRC_minisat} ${WRKSRC}/minisat-2.= 2.1<br></div><div>+<br></div><div>+do-build:<br></div><div>+=09@${MKDIR} ${= STAGEDIR}<br></div><div>+=09cd ${WRKSRC} && ${GMAKE} -C src -j${MAK= E_JOBS_NUMBER}<br></div><div>+<br></div><div>+do-install:<br></div><div>+. = for x in cbmc crangler goto-analyzer goto-cc goto-diff goto-instrument \<b= r></div><div>+=09goto-inspect goto-harness goto-synthesizer symtab2gb<br></= div><div>+=09${INSTALL_PROGRAM} ${WRKSRC}/src/${x}/${x} ${STAGEDIR}${PREFIX= }/bin/<br></div><div>+=09${INSTALL_MAN} ${WRKSRC}/doc/man/${x}.1 ${STAGEDIR= }${PREFIX}/share/man/man1/<br></div><div>+. endfor<br></div><div>+=09${LN}= -sf goto-cc ${STAGEDIR}${PREFIX}/bin/goto-gcc<br></div><div>+=09${LN} -sf = goto-cc ${STAGEDIR}${PREFIX}/bin/goto-ld<br></div><div>+=09${INSTALL_SCRIPT= } ${WRKSRC}/scripts/ls_<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer"= class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"_blank">parse= .py</a> ${STAGEDIR}${PREFIX}/bin/<br></div><div>+<br></div><div>+.include &= lt;<a data-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMai= lLink" href=3D"http://bsd.port.mk>" target=3D"_blank">bsd.port.mk></a>;<= br></div><div>diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo<br></d= iv><div>new file mode 100644<br></div><div>index 000000000000..f3e6d1161c6a= <br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/distinfo<br></d= iv><div>@@ -0,0 +1,5 @@<br></div><div>+TIMESTAMP =3D 1706723199<br></div><d= iv>+SHA256 (minisat2_2.2.1.orig.tar.gz) =3D e54afa3c192c1753bc8075c0c7e126d= 5c495d9066e3f90a2588091149ac9ca40<br></div><div>+SIZE (minisat2_2.2.1.orig.= tar.gz) =3D 44229<br></div><div>+SHA256 (diffblue-cbmc-cbmc-5.95.1_GH0.tar.= gz) =3D fdc1e862752430f8d069eb2f9c33dcd05078cf955bbc900e2cc840bcb01b3783<br= ></div><div>+SIZE (diffblue-cbmc-cbmc-5.95.1_GH0.tar.gz) =3D 9073428<br></d= iv><div>diff --git a/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a d= ata-ik=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" = href=3D"http://Solver.cc" target=3D"_blank">Solver.cc</a> b/devel/cbmc/file= s/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"ik-secure" rel=3D"noopener= noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"= _blank">Solver.cc</a><br></div><div>new file mode 100644<br></div><div>inde= x 000000000000..c15c2f12fb0a<br></div><div>--- /dev/null<br></div><div>+++ = b/devel/cbmc/files/patch-minisat-2.2.1_minisat_core_<a data-ik=3D"ik-secure= " rel=3D"noopener noreferrer" class=3D"defaultMailLink" href=3D"http://Solv= er.cc" target=3D"_blank">Solver.cc</a><br></div><div>@@ -0,0 +1,20 @@<br></= div><div>+--- minisat-2.2.1/minisat/core/<a data-ik=3D"ik-secure" rel=3D"no= opener noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc.orig"= target=3D"_blank">Solver.cc.orig</a>=092011-02-21 13:31:17 UTC<br></div><d= iv>++++ minisat-2.2.1/minisat/core/<a data-ik=3D"ik-secure" rel=3D"noopener= noreferrer" class=3D"defaultMailLink" href=3D"http://Solver.cc" target=3D"= _blank">Solver.cc</a><br></div><div>+@@ -210,7 +210,7 @@ void Solver::cance= lUntil(int level) {<br></div><div>+ for (int c =3D trail.size()-1; = c &gt;=3D trail_lim[level]; c--){<br></div><div>+ Var = x =3D var(trail[c]);<br></div><div>+ assigns [x] =3D l_Undef;<= br></div><div>+- if (phase_saving > 1 || (phase_saving =3D=3D= 1) && c > trail_lim.last())<br></div><div>++ if (pha= se_saving > 1 || ((phase_saving =3D=3D 1) && c > trail_lim.la= st()))<br></div><div>+ polarity[x] =3D sign(trail[c]);<br><= /div><div>+ insertVarOrder(x); }<br></div><div>+ qhead = =3D trail_lim[level];<br></div><div>+@@ -666,7 +666,7 @@ lbool Solver::sear= ch(int nof_conflicts)<br></div><div>+ <br></div><div>+ }else{<br></= div><div>+ // NO CONFLICT<br></div><div>+- if (nof_c= onflicts &gt;=3D 0 && conflictC &gt;=3D nof_conflicts || !w= ithinBudget()){<br></div><div>++ if ((nof_conflicts &gt;=3D = 0 && conflictC &gt;=3D nof_conflicts) || !withinBudget()){<br><= /div><div>+ // Reached bound on number of conflicts:<br></d= iv><div>+ progress_estimate =3D progressEstimate();<br></di= v><div>+ cancelUntil(0);<br></div><div>diff --git a/devel/c= bmc/files/patch-minisat-2.2.1_minisat_core_SolverTypes.h b/devel/cbmc/files= /patch-minisat-2.2.1_minisat_core_SolverTypes.h<br></div><div>new file mode= 100644<br></div><div>index 000000000000..fa26c6372b36<br></div><div>--- /d= ev/null<br></div><div>+++ b/devel/cbmc/files/patch-minisat-2.2.1_minisat_co= re_SolverTypes.h<br></div><div>@@ -0,0 +1,59 @@<br></div><div>+--- minisat-= 2.2.1/minisat/core/SolverTypes.h.orig=092011-02-21 13:31:17 UTC<br></div><d= iv>++++ minisat-2.2.1/minisat/core/SolverTypes.h<br></div><div>+@@ -47,7 +4= 7,7 @@ struct Lit {<br></div><div>+ int x;<br></div><div>+ <br></di= v><div>+ // Use this as a constructor:<br></div><div>+- friend Lit m= kLit(Var var, bool sign =3D false);<br></div><div>++ //friend Lit mkLit(= Var var, bool sign =3D false);<br></div><div>+ <br></div><div>+ bool op= erator =3D=3D (Lit p) const { return x =3D=3D p.x; }<br></div><div>+ bo= ol operator !=3D (Lit p) const { return x !=3D p.x; }<br></div><div>+@@ -55= ,7 +55,7 @@ struct Lit {<br></div><div>+ };<br></div><div>+ <br></div><div>= + <br></div><div>+-inline Lit mkLit (Var var, bool sign) { Lit p; p.x= =3D var + var + (int)sign; return p; }<br></div><div>++inline Lit mkLit = (Var var, bool sign =3D false) { Lit p; p.x =3D var + var + (int)sign; = return p; }<br></div><div>+ inline Lit operator ~(Lit p) { L= it q; q.x =3D p.x ^ 1; return q; }<br></div><div>+ inline Lit operator ^(= Lit p, bool b) { Lit q; q.x =3D p.x ^ (unsigned int)b; return q; }<br>= </div><div>+ inline bool sign (Lit p) { return p.x &= 1; }<br></div><div>+@@ -127,7 +127,10 @@ class Clause {<br></div><div>+ = unsigned has_extra : 1;<br></div><div>+ unsigned reloced : = 1;<br></div><div>+ unsigned size : 27; } = header;<br></div><div>++#include <util/pragma_push.def><br></div><d= iv>++#include <util/pragma_wzero_length_array.def><br></div><div>+ = union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];<br></div><= div>++#include <util/pragma_pop.def><br></div><div>+ <br></div><div>+= friend class ClauseAllocator;<br></div><div>+ <br></div><div>+@@ -142,= 11 +145,12 @@ class Clause {<br></div><div>+ for (int i =3D 0; i &l= t; ps.size(); i++) <br></div><div>+ data[i].lit =3D ps[i];<br><= /div><div>+ <br></div><div>+- if (header.has_extra)<br></div><div>++= if (header.has_extra) {<br></div><div>+ if (header.lear= nt)<br></div><div>+ data[header.size].act =3D 0;<br></div><= div>+ else<br></div><div>+ calcAbstraction();<b= r></div><div>++ }<br></div><div>+ }<br></div><div>+ <br></div><d= iv>+ // NOTE: This constructor cannot be used directly (doesn't allocat= e enough memory).<br></div><div>+@@ -157,11 +161,12 @@ class Clause {<br></= div><div>+ for (int i =3D 0; i < from.size(); i++)<br></div><div= >+ data[i].lit =3D from[i];<br></div><div>+ <br></div><div>+- = if (header.has_extra)<br></div><div>++ if (header.has_extra) {= <br></div><div>+ if (header.learnt)<br></div><div>+ = data[header.size].act =3D <a data-ik=3D"ik-secure" rel=3D"noopener nor= eferrer" class=3D"defaultMailLink" href=3D"http://from.data[header.size]" t= arget=3D"_blank">from.data[header.size]</a>.act;<br></div><div>+ = else <br></div><div>+ data[header.size].abs =3D <a data-i= k=3D"ik-secure" rel=3D"noopener noreferrer" class=3D"defaultMailLink" href= =3D"http://from.data[header.size]" target=3D"_blank">from.data[header.size]= </a>.abs;<br></div><div>++ }<br></div><div>+ }<br></div><div>+ <= br></div><div>+ public:<br></div><div>diff --git a/devel/cbmc/files/patch-m= inisat-2.2.1_minisat_mtl_IntTypes.h b/devel/cbmc/files/patch-minisat-2.2.1_= minisat_mtl_IntTypes.h<br></div><div>new file mode 100644<br></div><div>ind= ex 000000000000..d8c9ddedb701<br></div><div>--- /dev/null<br></div><div>+++= b/devel/cbmc/files/patch-minisat-2.2.1_minisat_mtl_IntTypes.h<br></div><di= v>@@ -0,0 +1,12 @@<br></div><div>+--- minisat-2.2.1/minisat/mtl/IntTypes.h.= orig=092011-02-21 13:31:17 UTC<br></div><div>++++ minisat-2.2.1/minisat/mtl= /IntTypes.h<br></div><div>+@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE S= OFTWARE OR THE USE OR OT<br></div><div>+ #else<br></div><div>+ <br></div><d= iv>+ # include <stdint.h><br></div><div>++#ifndef _MSC_VER<br></div= ><div>+ # include <inttypes.h><br></div><div>++#endif<br></div><div= >+ <br></div><div>+ #endiffile mode 100644<br></div><div>index 000000000000= ..f0dd61cd9963<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/f= iles/patch-src_solvers_sat_external__sat.cpp<br></div><div>@@ -0,0 +1,13 @@= <br></div><div>+--- src/solvers/sat/external_sat.cpp.orig=092023-10-30 12:1= 1:18 UTC<br></div><div>++++ src/solvers/sat/external_sat.cpp<br></div><div>= +@@ -119,8 +119,8 @@ external_satt::resultt external_satt::parse_result(std= <br></div><div>+ {<br></div><div>+ try<br></div><div>+ = {<br></div><div>+- signed long long as_long =3D std::stol(assign= ment_string);<br></div><div>+- size_t index =3D std::labs(as_long)= ;<br></div><div>++ signed long long as_long =3D std::stoll(assignm= ent_string);<br></div><div>++ size_t index =3D std::llabs(as_long)= ;<br></div><div>+ <br></div><div>+ if(index &gt;=3D number_of= _variables)<br></div><div>+ {<br></div><div>diff --git a/devel/cb= mc/files/patch-src_util_optional.h b/devel/cbmc/files/patch-src_util_option= al.h<br></div><div>new file mode 100644<br></div><div>index 000000000000..4= 507ce0ade2b<br></div><div>--- /dev/null<br></div><div>+++ b/devel/cbmc/file= s/patch-src_util_optional.h<br></div><div>@@ -0,0 +1,29 @@<br></div><div>+-= -- src/util/optional.h.orig=092023-10-30 12:11:18 UTC<br></div><div>++++ sr= c/util/optional.h<br></div><div>+@@ -11,20 +11,20 @@ Author: Diffblue Ltd.<= br></div><div>+ #define CPROVER_UTIL_OPTIONAL_H<br></div><div>+ <br></div><= div>+ #if defined __clang__<br></div><div>+- #pragma clang diagnostic push= ignore "-Wall"<br></div><div>+- #pragma clang diagnostic push ignore "-Wp= edantic"<br></div><div>++ #pragma clang diagnostic push<br></div><div>++ = #pragma clang diagnostic ignored "-Wall"<br></div><div>++ #pragma clang di= agnostic ignored "-Wpedantic"<br></div><div>+ #elif defined __GNUC__<br></d= iv><div>+- #pragma GCC diagnostic push ignore "-Wall"<br></div><div>+- #p= ragma GCC diagnostic push ignore "-Wpedantic"<br></div><div>++ #pragma GCC= diagnostic push<br></div><div>++ #pragma GCC diagnostic ignored "-Wall"<b= r></div><div>++ #pragma GCC diagnostic ignored "-Wpedantic"<br></div><div>= + #elif defined _MSC_VER<br></div><div>+ #pragma warning(push)<br></div><= div>+ #endif<br></div><div>+ #include <nonstd/optional.hpp><br></div>= <div>+ #if defined __clang__<br></div><div>+ #pragma clang diagnostic po= p<br></div><div>+- #pragma clang diagnostic pop<br></div><div>+ #elif defi= ned __GNUC__<br></div><div>+- #pragma GCC diagnostic pop<br></div><div>+ = #pragma GCC diagnostic pop<br></div><div>+ #elif defined _MSC_VER<br></di= v><div>+ #pragma warning(pop)<br></div><div>diff --git a/devel/cbmc/pkg-d= escr b/devel/cbmc/pkg-descr<br></div><div>new file mode 100644<br></div><di= v>index 000000000000..2004194d7c43<br></div><div>--- /dev/null<br></div><di= v>+++ b/devel/cbmc/pkg-descr<br></div><div>@@ -0,0 +1,7 @@<br></div><div>+C= BMC is a Bounded Model Checker for C and C++ programs.<br></div><div>+It su= pports C89, C99, most of C11 and most compiler extensions provided by gcc<b= r></div><div>+and Visual Studio. It allows verifying array bounds (buffer o= verflows), pointer<br></div><div>+safety, exceptions and user-specified ass= ertions. Furthermore, it can check C<br></div><div>+and C++ for consistency= with other languages, such as Verilog.<br></div><div>+The verification is = performed by unwinding the loops in the program and passing<br></div><div>+= the resulting equation to a decision procedure.<br></div><div>diff --git a/= devel/cbmc/pkg-plist b/devel/cbmc/pkg-plist<br></div><div>new file mode 100= 644<br></div><div>index 000000000000..2d23b585ef57<br></div><div>--- /dev/n= ull<br></div><div>+++ b/devel/cbmc/pkg-plist<br></div><div>@@ -0,0 +1,23 @@= <br></div><div>+bin/cbmc<br></div><div>+bin/crangler<br></div><div>+bin/got= o-analyzer<br></div><div>+bin/goto-cc<br></div><div>+bin/goto-diff<br></div= ><div>+bin/goto-instrument<br></div><div>+bin/goto-inspect<br></div><div>+b= in/goto-harness<br></div><div>+bin/goto-synthesizer<br></div><div>+bin/symt= ab2gb<br></div><div>+bin/ls_<a data-ik=3D"ik-secure" rel=3D"noopener norefe= rrer" class=3D"defaultMailLink" href=3D"http://parse.py" target=3D"_blank">= parse.py</a><br></div><div>+bin/goto-gcc<br></div><div>+bin/goto-ld<br></di= v><div>+share/man/man1/cbmc.1.gz<br></div><div>+share/man/man1/crangler.1.g= z<br></div><div>+share/man/man1/goto-analyzer.1.gz<br></div><div>+share/man= /man1/goto-cc.1.gz<br></div><div>+share/man/man1/goto-diff.1.gz<br></div><d= iv>+share/man/man1/goto-harness.1.gz<br></div><div>+share/man/man1/goto-ins= pect.1.gz<br></div><div>+share/man/man1/goto-instrument.1.gz<br></div><div>= +share/man/man1/goto-synthesizer.1.gz<br></div><div>+share/man/man1/symtab2= gb.1.gz<br></div></pre></blockquote></div><div>Hi,<br></div><div><br></div>= <div>Are these patches upstreamed or backported?<br></div><div><br></div><d= iv>Best regards,<br></div><div>Daniel (diizzy@)<br></div><div ><div><br></d= iv></div> --_=_swift_1706832300_c2dcb94f2c2cc263794507f6574d26b4_=_--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?379c7ddb410058469dcda4f67b45caa9>