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 11typedef unsigned long uint32_t; 12 13struct foo { 14 uint32_t words[1]; 15}; 16typedef struct foo foo_t; 17 18/** FNSPEC 19 f_spec: "\<forall>i. \<Gamma> \<turnstile> \<lbrace> \<acute>i = i \<rbrace> \<acute>ret__unsigned :== PROC f(\<acute>i) \<lbrace> \<acute>ret__unsigned = i + 1 \<rbrace>" 20*/ 21unsigned f(unsigned i) 22{ 23 return (3 / i ? i+1 : i); 24} 25 26 27static inline void __attribute__((__pure__)) 28foo_ptr_new(foo_t *foo_ptr, uint32_t bar) { 29 foo_ptr->words[0] = f(0); 30 31 foo_ptr->words[0] |= bar << 0; 32} 33 34unsigned g(unsigned i) 35{ 36 return f(i) + 3; 37} 38 39struct thing { 40 int *base; 41 int size; 42}; 43typedef struct thing thing_t; 44 45int h(thing_t t) 46{ 47 for (int i = 0; i < t.size; i++) { 48 t.base[i] = 0; 49 } 50 return t.size; 51} 52 53 54