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..." ? | 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.
