CBMC

cbmc:kk-klaas-squash

  1. Git
  2. lp:cbmc
  3. kk-klaas-squash
Last commit made on 2019-07-17
Get this branch:
git clone -b kk-klaas-squash https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
kk-klaas-squash
Repository:
lp:cbmc

Recent commits

4d58f88... by Kareem Khazem <email address hidden>

Whitespace fixes in preparation for func contracts

This commit applies clang-format and other whitespace changes introduced
by future commits, which introduce function contracts.

3e2bea3... by Michael Tautschnig <email address hidden>

Merge pull request #4903 from tautschnig/memcpy-strings

Support OBJECT_SIZE over string constants

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

Merge pull request #4902 from tautschnig/bitand

Value sets: Support bitand/bitor over pointers

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

Value sets: Support bit operations over pointers

Bit operations on pointers are used to defend against side channels
resulting from speculative execution. Hence we need to support these.
Without the support in value sets we silently just returned "unknown"
and thus subsequent dereferencing would fail.

1ba3dfb... by Michael Tautschnig <email address hidden>

Support OBJECT_SIZE over string constants

Pointer checks (including __CPROVER_{r,w}_ok) over string constants
should succeed when the access is within bounds. To do so, we must no
return non-deterministic values for the object size of string constants.

Fixes: #4871

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

Merge pull request #4900 from tautschnig/null-pointer-fix

Null-pointer filtering must handle unknown offsets

250b140... by Michael Tautschnig <email address hidden>

Merge pull request #4874 from diffblue/simplifier_new_interface3

Simplifier: new interface, final piece [blocks: #4904]

412754c... by Daniel Kroening <email address hidden>

improved typing in simplify_boolean

This improves type safety.

16e18d2... by Daniel Kroening <email address hidden>

removed unneeded call to simplify_node in simplify_boolean

Follow-up from comment in #4872. The call is a no-op.

2099dfe... by Daniel Kroening <email address hidden>

type simplify_unary_plus

This improves type safety.