BSD Ports

devel/cbmc 6.11.0 FreeBSD

Bounded Model Checker for C and C++ programs

System
FreeBSD
Repository
FreeBSD ports
Maintainer
[email protected]
Last update
Commit
eecb07b6f5
License
BSD4CLAUSE
Categories
devel
Package size
23191.4 KiB, 146037.0 KiB installed

Description

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 allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions. 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 resulting equation to a decision procedure.

In the other systems

SystemPortVersion
FreeBSDdevel/cbmc6.11.0
OpenBSDdevel/cbmc6.7.1

Install

Binary package:

pkg install cbmc

From the ports tree:

cd /usr/ports/devel/cbmc/ && make install clean

To depend on this port in another port's Makefile:

RUN_DEPENDS=	cbmc>0:devel/cbmc

Packages

The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.

Repositoryaarch64amd64armv6armv7i386
FreeBSD:14:latest6.11.06.11.0-6.4.16.11.0
FreeBSD:14:quarterly6.11.06.11.0n/a6.4.16.11.0
FreeBSD:15:latest6.11.06.11.0n/a6.4.16.4.1
FreeBSD:15:quarterly6.11.06.11.0n/an/an/a
FreeBSD:16:latest6.11.06.11.0n/an/an/a
FreeBSD:16:quarterlyn/an/an/an/an/a

Dependencies

As this port's Makefile names them.

Build 4

Runtime 2

The full lists below include those, and their dependencies in turn.

Build dependencies 31
Run dependencies 64

No port depends on this one.

Configuration

No options to configure.

USES
cmake bison python shebangfix perl5
Service scripts
none

Files

Manual pages 11
  • cbmc(1)
  • crangler(1)
  • goto-analyzer(1)
  • goto-cc(1)
  • goto-diff(1)
  • goto-gcc(1)
  • goto-harness(1)
  • goto-instrument(1)
  • goto-ld(1)
  • goto-synthesizer(1)
  • symtab2gb(1)
pkg-plist 30
  • bin/cbmc
  • bin/cprover
  • bin/crangler
  • bin/goto-analyzer
  • bin/goto-cc
  • bin/goto-diff
  • bin/goto-gcc
  • bin/goto-harness
  • bin/goto-inspect
  • bin/goto-instrument
  • bin/goto-ld
  • bin/goto-synthesizer
  • bin/ls_parse.py
  • bin/symtab2gb
  • etc/bash_completion.d/cbmc
  • include/cprover/api.h
  • include/cprover/api_options.h
  • include/cprover/verification_result.h
  • lib/libcprover..a
  • share/man/man1/cbmc.1.gz
  • share/man/man1/crangler.1.gz
  • share/man/man1/goto-analyzer.1.gz
  • share/man/man1/goto-cc.1.gz
  • share/man/man1/goto-diff.1.gz
  • share/man/man1/goto-gcc.1.gz
  • share/man/man1/goto-harness.1.gz
  • share/man/man1/goto-instrument.1.gz
  • share/man/man1/goto-ld.1.gz
  • share/man/man1/goto-synthesizer.1.gz
  • share/man/man1/symtab2gb.1.gz
distinfo 2
FileSizeSHA256
minisat2_2.2.1.orig.tar.gz44229e54afa3c192c1753bc8075c0c7e126d5c495d9066e3f90a2588091149ac9ca40
diffblue-cbmc-cbmc-6.11.0_GH0.tar.gz9.183866e+06217e5ed631bbd4b39659fde37a603482003605abd4cb2586b09c2da344d925db
Master sites 1
  • DEBIAN/pool/main/m/minisat2:minisat

Commit history 5

DateCommitCreditsLog message
eecb07b6f5 Olivier Cochard devel/cbmc: update to 6.11.0
c3ee0d25f0 Älven math/z3: Update 5.0.0.0 => 5.1.0.0
Approved by: arrowd@ (maintainer) Approved by: db@, yuri@ (Mentors, implicit) Differential Revision: https://reviews.freebsd.org/D58886
42678686fc Piotr Kubaj devel/cbmc: fix build on powerpc64*
1. powerpc64 always uses 64-bit long double. 2. powerpc64le before 16.0 uses 64-bit long double and switched to 128-bit IEEE long double in 16.0.
dfa5362257 Yuri Victorovich math/z3: update 4.16.0.0 → 5.0.0.0
PR: 297106 Approved by: Gleb Popov <[email protected]> (maintainer)
bc7bba7f5c Olivier Cochard devel/cbmc: update to 6.10.0