Code

Penetrating by blocks#5779

Code

Merged

keyboardDrummer merged 52 commits intodafny-lang:masterdafny-lang/dafny:masterfrom keyboardDrummer:penetratingByBlockskeyboardDrummer/dafny:penetratingByBlocksCopy head branch name to clipboardOct 7, 2024

+1,281-1,217

Commits

Commits on Sep 16, 2024

• Add proof by statement

  keyboardDrummer

  committed
  d6f3951

  Copy full SHA for d6f3951

• Merge remote-tracking branch 'origin/master' into penetratingByBlocks

  keyboardDrummer

  committed
  84c7073

  Copy full SHA for 84c7073

• Pass AssertMode to all Assert calls

  keyboardDrummer

  committed
  a2f6b5c

  Copy full SHA for a2f6b5c

Commits on Sep 20, 2024

• Use free calls inside by blocks

  keyboardDrummer

  committed
  313ad7e

  Copy full SHA for 313ad7e

• Move code from BoogieGenerator.TrStatement into separate files

  keyboardDrummer

  committed
  174abf8

  Copy full SHA for 174abf8

• Use namespace directive

  keyboardDrummer

  committed
  5a2f37c

  Copy full SHA for 5a2f37c

• Start with removing pre and post call stuff

  keyboardDrummer

  committed
  ae6f060

  Copy full SHA for ae6f060

• Finish pre/post call cleanup

  keyboardDrummer

  committed
  3cdae72

  Copy full SHA for 3cdae72

• Remove the proof field everywhere but in BlockByProof

  keyboardDrummer

  committed
  9e7a558

  Copy full SHA for 9e7a558

• Update parser

  keyboardDrummer

  committed
  2b17edc

  Copy full SHA for 2b17edc

• Fix a few bugs

  keyboardDrummer

  committed
  0774dc4

  Copy full SHA for 0774dc4

• More use of BodyTranslationContext.AssertMode

  keyboardDrummer

  committed
  1049866

  Copy full SHA for 1049866

• Improve printing

  keyboardDrummer

  committed
  a8b2312

  Copy full SHA for a8b2312

• Rename of UpdateStmt

  keyboardDrummer

  committed
  0391450

  Copy full SHA for 0391450

• Add comments

  keyboardDrummer

  committed
  6b985cf

  Copy full SHA for 6b985cf

Commits on Sep 21, 2024

• Definite assignment tracking issue

  keyboardDrummer

  committed
  fe456d3

  Copy full SHA for fe456d3

• Definite assignment tracker changed so it's never cleaned up

  keyboardDrummer

  committed
  5af6b22

  Copy full SHA for 5af6b22

• Add substituter implementation

  keyboardDrummer

  committed
  6e6d73d

  Copy full SHA for 6e6d73d

Commits on Sep 23, 2024

• Prepare for using ordered dictionary for locals

  keyboardDrummer

  committed
  212cfbe

  Copy full SHA for 212cfbe

• Introduce Variables class to track Boogie variables using an ordered dictionary

  keyboardDrummer

  committed
  da8787e

  Copy full SHA for da8787e

• CallBy.dfy works now

  keyboardDrummer

  committed
  185834a

  Copy full SHA for 185834a

• CallByHide.dfy passes

  keyboardDrummer

  committed
  6f2dbf3

  Copy full SHA for 6f2dbf3

• Convert giant if to switch statement

  keyboardDrummer

  committed
  16f8ef7

  Copy full SHA for 16f8ef7

• Fix

  keyboardDrummer

  committed
  5415a97

  Copy full SHA for 5415a97

• Merge remote-tracking branch 'origin/master' into penetratingByBlocks

  keyboardDrummer

  committed
  00e11e8

  Copy full SHA for 00e11e8

• Ran formatter and def assignment improvement

  keyboardDrummer

  committed
  10ee669

  Copy full SHA for 10ee669

Commits on Sep 24, 2024

• Move to symbols for mapping to tracking variables

  keyboardDrummer

  committed
  2eea9e3

  Copy full SHA for 2eea9e3

• Fixes

  keyboardDrummer

  committed
  6560fc2

  Copy full SHA for 6560fc2

• More fixes

  keyboardDrummer

  committed
  e9db4b9

  Copy full SHA for e9db4b9

• Fix formatter

  keyboardDrummer

  committed
  0830162

  Copy full SHA for 0830162

• Merge commit 'ef13a72f3a9d3f' into penetratingByBlocks

  keyboardDrummer

  committed
  35442d9

  Copy full SHA for 35442d9

• Fix

  keyboardDrummer

  committed
  d4ca466

  Copy full SHA for d4ca466

• Fix expect file

  keyboardDrummer

  committed
  4dfbd8b

  Copy full SHA for 4dfbd8b

• Undo Def as tracking changes

  keyboardDrummer

  committed
  e8c409f

  Copy full SHA for e8c409f

• Fixes

  keyboardDrummer

  committed
  a078831

  Copy full SHA for a078831

• Update expect file

  keyboardDrummer

  committed
  e86fed8

  Copy full SHA for e86fed8

• Update tests

  keyboardDrummer

  committed
  67cdf7b

  Copy full SHA for 67cdf7b

• Update tests

  keyboardDrummer

  committed
  054140b

  Copy full SHA for 054140b

• Use an immediately dictionary instead of adding and removing

  keyboardDrummer

  committed
  ae8d333

  Copy full SHA for ae8d333

• Fix test generation

  keyboardDrummer

  committed
  a4796d2

  Copy full SHA for a4796d2

• Refactoring

  keyboardDrummer

  committed
  8ab5cb7

  Copy full SHA for 8ab5cb7

• Update test

  keyboardDrummer

  committed
  bdb02ae

  Copy full SHA for bdb02ae

• Add test-case for assign such that

  keyboardDrummer

  committed
  2f189bb

  Copy full SHA for 2f189bb

• Add tests

  keyboardDrummer

  committed
  880fa30

  Copy full SHA for 880fa30

• Add another test

  keyboardDrummer

  committed
  95a09a2

  Copy full SHA for 95a09a2

Commits on Sep 25, 2024

• Updates

  keyboardDrummer

  committed
  13a25b3

  Copy full SHA for 13a25b3

• Fix SubsetTypes

  keyboardDrummer

  committed
  46dc302

  Copy full SHA for 46dc302

• Merge branch 'master' into penetratingByBlocks

  keyboardDrummer

  authored
  946bdd6

  Copy full SHA for 946bdd6

Commits on Oct 6, 2024

• Remove todos

  keyboardDrummer

  committed
  f45a1a3

  Copy full SHA for f45a1a3

• Regenerated makefiles

  keyboardDrummer

  committed
  7cce358

  Copy full SHA for 7cce358

• Merge remote-tracking branch 'origin/master' into penetratingByBlocks

  keyboardDrummer

  committed
  d132f87

  Copy full SHA for d132f87

• Update doos

  keyboardDrummer

  committed
  f9c2fa3

  Copy full SHA for f9c2fa3