Code

Extend pointer encoding#1277

Code

Draft

superaxander wants to merge 19 commits intodevutwente-fmt/vercors:devfrom pointer-extensionutwente-fmt/vercors:pointer-extensionCopy head branch name to clipboard

+2,480-332

Commits

Commits on Nov 12, 2024

• Implement very basic pointer-integer casts

  superaxander

  committed
  7d03daa

  Copy full SHA for 7d03daa

Commits on Nov 13, 2024

• Get rid of casts from Object and Null types as well

  superaxander

  committed
  58fc5a1

  Copy full SHA for 58fc5a1

Commits on Nov 14, 2024

• Get rid of identity casts

  superaxander

  committed
  14b322c

  Copy full SHA for 14b322c

• Keep cast helpers for identity pointer casts

  superaxander

  committed
  ea84557

  Copy full SHA for ea84557

Commits on Nov 20, 2024

• Take pointer provenance into account, implement pointer comparisons,

  Show description for b901ec8
  superaxander

  committed
  b901ec8

  Copy full SHA for b901ec8

Commits on Nov 21, 2024

• Disable provenance checks in function contracts, make casts preserve

  Show description for b6d23ba
  superaxander

  committed
  b6d23ba

  Copy full SHA for b6d23ba

• Get rid of some clutter caused by provenance checks

  superaxander

  committed
  9d48ed7

  Copy full SHA for 9d48ed7

Commits on Nov 22, 2024

• Remove unused PointerBlock node

  superaxander

  committed
  5f51b99

  Copy full SHA for 5f51b99

• Assuming/asserting seems to work

  superaxander

  committed
  1d6a5d8

  Copy full SHA for 1d6a5d8

• Add spec/tests for assuming/asserting

  superaxander

  committed
  51b0239

  Copy full SHA for 51b0239

• Finish cherry-picking Asserting/Assuming changes from Bob's branch

  superaxander

  committed
  7d8907e

  Copy full SHA for 7d8907e

• Use underlyingPath where available in SilverToCol (needs proper fix)

  superaxander

  committed
  b5e997d

  Copy full SHA for b5e997d

Commits on Nov 28, 2024

• Encode provenance with nondeterministic checks instead of asserts

  superaxander

  committed
  a213716

  Copy full SHA for a213716

• Fix compilation issues

  superaxander

  committed
  9a8e81c

  Copy full SHA for 9a8e81c

• Add specification syntax for reasoning about pointer blocks

  superaxander

  committed
  905b035

  Copy full SHA for 905b035

Commits on Dec 4, 2024

• Very basic version of bitwise operations

  superaxander

  committed
  e4fc992

  Copy full SHA for e4fc992

Commits on Dec 11, 2024

• Add tests for bit vector operations, implement signed bitvectors soundly

  superaxander

  committed
  65ac48d

  Copy full SHA for 65ac48d

• Add Asserting to SilverToCol

  superaxander

  committed
  d3cf0a6

  Copy full SHA for d3cf0a6

• Fix typo's in tests and move signedness to secondary field of TCInt

  superaxander

  committed
  ba2930f

  Copy full SHA for ba2930f