Code

Turn into passive cmd splitup#746

Code

Draft

keyboardDrummer wants to merge 29 commits intoboogie-org:masterboogie-org/boogie:masterfrom keyboardDrummer:TurnIntoPassiveCmdSplitupkeyboardDrummer/boogie:TurnIntoPassiveCmdSplitupCopy head branch name to clipboard

+674-464

Commits

Commits on May 31, 2023

• Recognize {:id ...} attributes on assignments

  Show description for 49d5d23
  atomb

  committed
  49d5d23

  Copy full SHA for 49d5d23

• Recognize {:id ...} on requires clauses

  Show description for 0ac0824
  atomb

  committed
  0ac0824

  Copy full SHA for 0ac0824

• Recognize {:id ...} on loop invariants

  Show description for 32398ee
  atomb

  committed
  32398ee

  Copy full SHA for 32398ee

• Add a field to VCResult to track unsat cores

  atomb

  committed
  5c4afaf

  Copy full SHA for 5c4afaf

• Basic support for labeled assertions

  atomb

  committed
  e945230

  Copy full SHA for e945230

• Fix concurrency bug accidentally discovered

  atomb

  committed
  ac56302

  Copy full SHA for ac56302

Commits on Jun 1, 2023

• Mostly complete verification coverage tracking

  atomb

  committed
  a97032b

  Copy full SHA for a97032b

• Add initial test for verification coverage

  atomb

  committed
  5919289

  Copy full SHA for 5919289

• Tweak RUN commands for verification coverage test

  atomb

  committed
  8ad7c16

  Copy full SHA for 8ad7c16

• Verification coverage unsupported in batch mode

  atomb

  committed
  e95aab5

  Copy full SHA for e95aab5

• Attempt to make timeouts test more robust

  atomb

  committed
  3ce4244

  Copy full SHA for 3ce4244

• Another try for more deterministic timeout testing

  atomb

  committed
  950080b

  Copy full SHA for 950080b

• Tiny tweaks to coverage tests

  atomb

  committed
  7b6679b

  Copy full SHA for 7b6679b

• Merge remote-tracking branch 'upstream/master' into broader-unsat-cores

  atomb

  committed
  b67d227

  Copy full SHA for b67d227

Commits on Jun 2, 2023

• Rename variables

  atomb

  committed
  20e06a0

  Copy full SHA for 20e06a0

• Adjust how IDs (and other attributes) are tracked

  atomb

  committed
  abcae74

  Copy full SHA for abcae74

• Remove /printNecessaryAssumes option

  Show description for 6b48078
  atomb

  committed
  6b48078

  Copy full SHA for 6b48078

• Typo in comment

  atomb

  committed
  d1861c0

  Copy full SHA for d1861c0

• Documentation for /printVerificationCoverage, :id

  atomb

  committed
  a07fe28

  Copy full SHA for a07fe28

• Remove conditionals on magic variable prefixes

  atomb

  committed
  82e7e24

  Copy full SHA for 82e7e24

• Copy :id attributes unconditionally

  atomb

  committed
  98dcf9f

  Copy full SHA for 98dcf9f

Commits on Jun 5, 2023

• Rename variable for id on CallCmds

  atomb

  committed
  d68b1f9

  Copy full SHA for d68b1f9

• Add comment about dummy operators

  atomb

  committed
  6d48d32

  Copy full SHA for 6d48d32

• PrintVerificationCoverage -> TrackVerificationCoverage

  atomb

  committed
  e43e4f2

  Copy full SHA for e43e4f2

• CurrentCoveredElements -> ProofRun.CoveredElements

  atomb

  committed
  94cf1ea

  Copy full SHA for 94cf1ea

• Rename command variables in VCGen for loops

  atomb

  committed
  449364c

  Copy full SHA for 449364c

• Update verification coverage test

  Show description for 725fe2d
  atomb

  committed
  725fe2d

  Copy full SHA for 725fe2d

• Remove uses of /printVerificationCoverage

  atomb

  committed
  cd50eef

  Copy full SHA for cd50eef

• Extract outer methods from turnIntoPassiveCmd

  keyboardDrummer

  committed
  20eace9

  Copy full SHA for 20eace9