CBMC

cbmc:deprecate_parametert_identifier

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

Branch merges

Branch information

Name:
deprecate_parametert_identifier
Repository:
lp:cbmc

Recent commits

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

deprecate parametert::get/set_identifier

This deprecates both parametert::get_identifier() and
parametert::set_identifier(). There has been a comment announcing this
since 2013.

Users of goto programs are meant to use
goto_functiont::parameter_identifiers. It remains to resolve the interface
that is used to pass these identifiers into goto_convert.

95e15fd... by Michael Tautschnig

Merge pull request #4251 from tautschnig/parameter-identifiers-locals

Local bitvector analysis: use parameter_identifiers [blocks: #4167]

17623d1... by Michael Tautschnig

Merge pull request #4099 from NathanJPhillips/documentation/symex

Symex Documentation

a35d547... by Michael Tautschnig

Merge pull request #2511 from polgreen/fix_trace_wording

Change "violated assumption" to "assumption" in trace

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

Local bitvector analysis: use parameter_identifiers

goto_functiont::type will go away.

c2f5c9b... by Nathan Phillips <email address hidden>

Improve documentation for goto_symext

0e65eb8... by Nathan Phillips <email address hidden>

Added code documentation

aead710... by Nathan Phillips <email address hidden>

Documentation formatting

e2c7ae7... by Nathan Phillips <email address hidden>

Moved parameters to match header file

8c1ffc9... by Polgreen <email address hidden>

make assumption output in trace reachable

Assumptions are never violated, instead they restrict the search space for non-det values