cbmc:saswat-chc-rebased

Last commit made on 2022-02-17
Get this branch:
git clone -b saswat-chc-rebased https://git.launchpad.net/cbmc

Branch merges

Branch information

Name:
saswat-chc-rebased
Repository:
lp:cbmc

Recent commits

61c3414... by Saswat Padhi <email address hidden>

fix minor sign comparison warnings

52af4f0... by Grigory Fedyukovich <email address hidden>

misc fixes after rebase
 - using standard CProver's array data structures (with, index)
 - more careful use of declarations (GOTO vs C)
 - serializing pointer names for further decoding

da905e6... by Grigory Fedyukovich <email address hidden>

added pointer dereferencing check;
fixed minor bugs; added more regression tests

f152a96... by Fedyukovich <fedyukog@3c22fbc6aedc.ant.amazon.com>

CHC generation at the level of basic blocks
initial support for memory; regression tests

4616645... by Saswat Padhi <email address hidden>

initial encoding logic

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

quantifiers over multiple variables

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

Merge pull request #6595 from tautschnig/bugfixes/6592-param-files

goto-cc: newlines in command files are just whitespace

9d9e213... by Michael Tautschnig <email address hidden>

Merge pull request #6587 from diffblue/remove_ID_size_usage

array_typet and vector_typet APIs

195458a... by Michael Tautschnig <email address hidden>

Merge pull request #6588 from diffblue/c_enum_underlying_type

c_enum_typet::underlying_type() and c_bitfield_typet::underlying_type()

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

Merge pull request #6585 from diffblue/quantifier-multi-binding

Quantifiers with multiple bindings