Code

Read clauses on methods#30

Code

Draft

robin-aws wants to merge 59 commits intomasterrobin-aws/dafny:masterfrom read-clauses-on-methodsrobin-aws/dafny:read-clauses-on-methodsCopy head branch name to clipboard

+1,504-319

Commits

Commits on Sep 16, 2021

• First step, adding to parser and Method model

  robin-aws

  committed
  1bf4616

Commits on Sep 17, 2021

• Split TheFrame into ReadsFrame and ModifiesFrame

  robin-aws

  committed
  6cf7685

• Just enough to support the first test case

  robin-aws

  committed
  e29db85

• Set default of "reads *" for methods

  robin-aws

  committed
  6fa7f62

Commits on Aug 4, 2023

• Merge branch 'master' of https://github.com/dafny-lang/dafny into read-clauses-on-methods

  Show description for c538c2b
  robin-aws

  committed
  c538c2b

• Partial fixes to bad merge

  robin-aws

  committed
  12c9933

• Remove zombie files from merge

  robin-aws

  committed
  41ee604

• More fixes

  robin-aws

  committed
  57d9919

• Another batch of error fixes

  robin-aws

  committed
  dbb4ce0

• Finally builds

  robin-aws

  committed
  9ce3f2a

• Fix test

  robin-aws

  committed
  905f103

• Address missing resolution etc.

  robin-aws

  committed
  bbeefdb

• Clean up WFOptions

  robin-aws

  committed
  7f77f7c

• Partially get test working

  robin-aws

  committed
  11d4a0d

Commits on Aug 14, 2023

• Missing cloning case

  robin-aws

  committed
  20118e6

Commits on Aug 15, 2023

• Default to reads *

  robin-aws

  committed
  f249adb

• Tweaks

  robin-aws

  committed
  b2b266c

Commits on Aug 17, 2023

• Fix iterators (different kind of reads frame)

  robin-aws

  committed
  e53422e

• Avoid reads checks when reads clause is * (not working yet?)

  robin-aws

  committed
  f1b1657

• Test todos

  robin-aws

  committed
  b2b3189

• Fixing check for wildcard, adding etran.WithReads/ModifiesClause()

  robin-aws

  committed
  46f9367

• Fix null readsFrame bug

  robin-aws

  committed
  e94bc0f

• Do reads checks on function by method bodies too

  robin-aws

  committed
  e0afd4a

• Clean up test file

  robin-aws

  committed
  f6dad35

Commits on Aug 18, 2023

• Updates to documentation

  robin-aws

  committed
  267acae

• Whitespace

  robin-aws

  committed
  7518121

Commits on Aug 19, 2023

• Apply reads clause to other clauses, {:concurrent} checks for empty frames

  robin-aws

  committed
  4f4ace4

• Typo fixes, more testing

  robin-aws

  committed
  22d8d4d

• Add WithDelayedReadsChecks

  robin-aws

  committed
  998b100

Commits on Aug 20, 2023

• Fix default values

  robin-aws

  committed
  37fa445

Commits on Aug 21, 2023

• Add ReadsCheckDelayer and apply it to other cases as well

  robin-aws

  committed
  0a82760

• Several missing calls to Method.Reads, beef up test cases

  robin-aws

  committed
  f7be5ed

• Whoops, dropping delayed reads checks statements

  robin-aws

  committed
  1a0d6be

• Subclassing and method call checks

  robin-aws

  committed
  38cdbf5

Commits on Aug 22, 2023

• Enable reads checks on statements outside of method contexts

  robin-aws

  committed
  a00fc44

• Trying out defaulting to reads {} on ghost methods

  robin-aws

  committed
  0a54826

Commits on Aug 23, 2023

• Lemmas instead of ghost methods

  robin-aws

  committed
  22a4867

Commits on Aug 25, 2023

• No reads or checking on lemmas, more LHS fixes, more tests

  robin-aws

  committed
  347563e

• update TODOs

  robin-aws

  committed
  af497ec

• Add option to enable, most testing (and reorganize old file tests)

  robin-aws

  committed
  275e56d

• More tests

  robin-aws

  committed
  1386c43

• Cloning another test file

  robin-aws

  committed
  1cb1175

• Remaining tests

  robin-aws

  committed
  0254121

• Whitespace and todos

  robin-aws

  committed
  82a160e

• Merge branch 'master' of https://github.com/dafny-lang/dafny into read-clauses-on-methods

  Show description for d376bf8
  robin-aws

  committed
  d376bf8

Commits on Aug 26, 2023

• Fix function-by-method handling, update test

  robin-aws

  committed
  ee39edc

Commits on Aug 29, 2023

• PR feedback (more to come)

  robin-aws

  committed
  85f9db2

• Merge duplicated code into AddMethodOverrideFrameSubsetChk

  robin-aws

  committed
  71b0a2f

• More feedback (especially fixing {:concurrent} w.r.t. default reads!)

  robin-aws

  committed
  5993220

• Address TODO about method specs referring to the set of allocated objects

  robin-aws

  committed
  96dde55

• Mark test inconsistent with function version as expected for now

  robin-aws

  committed
  b484dae

Commits on Aug 30, 2023

• Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSubsetChk

  robin-aws

  committed
  1f8b12c

• Update expect files

  robin-aws

  committed
  79d541a

• Add “Do” to “WithDelayedReadsChecks”

  robin-aws

  committed
  f16064a

• Reorder {:concurrent} checks

  robin-aws

  committed
  e27efe4

• Merge branch 'master' of https://github.com/dafny-lang/dafny into read-clauses-on-methods

  Show description for 3cdf36e
  robin-aws

  committed
  3cdf36e

• Whitespace

  robin-aws

  committed
  0acef7f

• Fix reference manual (options and attribute section numbering)

  robin-aws

  committed
  5fcf4a3

• Merge branch 'master' of https://github.com/dafny-lang/dafny into read-clauses-on-methods

  robin-aws

  committed
  33ac004