CBMC

cbmc:unwind-counters4

  1. Git
  2. lp:cbmc
  3. unwind-counters4
Last commit made on 2018-04-08
Get this branch:
git clone -b unwind-counters4 https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
unwind-counters4
Repository:
lp:cbmc

Recent commits

57aedaa... by Daniel Kroening <email address hidden>

add test for unwinding counter reset

1d81306... by Michael Tautschnig

Merge pull request #2015 from tautschnig/fix-smt2_solver-clean

smt2_solver.{o,d} should be removed by "make clean"

392144d... by Michael Tautschnig <email address hidden>

Makefiles: Place .d suffix used for dependencies in DEPEXT variable

Also clean up unnecessary duplicate dependencies in solvers/

839d32a... by Michael Tautschnig <email address hidden>

smt2_solver.{o,d} should be removed by "make clean"

The set of files to be removed is inferred from the SRC variable, which does not
include smt2_solver.cpp. Hence the generated files need to be listed explicitly.

48e427a... by Michael Tautschnig

Merge pull request #1979 from romainbrenguier/regression/fix-indexOf-test

Set string-max-length in indexOf test

c2f3726... by Michael Tautschnig

Merge pull request #1976 from romainbrenguier/regression/activate-dependency-tests

Activate tests for StringBuffer.append in loops

69fb74a... by Michael Tautschnig

Merge pull request #1995 from tautschnig/byte-update-soundness

[SV-COMP'18 6/19] Abort on byte_update(pointer)

aa766ae... by Romain Brenguier

Set string-max-length in indexOf test

Without this, the solver can end up with a difficult instance for minisat.
This behavior depends on the envioronment in which CBMC/JBMC is build, for
instance travis and appVeyor may get different counter-examples from the
SAT-solver, because of slightly different inputs.
The behavior can also vary from one commit to the other on the same system (even
if the changes seem unrelated to the solvers).
However running the same benchmark on the same operating system with the same
version of CBMC/JBMC should always behave the same.

988b818... by Daniel Kroening <email address hidden>

Merge pull request #1990 from tautschnig/missing-header

[SV-COMP'18 1/19] Include missing header

8300147... by Michael Tautschnig <email address hidden>

Abort on byte_update(pointer)

Just ignoring them would yield unsound results.