Code

Support loop-contracts in Pallas#1305

Code

Draft

RobertMensing wants to merge 11 commits intodevutwente-fmt/vercors:devfrom pallas-loop-contractsutwente-fmt/vercors:pallas-loop-contractsCopy head branch name to clipboard

+1,737-205

Commits

Commits on Feb 3, 2025

• Started to add support for loop-invariants in Pallas specifications

  RobertMensing

  committed
  6fd78bb

  Copy full SHA for 6fd78bb

Commits on Feb 5, 2025

• Added vscode-files to gitignore

  RobertMensing

  committed
  ae63639

  Copy full SHA for ae63639

Commits on Feb 6, 2025

• Added support for loop-invariants to C++-side of Pallas

  RobertMensing

  committed
  d34a814

  Copy full SHA for d34a814

• Bugfixes regarding Pallas loop invariants

  RobertMensing

  committed
  6fd8259

  Copy full SHA for 6fd8259

Commits on Feb 7, 2025

• Fixed construction of Pallas invariants

  RobertMensing

  committed
  ea06f20

  Copy full SHA for ea06f20

• Remove redundant casts from LLVM encoding

  RobertMensing

  committed
  d2b238d

  Copy full SHA for d2b238d

• Merge remote-tracking branch 'origin/dev' into pallas-loop-contracts

  RobertMensing

  committed
  29d70f7

  Copy full SHA for 29d70f7

Commits on Feb 10, 2025

• Fixed non-termination issue when handling loop-invariants

  RobertMensing

  committed
  f56f250

  Copy full SHA for f56f250

• Generate permissions-invariants for variables allocated with alloca

  RobertMensing

  committed
  2735a64

  Copy full SHA for 2735a64

• Refined generatoion of permission-invariants for Pallas loops

  RobertMensing

  committed
  681d1dc

  Copy full SHA for 681d1dc

Commits on Feb 11, 2025

• Added tests for loops in Pallas & fixed bug with for-loops

  RobertMensing

  committed
  adeae32

  Copy full SHA for adeae32