Code

klaas' Contracts work#3769

Code

Closed

karkhaz wants to merge 16 commits intodiffblue:developdiffblue/cbmc:developfrom

karkhaz:kk-contractskarkhaz/cbmc:kk-contractsCopy head branch name to clipboard

Commits

Commits on Jan 11, 2019

• Adds --expand-pointer-predicates to goto-instrument

  Show description for aa16319
  

  klaas

  authored and

  karkhaz

  committed
  aa16319

  Copy full SHA for aa16319

• Adds a one-argument points_to_valid_memory

  Show description for dc583e6
  

  klaas

  authored and

  karkhaz

  committed
  dc583e6

  Copy full SHA for dc583e6

• Adds tests for --expand-pointer-predicates

  

  klaas

  authored and

  karkhaz

  committed
  0d79dc4

  Copy full SHA for 0d79dc4

• Splits code contracts into check(WIP) and apply

  Show description for 40bd1b3
  

  klaas

  authored and

  karkhaz

  committed
  40bd1b3

  Copy full SHA for 40bd1b3

• Reworks checking of code contracts

  Show description for bdebfb6
  

  klaas

  authored and

  karkhaz

  committed
  bdebfb6

  Copy full SHA for bdebfb6

• Removes some dead code.

  Show description for 6166221
  

  klaas

  authored and

  karkhaz

  committed
  6166221

  Copy full SHA for 6166221

• Cleans up some loops to have braces

  

  klaas

  authored and

  karkhaz

  committed
  724ed52

  Copy full SHA for 724ed52

• Disambiguates two exprts with the same ID.

  Show description for 474be8f
  

  klaas

  authored and

  karkhaz

  committed
  474be8f

  Copy full SHA for 474be8f

• Turns some checks into DATA_INVARIANTs

  

  klaas

  authored and

  karkhaz

  committed
  248accf

  Copy full SHA for 248accf

• Fixes bugs making goto_rw too conservative

  Show description for 4a0ea4b
  

  klaas

  authored and

  karkhaz

  committed
  4a0ea4b

  Copy full SHA for 4a0ea4b

• Adds slice24 test.

  

  klaas

  authored and

  karkhaz

  committed
  21e6d39

  Copy full SHA for 21e6d39

• Code contracts: match up introducing/removing parameter map modifications

  Show description for 599ae62
  

  tautschnig

  authored and

  karkhaz

  committed
  599ae62

  Copy full SHA for 599ae62

• Adds havocking for function calls

  Show description for 8784880
  

  klaas

  authored and

  karkhaz

  committed
  8784880

  Copy full SHA for 8784880

• Fixes initialization for code contracts

  Show description for 98c9bf7
  

  klaas

  authored and

  karkhaz

  committed
  98c9bf7

  Copy full SHA for 98c9bf7

• Makes code contracts use goto_rw for write sets

  Show description for 47d43e6
  

  klaas

  authored and

  karkhaz

  committed
  47d43e6

  Copy full SHA for 47d43e6

• Adds comments & help to code_contracts

  Show description for abe1f5a
  

  klaas

  authored and

  karkhaz

  committed
  abe1f5a

  Copy full SHA for abe1f5a