Re: [NEW] cbmc - Bounded Model Checker for C and C++
cbmc has been imported. Thanks, -- jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF DDCC 0DFA 74AE 1524 E7EE
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Stuart Hendersonwrites: > On 2016/10/20 22:11, Jeremie Courreges-Anglas wrote: >> Jeremie Courreges-Anglas writes: >> >> > Simon Mages writes: >> > >> >> Anything else i have to do? >> >> >> >> Or only wait until somebody picks it up and commits it? >> > >> > New ports must be reviewed by at least a second developer. >> > >> > As far as I'm concerned, the port looks good as is. ok jca@ is if >> > someone wants to import it. >> > >> > Tarball attached for convenience. >> >> Updated tarball, fcambus@ spotted a missing build dep on devel/bison. > > | CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, > C99, > | most of C11 and most compiler extensions provided by gcc and Visual Studio. > It > | also supports SystemC using Scoot. We have recently added experimental > support > | for Java Bytecode. > > "we" sounds a bit funny here. Maybe "using Scoot, and has experimental..." ? Yup. > | CBMC verifies array bounds (buffer overflows), pointer safety, > ex\cep\tions > | and user-specified as\ser\tions. Furthermore, it can check C and C++ for > | consistency with other languages, such as Verilog. The verification is > | performed by unwinding the loops in the program and passing the > re\sul\ting > | equation to a decision procedure. > > There are some odd unicode characters in that paragraph which don't add > anything to it and I think should be removed. Also whitespace at eol. Heh, nice catch. > | While CBMC is aimed for embedded software, it also supports dynamic memory > | allocation using malloc and new. > | > | CBMC comes with a built-in solver for bit-vector formulas that is based on > | MiniSat. As an alternative, CBMC has featured support for external SMT > solvers > | since version 3.3. The solvers we recommend are (in no particular order) > | Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be > | installed separately and have different licensing conditions. > > "we" again, and version history of the project isn't really interesting > for DESCR here. Maybe trim to "based on MiniSat, and also supports external > SMT solvers"? -> CBMC comes with a built-in solver for bit-vector formulas that is based on MiniSat. As an alternative, CBMC has featured support for external SMT solvers. Recommended solvers are (in no particular order) Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be installed separately and have different licensing conditions. > | share/doc/cbmc/man/ > | share/doc/cbmc/man/cbmc.1 > | @man man/man1/cbmc.1 > > No need to include the manual twice. Yeah, I ignored those bits but hey, let's remove them. > Other than those minor things it looks good to import to me. Is this an ok? :) Updated tarball below, thanks. cbmc.5.tar.gz Description: Binary data -- jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF DDCC 0DFA 74AE 1524 E7EE
Re: [NEW] cbmc - Bounded Model Checker for C and C++
On 2016/10/20 22:11, Jeremie Courreges-Anglas wrote: > Jeremie Courreges-Anglaswrites: > > > Simon Mages writes: > > > >> Anything else i have to do? > >> > >> Or only wait until somebody picks it up and commits it? > > > > New ports must be reviewed by at least a second developer. > > > > As far as I'm concerned, the port looks good as is. ok jca@ is if > > someone wants to import it. > > > > Tarball attached for convenience. > > Updated tarball, fcambus@ spotted a missing build dep on devel/bison. | CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, | most of C11 and most compiler extensions provided by gcc and Visual Studio. It | also supports SystemC using Scoot. We have recently added experimental support | for Java Bytecode. "we" sounds a bit funny here. Maybe "using Scoot, and has experimental..." ? | CBMC verifies array bounds (buffer overflows), pointer safety, ex\cep\tions | and user-specified as\ser\tions. Furthermore, it can check C and C++ for | consistency with other languages, such as Verilog. The verification is | performed by unwinding the loops in the program and passing the re\sul\ting | equation to a decision procedure. There are some odd unicode characters in that paragraph which don't add anything to it and I think should be removed. Also whitespace at eol. | While CBMC is aimed for embedded software, it also supports dynamic memory | allocation using malloc and new. | | CBMC comes with a built-in solver for bit-vector formulas that is based on | MiniSat. As an alternative, CBMC has featured support for external SMT solvers | since version 3.3. The solvers we recommend are (in no particular order) | Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be | installed separately and have different licensing conditions. "we" again, and version history of the project isn't really interesting for DESCR here. Maybe trim to "based on MiniSat, and also supports external SMT solvers"? | share/doc/cbmc/man/ | share/doc/cbmc/man/cbmc.1 | @man man/man1/cbmc.1 No need to include the manual twice. Other than those minor things it looks good to import to me.
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Jeremie Courreges-Anglaswrites: > Simon Mages writes: > >> Anything else i have to do? >> >> Or only wait until somebody picks it up and commits it? > > New ports must be reviewed by at least a second developer. > > As far as I'm concerned, the port looks good as is. ok jca@ is if > someone wants to import it. > > Tarball attached for convenience. Updated tarball, fcambus@ spotted a missing build dep on devel/bison. cbmc.4.tar.gz Description: Binary data -- jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF DDCC 0DFA 74AE 1524 E7EE
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Simon Mageswrites: > Anything else i have to do? > > Or only wait until somebody picks it up and commits it? New ports must be reviewed by at least a second developer. As far as I'm concerned, the port looks good as is. ok jca@ is if someone wants to import it. Tarball attached for convenience. cbmc.3.tar.gz Description: Binary data -- jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF DDCC 0DFA 74AE 1524 E7EE
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Anything else i have to do? Or only wait until somebody picks it up and commits it? BR Simon 2016-10-17 9:41 GMT+02:00, Simon Mages: > Hi, > > 2016-10-16 19:17 GMT+02:00, Jeremie Courreges-Anglas : >> Simon Mages writes: >> >>> Hi, >>> >>> 2016-10-16 12:14 GMT+02:00, Stuart Henderson : On 2016/10/16 12:09, Simon Mages wrote: > Ok, thanks for the feedback. > > But i really don't get the llvm dependency. > I used the llvm in base on current to build > this port. Why shouldi suddenly use this > one? LLVM is not enabled in base. Anyway, setting MODULES=lang/clang will add the dep automatically. >>> Finally i got it, i was working with wrong assumptions, sorry for that. >>> >>> Attached the new port. >>> >>> # tar zcvf /tmp/cbmc.tar.gz devel/cbmc >>> devel/cbmc >>> devel/cbmc/Makefile >>> devel/cbmc/patches >>> devel/cbmc/patches/patch-src_big-int_bigint-test_cc >>> devel/cbmc/patches/patch-src_common~ >>> devel/cbmc/patches/patch-src_big-int_bigint_cc >>> devel/cbmc/patches/patch-src_common >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_Solver_cc >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_SolverTypes_h >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_IntTypes_h >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_Vec_h >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_simp_SimpSolver_cc >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_Options_h >>> devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_ParseUtils_h >>> devel/cbmc/distinfo >>> devel/cbmc/pkg >>> devel/cbmc/pkg/PLIST >>> devel/cbmc/pkg/DESCR >>> >>> Lets see if now everything is alright :) >> >> Looks nicer, here are a few improvements: >> - some spacing nits >> - use MASTER_SITE_DEBIAN >> - as Stuart pointed out, no need for p5-libwww any more >> - respect CFLAGS, CXXFLAGS and LDFLAGS, using MAKE_FLAGS; this helps >> a lot for debug builds >> - instead of putting the minisat2 patches in the port patches/ >> directory, we could also just use upstream's patch in post-extract. >> From my POV those patches aren't my concern, so I don't care about >> them being tracked by CVS. >> - patch the include file that provides the "compatibility" goo for >> alloca, instead of patching consumers. >> >> Updated tarball below. > From my point of view we can just take the version you send. > Its very interesting to see what the ports framework can do, thanks a lot > @all > people who replied so far :) > >> Note: you create a dedicated section where to set CP_CXXFLAGS, LINKLIB, >> etc on OpenBSD, an alternative could be to just amend the FreeBSD >> section: >> >> -else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),) >> +else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),) >> >> I doubt that it matters much, upstream may have an opinion already. > The problem here is that the version of 'ar' we are using does not > support the -T flag. > Thats why i created the OpenBSD section in the first place. > > BR > Simon >
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Hi, 2016-10-16 19:17 GMT+02:00, Jeremie Courreges-Anglas: > Simon Mages writes: > >> Hi, >> >> 2016-10-16 12:14 GMT+02:00, Stuart Henderson : >>> On 2016/10/16 12:09, Simon Mages wrote: Ok, thanks for the feedback. But i really don't get the llvm dependency. I used the llvm in base on current to build this port. Why shouldi suddenly use this one? >>> >>> LLVM is not enabled in base. Anyway, setting MODULES=lang/clang will >>> add the dep automatically. >> Finally i got it, i was working with wrong assumptions, sorry for that. >> >> Attached the new port. >> >> # tar zcvf /tmp/cbmc.tar.gz devel/cbmc >> devel/cbmc >> devel/cbmc/Makefile >> devel/cbmc/patches >> devel/cbmc/patches/patch-src_big-int_bigint-test_cc >> devel/cbmc/patches/patch-src_common~ >> devel/cbmc/patches/patch-src_big-int_bigint_cc >> devel/cbmc/patches/patch-src_common >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_Solver_cc >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_SolverTypes_h >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_IntTypes_h >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_Vec_h >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_simp_SimpSolver_cc >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_Options_h >> devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_ParseUtils_h >> devel/cbmc/distinfo >> devel/cbmc/pkg >> devel/cbmc/pkg/PLIST >> devel/cbmc/pkg/DESCR >> >> Lets see if now everything is alright :) > > Looks nicer, here are a few improvements: > - some spacing nits > - use MASTER_SITE_DEBIAN > - as Stuart pointed out, no need for p5-libwww any more > - respect CFLAGS, CXXFLAGS and LDFLAGS, using MAKE_FLAGS; this helps > a lot for debug builds > - instead of putting the minisat2 patches in the port patches/ > directory, we could also just use upstream's patch in post-extract. > From my POV those patches aren't my concern, so I don't care about > them being tracked by CVS. > - patch the include file that provides the "compatibility" goo for > alloca, instead of patching consumers. > > Updated tarball below. >From my point of view we can just take the version you send. Its very interesting to see what the ports framework can do, thanks a lot @all people who replied so far :) > Note: you create a dedicated section where to set CP_CXXFLAGS, LINKLIB, > etc on OpenBSD, an alternative could be to just amend the FreeBSD > section: > > -else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),) > +else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),) > > I doubt that it matters much, upstream may have an opinion already. The problem here is that the version of 'ar' we are using does not support the -T flag. Thats why i created the OpenBSD section in the first place. BR Simon
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Simon Mageswrites: > Hi, > > 2016-10-16 12:14 GMT+02:00, Stuart Henderson : >> On 2016/10/16 12:09, Simon Mages wrote: >>> Ok, thanks for the feedback. >>> >>> But i really don't get the llvm dependency. >>> I used the llvm in base on current to build >>> this port. Why shouldi suddenly use this >>> one? >> >> LLVM is not enabled in base. Anyway, setting MODULES=lang/clang will >> add the dep automatically. > Finally i got it, i was working with wrong assumptions, sorry for that. > > Attached the new port. > > # tar zcvf /tmp/cbmc.tar.gz devel/cbmc > devel/cbmc > devel/cbmc/Makefile > devel/cbmc/patches > devel/cbmc/patches/patch-src_big-int_bigint-test_cc > devel/cbmc/patches/patch-src_common~ > devel/cbmc/patches/patch-src_big-int_bigint_cc > devel/cbmc/patches/patch-src_common > devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_Solver_cc > devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_SolverTypes_h > devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_IntTypes_h > devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_Vec_h > devel/cbmc/patches/patch-minisat-2_2_1_minisat_simp_SimpSolver_cc > devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_Options_h > devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_ParseUtils_h > devel/cbmc/distinfo > devel/cbmc/pkg > devel/cbmc/pkg/PLIST > devel/cbmc/pkg/DESCR > > Lets see if now everything is alright :) Looks nicer, here are a few improvements: - some spacing nits - use MASTER_SITE_DEBIAN - as Stuart pointed out, no need for p5-libwww any more - respect CFLAGS, CXXFLAGS and LDFLAGS, using MAKE_FLAGS; this helps a lot for debug builds - instead of putting the minisat2 patches in the port patches/ directory, we could also just use upstream's patch in post-extract. From my POV those patches aren't my concern, so I don't care about them being tracked by CVS. - patch the include file that provides the "compatibility" goo for alloca, instead of patching consumers. Updated tarball below. Note: you create a dedicated section where to set CP_CXXFLAGS, LINKLIB, etc on OpenBSD, an alternative could be to just amend the FreeBSD section: -else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),) +else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),) I doubt that it matters much, upstream may have an opinion already. cbmc.3.tar.gz Description: Binary data -- jca | PGP : 0x1524E7EE / 5135 92C1 AD36 5293 2BDF DDCC 0DFA 74AE 1524 E7EE
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Hi, 2016-10-16 12:14 GMT+02:00, Stuart Henderson: > On 2016/10/16 12:09, Simon Mages wrote: >> Ok, thanks for the feedback. >> >> But i really don't get the llvm dependency. >> I used the llvm in base on current to build >> this port. Why shouldi suddenly use this >> one? > > LLVM is not enabled in base. Anyway, setting MODULES=lang/clang will > add the dep automatically. Finally i got it, i was working with wrong assumptions, sorry for that. Attached the new port. # tar zcvf /tmp/cbmc.tar.gz devel/cbmc devel/cbmc devel/cbmc/Makefile devel/cbmc/patches devel/cbmc/patches/patch-src_big-int_bigint-test_cc devel/cbmc/patches/patch-src_common~ devel/cbmc/patches/patch-src_big-int_bigint_cc devel/cbmc/patches/patch-src_common devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_Solver_cc devel/cbmc/patches/patch-minisat-2_2_1_minisat_core_SolverTypes_h devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_IntTypes_h devel/cbmc/patches/patch-minisat-2_2_1_minisat_mtl_Vec_h devel/cbmc/patches/patch-minisat-2_2_1_minisat_simp_SimpSolver_cc devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_Options_h devel/cbmc/patches/patch-minisat-2_2_1_minisat_utils_ParseUtils_h devel/cbmc/distinfo devel/cbmc/pkg devel/cbmc/pkg/PLIST devel/cbmc/pkg/DESCR Lets see if now everything is alright :) BR Simon cbmc.tar.gz Description: GNU Zip compressed data
Re: [NEW] cbmc - Bounded Model Checker for C and C++
On 2016/10/16 12:09, Simon Mages wrote: > Ok, thanks for the feedback. > > But i really don't get the llvm dependency. > I used the llvm in base on current to build > this port. Why shouldi suddenly use this > one? LLVM is not enabled in base. Anyway, setting MODULES=lang/clang will add the dep automatically.
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Ok, thanks for the feedback. But i really don't get the llvm dependency. I used the llvm in base on current to build this port. Why shouldi suddenly use this one? BR Simon Am Sonntag, 16. Oktober 2016 schrieb Stuart Henderson : > On 2016/10/16 07:58, Simon Mages wrote: > > > first, nice port. I would like to test my own code with it. But you > > > missed the clang dependency. > > > > Well, i thought that a new port will not be taged for a past release. If > > this is wrong i can > > add the dependency. > > I don't understand what you're saying here. > > > > bsd,port.mk(5): > > > REVISION > > > Revision number of the current package. Defaults to empty > (very > > > first package),... > > > > > > Why do you not fixed the missing RCS tags of the portscheck you made? > > > > What should i fix there? I thought cvs will add > > them on commit. > > You should have the "$OpenBSD$" part (with the preceding # in Makefile), > cvs will fill in the committer account, revision, timestamp, etc. Some > of the missing tags were on patches/*; these should be generated with > "make update-patches" which adds the tags for you. > > Other comments - > > .. > > # this port will apply patches to minisat > pre-build: > cd ${WRKSRC} && ${MAKE_PROGRAM} minisat2-download > > You can't do that, package build machines don't have network access. > (Also note that it is unsafe! There is no checking of hash or signature > in their Makefile). It will need to be downloaded by setting DISTFILES > instead, like this > > DISTFILES= ${DISTNAME}${EXTRACT_SUFX} \ > minisat2_2.2.1.orig.tar.gz:0 > > MASTER_SITES0= http://ftp.debian.org/debian/pool/main/m/minisat2/ > > and 'make makesum' to regenerate distinfo. It will then be untarred > during the extract stage but might not be in the place you need; replace > your pre-build line with any necessary mv and patch commands. Better to > put those in post-patch rather than pre-build. I think this may also > allow you to remove the lwp dependency. > > .. > > skip this: > > + ifeq ($(origin CC),default) > +CC = clang > + endif > + ifeq ($(origin CXX),default) > +CXX= clang++ > + endif > > and use this in Makefile instead: > > MODULES=lang/clang > MODCLANG_LANGS= c++ > MODCLANG_ARCHS= * > > .. > > Put the GH_* bits up where you have DISTNAME (like in Makefile.template). > > .. > > # 4-clause BSD license > > we don't differentiate between versions of the BSD license in these > markers, better to just put "BSD" - if users care about specific > details they should be checking for themselves. (We do have more > specifics for GPL because the different versions are incompatible > with different other licenses). > >
Re: [NEW] cbmc - Bounded Model Checker for C and C++
On 2016/10/16 07:58, Simon Mages wrote: > > first, nice port. I would like to test my own code with it. But you > > missed the clang dependency. > > Well, i thought that a new port will not be taged for a past release. If > this is wrong i can > add the dependency. I don't understand what you're saying here. > > bsd,port.mk(5): > > REVISION > > Revision number of the current package. Defaults to empty (very > > first package),... > > > > Why do you not fixed the missing RCS tags of the portscheck you made? > > What should i fix there? I thought cvs will add > them on commit. You should have the "$OpenBSD$" part (with the preceding # in Makefile), cvs will fill in the committer account, revision, timestamp, etc. Some of the missing tags were on patches/*; these should be generated with "make update-patches" which adds the tags for you. Other comments - .. # this port will apply patches to minisat pre-build: cd ${WRKSRC} && ${MAKE_PROGRAM} minisat2-download You can't do that, package build machines don't have network access. (Also note that it is unsafe! There is no checking of hash or signature in their Makefile). It will need to be downloaded by setting DISTFILES instead, like this DISTFILES= ${DISTNAME}${EXTRACT_SUFX} \ minisat2_2.2.1.orig.tar.gz:0 MASTER_SITES0= http://ftp.debian.org/debian/pool/main/m/minisat2/ and 'make makesum' to regenerate distinfo. It will then be untarred during the extract stage but might not be in the place you need; replace your pre-build line with any necessary mv and patch commands. Better to put those in post-patch rather than pre-build. I think this may also allow you to remove the lwp dependency. .. skip this: + ifeq ($(origin CC),default) +CC = clang + endif + ifeq ($(origin CXX),default) +CXX= clang++ + endif and use this in Makefile instead: MODULES=lang/clang MODCLANG_LANGS= c++ MODCLANG_ARCHS= * .. Put the GH_* bits up where you have DISTNAME (like in Makefile.template). .. # 4-clause BSD license we don't differentiate between versions of the BSD license in these markers, better to just put "BSD" - if users care about specific details they should be checking for themselves. (We do have more specifics for GPL because the different versions are incompatible with different other licenses).
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Hi, Am Samstag, 15. Oktober 2016 schrieb Jan Klemkow : > Hi Simon, > > first, nice port. I would like to test my own code with it. But you > missed the clang dependency. Well, i thought that a new port will not be taged for a past release. If this is wrong i can add the dependency. > Your port is new and don't need a > REVISION. Ok, will fix that. > bsd,port.mk(5): > REVISION > Revision number of the current package. Defaults to empty (very > first package),... > > Why do you not fixed the missing RCS tags of the portscheck you made? What should i fix there? I thought cvs will add them on commit. > Little nitpick: as far as I know its more common to use spaces between > variables and their equals signs like in > /usr/ports/infrastructure/templates/Makefile.template. Yea, i can fix that. > bye, > Jan > > log: > > ## Entering big-int > gmake -C big-int > gmake[1]: Entering directory > '/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' > clang++ -c -MMD -MP -std=c++11 -Wall -O2 -o bigint-func.o > bigint-func.cc > gmake[1]: clang++: Command not found > gmake[1]: *** [../common:183: bigint-func.o] Error 127 > gmake[1]: Leaving directory > '/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' > gmake: *** [Makefile:50: big-int.dir] Error 2 > *** Error 2 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2671 > '/usr/ports/pobj/cbmc-5.5/.build_done') > *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1884 > '/usr/ports/packages/amd64/all/cbmc-5.5p0.tgz') > *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2409 > '_internal-package') > *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2389 > 'package') > *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1901 > '/var/db/pkg/cbmc-5.5p0/+CONTENTS') > *** Error 1 in /usr/ports/devel/cbmc > (/usr/ports/infrastructure/mk/bsd.port.mk:2389 'install') > > > On Fri, Oct 14, 2016 at 08:15:21PM +0200, Simon Mages wrote: > > Hi, > > > > this is my first port, i hope everything is fine. > > > > A college of mine was using this tool to analyse some C code. I think > this > > tool is pretty interesting and can be put to good use for all sorts of > programs > > or parts of it. > > > > COMMENT= Bounded Model Checker for C and C++ programs > > > > # cat pkg/DESCR > > CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, > C99, > > most of C11 and most compiler extensions provided by gcc and Visual > Studio. It > > also supports SystemC using Scoot. We have recently added experimental > support > > for Java Bytecode. > > > > CBMC verifies array bounds (buffer overflows), pointer safety, > ex??cep??tions > > and user-specified as??ser??tions. Furthermore, it can check C and C++ > for > > consistency with other languages, such as Verilog. The verification is > > performed by unwinding the loops in the program and passing the > re??sul??ting > > equation to a decision procedure. > > > > While CBMC is aimed for embedded software, it also supports dynamic > memory > > allocation using malloc and new. > > > > CBMC comes with a built-in solver for bit-vector formulas that is based > on > > MiniSat. As an alternative, CBMC has featured support for external SMT > solvers > > since version 3.3. The solvers we recommend are (in no particular order) > > Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be > > installed separately and have different licensing conditions. > > > > # portcheck > > Makefile does not have $OpenBSD$ RCS tag at the top > > patches/patch-Makefiles does not have $OpenBSD$ RCS tag at the top > > patches/patch-bigint-fix-includes does not have $OpenBSD$ RCS tag at > the top > > devel/cbmc > > > > Content of the archive: > > devel/cbmc > > devel/cbmc/Makefile > > devel/cbmc/patches > > devel/cbmc/patches/patch-Makefiles > > devel/cbmc/patches/patch-bigint-fix-includes > > devel/cbmc/distinfo > > devel/cbmc/pkg > > devel/cbmc/pkg/PLIST > > devel/cbmc/pkg/DESCR > > > > BR > > Simon > > >
Re: [NEW] cbmc - Bounded Model Checker for C and C++
Hi Simon, first, nice port. I would like to test my own code with it. But you missed the clang dependency. Your port is new and don't need a REVISION. bsd,port.mk(5): REVISION Revision number of the current package. Defaults to empty (very first package),... Why do you not fixed the missing RCS tags of the portscheck you made? Little nitpick: as far as I know its more common to use spaces between variables and their equals signs like in /usr/ports/infrastructure/templates/Makefile.template. bye, Jan log: ## Entering big-int gmake -C big-int gmake[1]: Entering directory '/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' clang++ -c -MMD -MP -std=c++11 -Wall -O2 -o bigint-func.o bigint-func.cc gmake[1]: clang++: Command not found gmake[1]: *** [../common:183: bigint-func.o] Error 127 gmake[1]: Leaving directory '/usr/ports/pobj/cbmc-5.5/cbmc-cbmc-5.5/src/big-int' gmake: *** [Makefile:50: big-int.dir] Error 2 *** Error 2 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2671 '/usr/ports/pobj/cbmc-5.5/.build_done') *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1884 '/usr/ports/packages/amd64/all/cbmc-5.5p0.tgz') *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2409 '_internal-package') *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:2389 'package') *** Error 1 in . (/usr/ports/infrastructure/mk/bsd.port.mk:1901 '/var/db/pkg/cbmc-5.5p0/+CONTENTS') *** Error 1 in /usr/ports/devel/cbmc (/usr/ports/infrastructure/mk/bsd.port.mk:2389 'install') On Fri, Oct 14, 2016 at 08:15:21PM +0200, Simon Mages wrote: > Hi, > > this is my first port, i hope everything is fine. > > A college of mine was using this tool to analyse some C code. I think this > tool is pretty interesting and can be put to good use for all sorts of > programs > or parts of it. > > COMMENT= Bounded Model Checker for C and C++ programs > > # cat pkg/DESCR > CBMC is a Bounded Model Checker for C and C++ programs. It supports C89, C99, > most of C11 and most compiler extensions provided by gcc and Visual Studio. It > also supports SystemC using Scoot. We have recently added experimental support > for Java Bytecode. > > CBMC verifies array bounds (buffer overflows), pointer safety, ex??cep??tions > and user-specified as??ser??tions. Furthermore, it can check C and C++ for > consistency with other languages, such as Verilog. The verification is > performed by unwinding the loops in the program and passing the re??sul??ting > equation to a decision procedure. > > While CBMC is aimed for embedded software, it also supports dynamic memory > allocation using malloc and new. > > CBMC comes with a built-in solver for bit-vector formulas that is based on > MiniSat. As an alternative, CBMC has featured support for external SMT solvers > since version 3.3. The solvers we recommend are (in no particular order) > Boolector, MathSAT, Yices 2 and Z3. Note that these solvers need to be > installed separately and have different licensing conditions. > > # portcheck > Makefile does not have $OpenBSD$ RCS tag at the top > patches/patch-Makefiles does not have $OpenBSD$ RCS tag at the top > patches/patch-bigint-fix-includes does not have $OpenBSD$ RCS tag at the top > devel/cbmc > > Content of the archive: > devel/cbmc > devel/cbmc/Makefile > devel/cbmc/patches > devel/cbmc/patches/patch-Makefiles > devel/cbmc/patches/patch-bigint-fix-includes > devel/cbmc/distinfo > devel/cbmc/pkg > devel/cbmc/pkg/PLIST > devel/cbmc/pkg/DESCR > > BR > Simon