test/coq/pass/while_PM_terminating.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

default Order dec

$include <prelude.sail>

register GPR00 : int

function test b : int -> unit = {
  i : int = 0;
  while i < 64 do {
    GPR00 = b + i;
    i = i + 1;
  }
}

termination_measure test while 64 - i