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
11/* also tests
12   - post-increment and decrement (which are common in for loops)
13   - arrays on the heap and stack (treated differently in VCG-land)
14*/
15
16int *f(int *i, int c)
17{
18  unsigned j;
19  for (j = 0; j < 4; j++) i[j] = i[j] + c;
20  i[0]++;
21  return i;
22}
23
24int g(int c)
25{
26  for (unsigned int j = 10; 0 < j; j--)
27    /** INVARIANT: "\<lbrace> 0 <= \<acute>j & \<acute>j <= 10 \<rbrace>" */
28    {
29      c = c + j;
30    }
31  return c;
32}
33
34int h(int c)
35{
36  int a[10];
37  for (unsigned int j = 0; j < 10; j++) a[j] = j;
38  a[0] = a[1] + a[2];
39  return a[0];
40}
41
42int f2(int *a)
43{
44  int j, res;
45  for (j=0,res=0; j < 32; j += 4) { res += a[j]; }
46  return res;
47}
48