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
11unsigned global;
12
13int mult(int x, int y)
14{
15  return x * y;
16}
17
18int fact(int n)
19{
20  int factor, total;
21  total = 1;
22  factor = 2;
23  while (factor <= n)
24    /** INV: "\<lbrace> unat \<acute>total = fac (unat \<acute>factor - 1) &
25                       \<acute>factor \<le> \<acute>n + 1
26              \<rbrace>" */
27    {
28      total = mult(factor, total);
29      factor = factor + 1;
30    }
31  return total;
32}
33
34/** FNSPEC
35  g_modifies: "\<forall> \<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC g() {t. t may_not_modify_globals \<sigma>}"
36*/
37int g(void)
38{
39  return 257;
40}
41
42/** FNSPEC
43  f_spec: "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== PROC f(n) \<lbrace> \<acute>ret__int = 1 \<rbrace>"
44  f_modifies: "\<forall>\<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC f(\<acute>n)
45                       {t. t may_not_modify_globals \<sigma>}"
46*/
47int f (int n)
48{
49  char c;
50  global++;
51  c = g();
52  return c;
53}
54
55
56/** FNSPEC
57  h_modifies:
58    "\<forall> \<sigma>.
59       \<Gamma> \<turnstile>
60          {\<sigma>}
61            \<acute>ret__ptr_to_void :== PROC h()
62          {t. t may_not_modify_globals \<sigma>}"
63*/
64void *h(void)
65{
66  return 0;
67}
68
69/** FNSPEC
70  i_modifies: "\<forall> \<sigma>. \<Gamma> \<turnstile> {\<sigma>} \<acute>ret__int :== PROC i() {t. t may_not_modify_globals \<sigma>}"
71*/
72int i(void)
73{
74  int *iptr = h();
75  return iptr[3];
76}
77
78/** FNSPEC
79      has_bogus_spec_spec: "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== PROC has_bogus_spec() \<lbrace> \<acute>ret__int = 4 \<rbrace>"
80*/
81int has_bogus_spec(void)
82{
83  return 3;
84}
85
86int calls_bogus(void)
87{
88  return has_bogus_spec();
89}
90