Code

Booster 2#508

Code

Draft

virgil-serbanuta wants to merge 16 commits intomasterruntimeverification/wasm-semantics:masterfrom booster-2runtimeverification/wasm-semantics:booster-2Copy head branch name to clipboard

+1,190-124

Commits

Commits on Sep 26, 2023

• Rule labels

  virgil-serbanuta

  committed
  06fcd6a

  Copy full SHA for 06fcd6a

• Mark some functions as total

  virgil-serbanuta

  committed
  f56b93e

  Copy full SHA for f56b93e

• Definedness for #signed

  virgil-serbanuta

  committed
  14237e7

  Copy full SHA for 14237e7

• Add an Int-to-Int map

  virgil-serbanuta

  committed
  cbeb81f

  Copy full SHA for cbeb81f

• Use an Int-to-Int map for <memAddrs>

  virgil-serbanuta

  committed
  ac2d70a

  Copy full SHA for ac2d70a

• Int-to-Int map for <funcAddrs>

  virgil-serbanuta

  committed
  fc028a8

  Copy full SHA for fc028a8

• Make intBinOp total

  virgil-serbanuta

  committed
  78f41eb

  Copy full SHA for 78f41eb

• Make intRelOp total

  virgil-serbanuta

  committed
  34f84b3

  Copy full SHA for 34f84b3

• Update <locals> without map unification.

  virgil-serbanuta

  committed
  d4047f8

  Copy full SHA for d4047f8

• Use lookup for <funcAddrs> in #call instead of map unification.

  virgil-serbanuta

  committed
  038e66b

  Copy full SHA for 038e66b

• Split store evaluation to use one map unification per rewrite

  virgil-serbanuta

  committed
  6d3ca0d

  Copy full SHA for 6d3ca0d

• Split load evaluation to use one map unification per rewrite

  virgil-serbanuta

  committed
  515b11c

  Copy full SHA for 515b11c

Commits on Sep 27, 2023

• Fix KBuild file

  virgil-serbanuta

  committed
  5ea9462

  Copy full SHA for 5ea9462

• Remove concrete signedTotal

  virgil-serbanuta

  committed
  e11cfaf

  Copy full SHA for e11cfaf

• Map int to val for <locals>

  virgil-serbanuta

  committed
  0fe0b76

  Copy full SHA for 0fe0b76

• tmp

  virgil-serbanuta

  committed
  b1fa1e6

  Copy full SHA for b1fa1e6