diff options
Diffstat (limited to 'test/coq/pass/while_PM_terminating.sail')
| -rw-r--r-- | test/coq/pass/while_PM_terminating.sail | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/coq/pass/while_PM_terminating.sail b/test/coq/pass/while_PM_terminating.sail new file mode 100644 index 00000000..5129e997 --- /dev/null +++ b/test/coq/pass/while_PM_terminating.sail @@ -0,0 +1,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 |