Improvements to code contracts [depends-on: #2646, #2676, blocks: #2712]#2677

Closed

qaphla wants to merge 13 commits intodiffblue:developfrom

qaphla:contracts_part2

Commits on Aug 3, 2018

Splits code contracts into check(WIP) and apply
klaas
committed
Reworks checking of code contracts
klaas
committed
Removes some dead code.
klaas
committed
Cleans up some loops to have braces
klaas
committed
Disambiguates two exprts with the same ID.
klaas
committed
Turns some checks into DATA_INVARIANTs
klaas
committed
Fixes bugs making goto_rw too conservative
klaas
committed
Adds slice24 test.
klaas
committed
Code contracts: match up introducing/removing parameter map modifications

tautschnig
authored and
klaas
committed
Adds havocking for function calls
klaas
committed
Fixes initialization for code contracts
klaas
committed
Makes code contracts use goto_rw for write sets
klaas
committed
Cleans up comments in code_contracts
klaas
committed