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 g(int); 12int f(int i) 13{ 14 if (__builtin_expect(i < 0, 0)) return g(-i); 15 else return i + 3; 16} 17 18int g(int i) 19{ 20 int acc = i < 0 ? i : 0; 21 while (acc < i) /** INV: "\<lbrace> \<acute>acc <=s \<acute>i \<rbrace>" */ { 22 acc++; 23 } 24 return acc; 25} 26