Code

Array-cell sensitivity#5057

Code

Merged

smowton merged 21 commits intodiffblue:developdiffblue/cbmc:developfrom

smowton:romain/feature/array-cell-sensitivitysmowton/cbmc:romain/feature/array-cell-sensitivityCopy head branch name to clipboard

Aug 26, 2019

Commits

Commits on Aug 21, 2019

• Add L1_WITH_CONSTANT_PROPAGATION mode to goto_symex_statet::rename

  Show description for 13ccc77
  

  smowton

  authored and

  romainbrenguier

  committed
  13ccc77

  Copy full SHA for 13ccc77

• Symex: enable array cell sensitivity

  

  smowton

  authored and

  romainbrenguier

  committed
  1f33401

  Copy full SHA for 1f33401

• Array cell sensitivity: tolerate zero-length arrays

  

  smowton

  authored and

  romainbrenguier

  committed
  da30884

  Copy full SHA for da30884

• Resolve array indices before dereferencing

  Show description for 026a510
  

  smowton

  authored and

  romainbrenguier

  committed
  026a510

  Copy full SHA for 026a510

• Set a limit size for array cell propagation

  Show description for 7b958bf
  romainbrenguier

  committed
  7b958bf

  Copy full SHA for 7b958bf

• Attempt to get missing array size from symbol table

  Show description for 08a71e9
  romainbrenguier

  committed
  08a71e9

  Copy full SHA for 08a71e9

• Rename size to L2 in field_sensitivity::apply

  Show description for 22f3570
  romainbrenguier

  committed
  22f3570

  Copy full SHA for 22f3570

• Make field_sensitivity::apply handle non-constant index

  Show description for d11bece
  romainbrenguier

  committed
  d11bece

  Copy full SHA for d11bece

• Only apply field_sensitivity to dereferenced object

  Show description for 33e0037
  romainbrenguier

  committed
  33e0037

  Copy full SHA for 33e0037

• Apply field sensitivity in symex_printf

  Show description for e86810e
  romainbrenguier

  committed
  e86810e

  Copy full SHA for e86810e

• Allow trace to assign in two steps

  Show description for 91de164
  romainbrenguier

  committed
  91de164

  Copy full SHA for 91de164

• Adapt double_deref test for array cell sensitivity

  Show description for d857648
  romainbrenguier

  committed
  d857648

  Copy full SHA for d857648

• Tag test failing with SMT backend

  Show description for 162abbd
  romainbrenguier

  committed
  162abbd

  Copy full SHA for 162abbd

• Simplify lhs in build goto trace

  Show description for c3fdc33
  romainbrenguier

  committed
  c3fdc33

  Copy full SHA for c3fdc33

• Add tests for array-cell sensitivity

  Show description for c93c1ca
  

  smowton

  authored and

  romainbrenguier

  committed
  c93c1ca

  Copy full SHA for c93c1ca

• Document how arrays are handled by field sensitivity

  Show description for ca78842
  romainbrenguier

  committed
  ca78842

  Copy full SHA for ca78842

• Activate regression tests previously KNOWNBUG

  Show description for 08d43f9
  romainbrenguier

  committed
  08d43f9

  Copy full SHA for 08d43f9

• Add execution tests for array-cell-sensitivity

  Show description for 869f2cd
  

  smowton

  authored and

  romainbrenguier

  committed
  869f2cd

  Copy full SHA for 869f2cd

Commits on Aug 23, 2019

• Make field sensitivity max array size configurable

  Show description for 05e04bd
  

  romainbrenguier

  authored and

  smowton

  committed
  05e04bd

  Copy full SHA for 05e04bd

• Add max-field-sensitivity-array-size option

  Show description for edb9ad7
  

  romainbrenguier

  authored and

  smowton

  committed
  edb9ad7

  Copy full SHA for edb9ad7

• Add tests for field sensitivity options

  Show description for 123a68e
  

  romainbrenguier

  authored and

  smowton

  committed
  123a68e

  Copy full SHA for 123a68e