CBMC

cbmc:prop_propositional

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

Branch merges

Branch information

Name:
prop_propositional
Repository:
lp:cbmc

Recent commits

30ddd4a... by Daniel Kroening <email address hidden>

rename prop -> propositional

7dd720b... by Michael Tautschnig

Merge pull request #4502 from tautschnig/parameter-names

Ensure Java stubbing names parameters [blocks: #4485]

607df45... by antlechner <email address hidden>

Merge pull request #4506 from antlechner/antonia/class-identifier-param

Remove unused class_identifier parameter from Java object factory

6c46e2c... by Michael Tautschnig

Merge pull request #4504 from romainbrenguier/bugfix/verbosity0

Set verbosity to 0 for null_message_handlert

b97b80a... by Antonia Lechner <email address hidden>

Inline qualified_clsid variable

Naming this variable only duplicates the information that is already
given in the name of the function set_class_identifier.

34d20fa... by Antonia Lechner <email address hidden>

Remove unused class_identifier parameter

This parameter was only "used" in gen_nondet_struct_init, where it was
assigned a new value before it was actually used.

5e8e414... by Romain Brenguier

Set verbosity to 0 for null_message_handlert

This avoids executing conditional message outputs on null message
handlers.

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

Ensure Java stubbing names parameters

For functions with a body we require that parameters are named so that
we can generate assignments to them (even when the body may not read the
value). Also guard against future regressions by sanity checking
parameter names for any converted function.

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

Model GCC's __builtin_clz{,l,ll}

Implement counting leading zeros based on algorithms described in
Hacker's Delight.

2825f54... by Romain Brenguier <email address hidden>

Merge pull request #4498 from romainbrenguier/bugfix/double-printing

Fix bug in the printing of double for limit values