1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7int g(int); 8int f(int i) 9{ 10 if (__builtin_expect(i < 0, 0)) return g(-i); 11 else return i + 3; 12} 13 14int g(int i) 15{ 16 int acc = i < 0 ? i : 0; 17 while (acc < i) /** INV: "\<lbrace> \<acute>acc <=s \<acute>i \<rbrace>" */ { 18 acc++; 19 } 20 return acc; 21} 22