Code

Array speedup#1874

Code

Closed

tautschnig wants to merge 6 commits intodevelopdiffblue/cbmc:developfrom array-speedupdiffblue/cbmc:array-speedupCopy head branch name to clipboard

+574-684

Commits

Commits on Apr 24, 2022

• Use instantiate() when flattening array_comprehension_exprt

  Show description for a2a4feb
  tautschnig

  committed
  a2a4feb

  Copy full SHA for a2a4feb

• Failing test to demonstrate need for extensionality rule

  Show description for 6f2263a
  tautschnig

  committed
  6f2263a

  Copy full SHA for 6f2263a

• Flattening: support index expressions over zero bitwidth arrays

  Show description for b2589d4
  tautschnig

  committed
  b2589d4

  Copy full SHA for b2589d4

• Test trace-values: create reads to enforce instantiation

  Show description for ecfb7ae
  tautschnig

  committed
  ecfb7ae

  Copy full SHA for ecfb7ae

• performance tests for reading/writing arrays

  

  Daniel Kroening

  authored and

  tautschnig

  committed
  2178a2f

  Copy full SHA for 2178a2f

• Array theory: implement weakly equivalent arrays

  Show description for a02b480
  

  Daniel Kroening

  and

  tautschnig

  committed
  a02b480

  Copy full SHA for a02b480