CBMC

cbmc:default-verbosity-status

  1. Git
  2. lp:cbmc
  3. default-verbosity-status
Last commit made on 2019-02-03
Get this branch:
git clone -b default-verbosity-status https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
default-verbosity-status
Repository:
lp:cbmc

Recent commits

83ce825... by Daniel Kroening <email address hidden>

change default verbosity of CBMC to 'status'

This reduces the amount of default output on the console.

4dc7725... by Daniel Kroening <email address hidden>

vector_typet::size() is now a constant_exprt

The codebase assumes basically globally that vector_typet::size() is a
constant_exprt. This is now enforced by the signature.

934f310... by Daniel Kroening <email address hidden>

C/C++ now have frontend_vector type

This enables distinguishing the case of a size that is an arbitary
expression from the case where the size is required to be constant.

4aa485f... by Michael Tautschnig

Merge pull request #3249 from romainbrenguier/refactor/propt-messaget

Stop propt inheriting from messaget [blocks: #3800]

c74d257... by Peter Schrammel <email address hidden>

Merge pull request #3968 from peterschrammel/cover-verifier

Add cover goals verifier [blocks: 3969]

756b003... by Romain Brenguier

Stop propt inheriting from messaget

No functional changes.
A propt object should not be used as a messaget so the messaget should
rather be a field.

969f5d6... by Peter Schrammel <email address hidden>

Update goto-checker docs

w.r.t. cover goals verifier

29509e5... by Peter Schrammel <email address hidden>

Use goto verifier for --cover in CBMC

instead of bmc_covert

Fixes --cover tests without property descriptions.
The unified property handling introduced in a1100e16
used by goto verifier does not allow properties
without description.

5d5d61b... by Peter Schrammel <email address hidden>

Add C test input generator

Replaces the test input extraction part of bmc_covert,
which is entirely independent of producing traces now.
To be moved into a prospective ccover tool.

27e3efd... by Peter Schrammel <email address hidden>

Fix unit test dependencies