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