Stuart Henderson <s...@spacehopper.org> writes: > On 2016/10/20 22:11, Jeremie Courreges-Anglas wrote: >> Jeremie Courreges-Anglas <j...@wxcvbn.org> writes: >> >> > Simon Mages <mages.si...@googlemail.com> 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
