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