Code

Document and refactor goto check#4611

Code

Merged

xbauch merged 13 commits intodiffblue:developdiffblue/cbmc:developfrom

xbauch:refactor/goto-checkxbauch/cbmc:refactor/goto-checkCopy head branch name to clipboard

May 19, 2019

Commits

Commits on May 19, 2019

• Separate checking address-of expressions

  Show description for 60e119d
  petr-bauch

  committed
  60e119d

  Copy full SHA for 60e119d

• Clean-up and document check_rec_address

  Show description for a3f70a7
  petr-bauch

  committed
  a3f70a7

  Copy full SHA for a3f70a7

• Separate checking logical operators

  Show description for 41f7f46
  petr-bauch

  committed
  41f7f46

  Copy full SHA for 41f7f46

• Clean-up and document check_rec_logical_op

  Show description for 102b5b0
  petr-bauch

  committed
  102b5b0

  Copy full SHA for 102b5b0

• Refactor, rename, and document add_guarded_claim

  Show description for 1f105fe
  petr-bauch

  committed
  1f105fe

  Copy full SHA for 1f105fe

• Separate and refactor checking if

  Show description for d74ef71
  petr-bauch

  committed
  d74ef71

  Copy full SHA for d74ef71

• Separate and refactor checking member

  Show description for 266f00b
  petr-bauch

  committed
  266f00b

  Copy full SHA for 266f00b

• Separate and document checking arithmetic ops

  Show description for 2662f2b
  petr-bauch

  committed
  2662f2b

  Copy full SHA for 2662f2b

• Document and refactor invalidate

  Show description for f931965
  petr-bauch

  committed
  f931965

  Copy full SHA for f931965

• Use make_assumption/assertion wrappers

  Show description for c7c94b2
  petr-bauch

  committed
  c7c94b2

  Copy full SHA for c7c94b2

• Use built-in methods

  Show description for cecc289
  petr-bauch

  committed
  cecc289

  Copy full SHA for cecc289

• Add documentation

  Show description for e0eab84
  petr-bauch

  committed
  e0eab84

  Copy full SHA for e0eab84

• Clang-formatting

  Show description for b5060ee
  petr-bauch

  committed
  b5060ee

  Copy full SHA for b5060ee