CBMC

cbmc:fix-function-depth

  1. Git
  2. lp:cbmc
  3. fix-function-depth
Last commit made on 2018-11-29
Get this branch:
git clone -b fix-function-depth https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
fix-function-depth
Repository:
lp:cbmc

Recent commits

5cb5d7e... by Daniel Kroening <email address hidden>

fix function depth display in case of hidden calls/returns

Previously, hidden function calls or hidden functions could cause the depth
count to get out of sync.

31060e1... by Daniel Kroening <email address hidden>

Merge pull request #3458 from diffblue/compact-trace

added --compact-trace option [blocks: #3459]

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

Merge pull request #3456 from diffblue/hide_call_CPROVER

Hide calls/returns from/to hidden functions

b62ffe9... by Daniel Kroening <email address hidden>

added --compact-trace option

This offers a denser way of viewing traces. The rationale is that traces
are getting longer; furthermore, the new format makes it easier to spot
function calls and the actual function parameters.

e754de7... by Michael Tautschnig

Merge pull request #3476 from diffblue/smt2_use_format

smt2_solver: use smt2_format instead of .pretty()

6fd0cf3... by Daniel Kroening <email address hidden>

Hide function calls and returns from and to hidden functions

This removes clutter in any counterexample traces; the assumption is that
hidden functions have no meaning for the user.

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

smt2_solver: use smt2_format instead of .pretty()

f0c59b5... by Daniel Kroening <email address hidden>

Merge pull request #3461 from diffblue/smt2_solver_get-value

SMT2 solver: implement get-value

aec39d5... by Michael Tautschnig

Merge pull request #3475 from martin-cs/fix/document-backtrace-option-in-makefile

Document the flag needed for function names in stack backtraces.

57e8cc6... by martin <martin@raphael>

Document the flag needed for function names in stack backtraces.

Glibc and Apple's libc both provide support for stack introspection.
This is used by the invariant code to generate a stack backtrace
on invariant failure. By default GCC strips out the function names
so an additional LINKFLAG is needed to get function names in the
backtrace. This was hidden^Wdocumented in util/invariant.cpp, this
patch adds it to config.inc so it can be more widely understood
and used.