Code

Use BDDs for encoding symex guards#3730

Code

Merged

romainbrenguier merged 18 commits intodiffblue:developdiffblue/cbmc:developfrom

romainbrenguier:experiment/bdd-guards4romainbrenguier/cbmc:experiment/bdd-guards4Copy head branch name to clipboard

Mar 7, 2019

Commits

Commits on Mar 7, 2019

• Reformat guard.cpp and guard.h

  Show description for a5c9790
  romainbrenguier

  committed
  a5c9790

  Copy full SHA for a5c9790

• Move guardt to analyses module

  Show description for decfe4a
  romainbrenguier

  committed
  decfe4a

  Copy full SHA for decfe4a

• Replace use of guardt by operandst in symex_assign

  Show description for 115011a
  romainbrenguier

  committed
  115011a

  Copy full SHA for 115011a

• Add guard_manager class and pass it around

  Show description for 9727c5e
  romainbrenguier

  committed
  9727c5e

  Copy full SHA for 9727c5e

• Remove unused field ns field of bdd_exprt

  Show description for 4da4bd3
  romainbrenguier

  committed
  4da4bd3

  Copy full SHA for 4da4bd3

• Remove root field of bdd_exprt

  Show description for f9a698c
  romainbrenguier

  committed
  f9a698c

  Copy full SHA for f9a698c

• Define idt type for bdd_node::id() functions

  Show description for f640d73
  romainbrenguier

  committed
  f640d73

  Copy full SHA for f640d73

• Add a cache to as_expr function for BDDs

  Show description for c63b9df
  romainbrenguier

  committed
  c63b9df

  Copy full SHA for c63b9df

• New implementation of guards using BDDs

  Show description for f164c83
  romainbrenguier

  committed
  f164c83

  Copy full SHA for f164c83

• Move guard implementation to guard_expr.h/cpp

  Show description for de291f6
  romainbrenguier

  committed
  de291f6

  Copy full SHA for de291f6

• Rename class to guard_exprt

  Show description for c8d8c48
  romainbrenguier

  committed
  c8d8c48

  Copy full SHA for c8d8c48

• Switch between guard bdd and guard expr

  Show description for eba0713
  romainbrenguier

  committed
  eba0713

  Copy full SHA for eba0713

• Document the BDD_GUARDS compilation flag

  Show description for fccd412
  romainbrenguier

  committed
  fccd412

  Copy full SHA for fccd412

• Add is_always_simplified field in guard implementations

  Show description for ff79e86
  romainbrenguier

  committed
  ff79e86

  Copy full SHA for ff79e86

• Enable BDD_GUARDS in one of the travis steps

  Show description for f4afbd1
  romainbrenguier

  committed
  f4afbd1

  Copy full SHA for f4afbd1

• Deactivate a test which takes too long with BDDs

  Show description for a50678c
  romainbrenguier

  committed
  a50678c

  Copy full SHA for a50678c

• Make guard_expr return a value

  Show description for 7503ac6
  romainbrenguier

  committed
  7503ac6

  Copy full SHA for 7503ac6

• Apply clang-format suggestions

  Show description for 22ed54b
  romainbrenguier

  committed
  22ed54b

  Copy full SHA for 22ed54b