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