1/*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11int f(int n)
12{
13  int total = 1;
14  do {
15    total = total * n;
16    n--;
17  } while (n >= 0);
18  return total;
19}
20
21int g(int x, int y)
22{
23  do
24    /** INV: "\<lbrace> \<acute>x > \<acute>y \<rbrace>" */
25    x += y;
26  while (y < 100);
27  return x;
28}
29
30int h(int x)
31{
32  do
33    /** INV: "\<lbrace> \<acute>x > \<acute>y \<rbrace>" */
34    {
35      x ++;
36    }
37  while (x < 100);
38  return x;
39}
40
41