CBMC

cbmc:decision_procedure3

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

Branch merges

Branch information

Name:
decision_procedure3
Repository:
lp:cbmc

Recent commits

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

use new handle API

106da9a... by Daniel Kroening <email address hidden>

introduce ranged for in prop_minimizet

016c8d1... by Daniel Kroening <email address hidden>

move l_get and convert back into prop_convt

prop_convt is an instance of decision_proceduret that uses propositional
logic.

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

cover_goalst does not need prop_convt

No methods of prop_convt are used.

22e71cd... by Daniel Kroening <email address hidden>

use new handle interface in cover_goals

The literal-based interface is more specific, and cover_goals doesn't
require anything beyond what decision_proceduret offers.

23d2409... by Daniel Kroening <email address hidden>

introduce ranged for in cover_goals

91f8fd8... by Daniel Kroening <email address hidden>

elaborate prop_convt::handle(expr)

This change adds three features:

1) Non-boolean expressions are returned verbatim.

2) Boolean expressions that are determined to be a constant (e.g., by means
of constant folding) are returned as constants, to enable further
optimisation by users.

3) Literals returned are frozen, to simplify incremental usage.

21811fa... by Michael Tautschnig

Merge pull request #4524 from antlechner/antonia/fewer-param-constructors

Use constructors with fewer parameters if possible, for dereference_exprt and plus_exprt

c7fa8e7... by Michael Tautschnig

Merge pull request #4526 from tautschnig/fix-pointer-comparison

NULL compares equal to 0

8f68057... by Michael Tautschnig <email address hidden>

NULL compares equal to 0 when config.ansi_c.NULL_is_zero is set

When comparing constants, we just compared their string representations.
This fails when one side of the (in)equality was NULL while the other
side was 0, which is wrong when config.ansi_c.NULL_is_zero is set. Thus
actually test both sides for being zero in this configuration.