Code

WIP: Heapster/try unifying arrays#1650

Code

Merged

mergify[bot] merged 9 commits intomasterGaloisInc/saw-script:masterfrom heapster/arrays-unifyGaloisInc/saw-script:heapster/arrays-unifyCopy head branch name to clipboardMay 2, 2022

+103-31

Commits

Commits on Apr 29, 2022

• Eliminate field-shaped blocks in the array prover.

  abakst

  committed
  50ddf87

• Add test for blocks with sequence of field shapes

  abakst

  committed
  147d85c

• Fix broken testcase

  abakst

  committed
  9220cec

• Try solving for array lifetime/rw modality.

  abakst

  committed
  12e1d87

Commits on May 2, 2022

• Merge branch 'master' into heapster/arrays-unify

  

  Eddy Westbrook

  authored
  90425ea

• updated the translation of LLVM global constants to not use the "show" method to convert symbol names to strings

  

  Eddy Westbrook

  committed
  92b699a

• fixed a type error message, which was saying "not a sort" when it was supposed to say "not a tuple"

  

  Eddy Westbrook

  committed
  fa82780

• fixed translateLLVMValue on string values, which was somehow giving an incorrect translation; also fixed up the comments on translateLLVMValue to help clarify what it is supposed to return

  

  Eddy Westbrook

  committed
  5f6f718

• bug fix: changed implLLVMArrayBorrowed to check for the block permission used by the rule having the same shape as the array permission cell; changed the call to this rule in proveLLVMArray to ensu…

  Show description for ba63344
  

  Eddy Westbrook

  committed
  ba63344