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