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