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