Code

Array cell sensitivity#4680

Code

Closed

romainbrenguier wants to merge 21 commits intodiffblue:developdiffblue/cbmc:developfrom

romainbrenguier:feature/array-cell-sensitivityromainbrenguier/cbmc:feature/array-cell-sensitivityCopy head branch name to clipboard

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

• Make field sensitivity max array size configurable

  Show description for 163d6b4
  romainbrenguier

  committed
  163d6b4

  Copy full SHA for 163d6b4

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

  Show description for ab8fd3b
  romainbrenguier

  committed
  ab8fd3b

  Copy full SHA for ab8fd3b

• Add tests for field sensitivity options

  Show description for 9684a25
  romainbrenguier

  committed
  9684a25

  Copy full SHA for 9684a25