move-stackless-bytecode 0.3.2

Move stackless bytecode
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

============ initial translation from Move ================

[variant baseline]
public fun Test::test($t0|_r: Test::R) {
  0: return ()
}

============ after pipeline `data_invariant_instrumentation` ================

[variant verification]
public fun Test::test($t0|_r: Test::R) {
  0: assume And(WellFormed($t0), forall $elem: select Test::R.s($t0): forall $elem: $elem: Gt(select Test::S.y($elem), 0))
  1: label L1
  2: return ()
}