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