Code

Function alloc soundness fix#6018

Code

Draft

typerSniper wants to merge 24 commits intodafny-lang:masterdafny-lang/dafny:masterfrom typerSniper:function-alloc-soundness-fixtyperSniper/dafny:function-alloc-soundness-fixCopy head branch name to clipboard

+50-49

Commits

Commits on Jan 6, 2025

• remove allocation definition axiom

  typerSniper

  committed
  e69d48e

  Copy full SHA for e69d48e

• ensure allocatedness for every function's return value

  typerSniper

  committed
  af9198d

  Copy full SHA for af9198d

• emit isAlloc assumptions for top-level functions when used and well-formed lambdas when defined

  typerSniper

  committed
  af8b4f0

  Copy full SHA for af8b4f0

• oops

  typerSniper

  committed
  2b5ff84

  Copy full SHA for 2b5ff84

Commits on Jan 7, 2025

• add back one implication

  typerSniper

  committed
  ca92279

  Copy full SHA for ca92279

Commits on Jan 8, 2025

• alloced only when heap!=null

  typerSniper

  committed
  8340693

  Copy full SHA for 8340693

• add nul check

  typerSniper

  committed
  808fa88

  Copy full SHA for 808fa88

Commits on Jan 17, 2025

• fix out

  typerSniper

  committed
  72dc4f1

  Copy full SHA for 72dc4f1

• Merge branch 'master' into function-alloc-soundness-fix

  typerSniper

  authored
  20072e3

  Copy full SHA for 20072e3

• move isalloc out of quantifier

  typerSniper

  committed
  d92565e

  Copy full SHA for d92565e

• dummy code

  typerSniper

  committed
  5c16f2e

  Copy full SHA for 5c16f2e

• format

  typerSniper

  committed
  f710bc5

  Copy full SHA for f710bc5

• Merge branch 'function-alloc-soundness-fix' of https://github.com/typerSniper/dafny into function-alloc-soundness-fix

  typerSniper

  committed
  122aa3a

  Copy full SHA for 122aa3a

Commits on Jan 29, 2025

• hand feed definition aximo

  typerSniper

  committed
  0229a30

  Copy full SHA for 0229a30

• remove unnecessary proof

  typerSniper

  committed
  5af74f3

  Copy full SHA for 5af74f3

• expect file update, new errror

  typerSniper

  committed
  b9fb825

  Copy full SHA for b9fb825

• update rc

  typerSniper

  committed
  ccbe830

  Copy full SHA for ccbe830

• new vc

  typerSniper

  committed
  86db816

  Copy full SHA for 86db816

• update check

  typerSniper

  committed
  abbdba0

  Copy full SHA for abbdba0

• Merge branch 'master' into function-alloc-soundness-fix

  typerSniper

  authored
  901dace

  Copy full SHA for 901dace

Commits on Jan 30, 2025

• remove probably unnecessary can call

  typerSniper

  committed
  e8b19cd

  Copy full SHA for e8b19cd

• Merge branch 'function-alloc-soundness-fix' of https://github.com/typerSniper/dafny into function-alloc-soundness-fix

  typerSniper

  committed
  f44285d

  Copy full SHA for f44285d

• Merge branch 'master' into function-alloc-soundness-fix

  typerSniper

  authored
  0d77373

  Copy full SHA for 0d77373

Commits on Feb 3, 2025

• Merge branch 'master' into function-alloc-soundness-fix

  typerSniper

  authored
  f11a294

  Copy full SHA for f11a294