Code

Use bddt to simplify guardt#310

Code

Closed

tautschnig wants to merge 43 commits intodiffblue:developdiffblue/cbmc:developfrom

tautschnig:bdd-guardstautschnig/cbmc:bdd-guardsCopy head branch name to clipboard

Commits

Commits on Jul 19, 2017

• Handle array initialization with a non-array gracefully

  Show description for 9740142
  tautschnig

  committed
  9740142

  Copy full SHA for 9740142

Commits on Jul 20, 2017

• added a non-recursive variant of APPLY

  

  Daniel Kroening

  committed
  564f64c

  Copy full SHA for 564f64c

• disable linter for assertions

  

  Daniel Kroening

  committed
  a71ca41

  Copy full SHA for a71ca41

Commits on Jul 24, 2017

• Support out-of-bounds checks on arrays of dynamic size

  Show description for d078dd8
  tautschnig

  committed
  d078dd8

  Copy full SHA for d078dd8

Commits on Aug 1, 2017

• More complete modelling of fgets

  Show description for 6eef691
  tautschnig

  committed
  6eef691

  Copy full SHA for 6eef691

• Import getopt{,_long} and vasprintf models from SV-COMP/busybox

  Show description for f691135
  tautschnig

  committed
  f691135

  Copy full SHA for f691135

Commits on Aug 3, 2017

• Merge pull request #131 from tautschnig/struct-init-error

  Show description for 151efbc
  

  Daniel Kroening

  authored
  151efbc

  Copy full SHA for 151efbc

• increased version number in preparation for release 5.8

  

  Daniel Kroening

  committed
  eb96b70

  Copy full SHA for eb96b70

• Merge pull request #1144 from diffblue/miniBDD-non-recursive-apply

  Show description for 8e70eaa
  

  Daniel Kroening

  authored
  8e70eaa

  Copy full SHA for 8e70eaa

• fix for operator< on reverse_keyt in miniBDD, fixing segfault in ebmc

  

  Daniel Kroening

  committed
  439ef97

  Copy full SHA for 439ef97

• invariant_violated does not return

  

  Daniel Kroening

  committed
  393256f

  Copy full SHA for 393256f

• test for miniBDD

  

  Daniel Kroening

  committed
  ff945b3

  Copy full SHA for ff945b3

• Symex support for lhs-typecasts and side effects

  tautschnig

  committed
  879a47b

  Copy full SHA for 879a47b

• Extract elements of array, struct directly instead of simplifying

  Show description for 08f1a9e
  tautschnig

  committed
  08f1a9e

  Copy full SHA for 08f1a9e

• Removed redundant get_pc() (there is pc())

  tautschnig

  committed
  f281f88

  Copy full SHA for f281f88

• Fix symex thread statistics

  tautschnig

  committed
  52db9e4

  Copy full SHA for 52db9e4

• Extended symex progres statistics

  tautschnig

  committed
  c69a21b

  Copy full SHA for c69a21b

• Symex: output instruction processing and loop unwinding like CBMC

  Show description for acdc797
  tautschnig

  committed
  acdc797

  Copy full SHA for acdc797

• symex --max-search-time limit and cleanup

  Show description for 260e03d
  tautschnig

  committed
  260e03d

  Copy full SHA for 260e03d

• Perform function-pointer removal in symex

  tautschnig

  committed
  73adfb0

  Copy full SHA for 73adfb0

Commits on Aug 4, 2017

• Avoid using integer_typet where unsuitable

  Show description for e2ed0df
  tautschnig

  committed
  e2ed0df

  Copy full SHA for e2ed0df

• Merge pull request #1062 from diffblue/fix_for_miniBDD

  Show description for 0cad6f4
  

  Daniel Kroening

  authored
  0cad6f4

  Copy full SHA for 0cad6f4

• Merge pull request #151 from tautschnig/symex-improvements

  Show description for ea476f7
  

  Daniel Kroening

  authored
  ea476f7

  Copy full SHA for ea476f7

• Merge pull request #1167 from tautschnig/c-library-ext

  Show description for df81a9c
  

  Daniel Kroening

  authored
  df81a9c

  Copy full SHA for df81a9c

• Merge pull request #1035 from tautschnig/no_integer_typet

  Show description for bb9cef3
  

  Daniel Kroening

  authored
  bb9cef3

  Copy full SHA for bb9cef3

• Avoid spurious signed/unsigned comparison warnings

  Show description for a3578c0
  tautschnig

  committed
  a3578c0

  Copy full SHA for a3578c0

• Merge pull request #1205 from tautschnig/sign-compare-fix

  Show description for 652ea09
  

  Daniel Kroening

  authored
  652ea09

  Copy full SHA for 652ea09

• Merge pull request #1158 from tautschnig/array-bounds

  Show description for 76ae912
  

  Daniel Kroening

  authored
  76ae912

  Copy full SHA for 76ae912

• fix vacuous conjuncts

  

  Daniel Kroening

  committed
  de40333

  Copy full SHA for de40333

• Stop using C headers

  reuk

  committed
  548aeba

  Copy full SHA for 548aeba

• Update coding standard

  reuk

  committed
  33811ce

  Copy full SHA for 33811ce

• Enable extractbits over arbitrary types, fix byte extract omission

  Show description for 2f55076
  tautschnig

  committed
  2f55076

  Copy full SHA for 2f55076

• Merge pull request #1211 from tautschnig/fix-1209

  Show description for 9d3a99e
  

  Daniel Kroening

  authored
  9d3a99e

  Copy full SHA for 9d3a99e

Commits on Aug 5, 2017

• Merge pull request #1210 from reuk/stop-using-c-headers

  Show description for 4dd5405
  

  Daniel Kroening

  authored
  4dd5405

  Copy full SHA for 4dd5405

Commits on Aug 7, 2017

• goto-analyzer needs solvers (once BDDs are used in guardt), add binary

  tautschnig

  committed
  d994055

  Copy full SHA for d994055

• Use BDDs to simplify guard expressions

  tautschnig

  committed
  0fc3854

  Copy full SHA for 0fc3854

• BDDs require a namespace - pass one to guardt's or operator

  tautschnig

  committed
  db496e8

  Copy full SHA for db496e8

• guardt::operator-=: use member function instead of friend

  tautschnig

  committed
  5a0c488

  Copy full SHA for 5a0c488

• fixup! goto-analyzer needs solvers (once BDDs are used in guardt), add binary

  tautschnig

  committed
  a3b5808

  Copy full SHA for a3b5808

• bdd -> exprt: fix copy&paste error to avoid a && TRUE

  tautschnig

  committed
  4b2774b

  Copy full SHA for 4b2774b

• Alternative bdd -> exprt translation expanding ID_if

  Show description for 255f431
  tautschnig

  committed
  255f431

  Copy full SHA for 255f431

• Simplify ID_and, ID_or, ID_xor via BDDs - disabled

  Show description for 0696c4e
  tautschnig

  committed
  0696c4e

  Copy full SHA for 0696c4e

• Avoid use of sort_and_join in guard operations

  tautschnig

  committed
  02a6288

  Copy full SHA for 02a6288