Re: [NEW] cbmc - Bounded Model Checker for C and C++

2016-10-22 Thread Jeremie Courreges-Anglas 

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++

2016-10-20 Thread Jeremie Courreges-Anglas 
Stuart Henderson  writes:

> 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++

2016-10-20 Thread Stuart Henderson 
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..." ?

| 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++

2016-10-20 Thread Jeremie Courreges-Anglas 
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.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++

2016-10-18 Thread Jeremie Courreges-Anglas 
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.



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++

2016-10-18 Thread Simon Mages 
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++

2016-10-17 Thread 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++

2016-10-16 Thread 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.

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++

2016-10-16 Thread Simon Mages 
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++

2016-10-16 Thread 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.

Re: [NEW] cbmc - Bounded Model Checker for C and C++

2016-10-16 Thread Simon Mages 
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++

2016-10-16 Thread 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++

2016-10-16 Thread Simon Mages 
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++

2016-10-15 Thread Jan Klemkow 
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