1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7typedef unsigned long uint32_t; 8 9struct foo { 10 uint32_t words[1]; 11}; 12typedef struct foo foo_t; 13 14/** FNSPEC 15 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>" 16*/ 17unsigned f(unsigned i) 18{ 19 return (3 / i ? i+1 : i); 20} 21 22 23static inline void __attribute__((__pure__)) 24foo_ptr_new(foo_t *foo_ptr, uint32_t bar) { 25 foo_ptr->words[0] = f(0); 26 27 foo_ptr->words[0] |= bar << 0; 28} 29 30unsigned g(unsigned i) 31{ 32 return f(i) + 3; 33} 34 35struct thing { 36 int *base; 37 int size; 38}; 39typedef struct thing thing_t; 40 41int h(thing_t t) 42{ 43 for (int i = 0; i < t.size; i++) { 44 t.base[i] = 0; 45 } 46 return t.size; 47} 48 49 50