-
Notifications
You must be signed in to change notification settings - Fork 105
/
factorial.c
81 lines (63 loc) · 2.09 KB
/
factorial.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
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/** FNSPEC alloc_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> ((\<lambda>p s. if k > 0 then (\<turnstile>\<^sub>s p \<and>\<^sup>* \<turnstile>\<^sub>s (p +\<^sub>p 1) \<and>\<^sup>*
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned_long)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned long *alloc(void)
{
/* Stub */
}
/** FNSPEC free_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (sep_cut' (ptr_val \<acute>p) (2 * size_of TYPE(machine_word)) \<and>\<^sup>* free_pool k)\<^bsup>sep\<^esup> \<rbrace>
PROC free(\<acute>p)
\<lbrace> (free_pool (k + 1))\<^bsup>sep\<^esup> \<rbrace>"
*/
void free(unsigned long *p)
{
/* Stub */
}
/** FNSPEC factorial_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned_long :== PROC factorial(\<acute>n)
\<lbrace> if \<acute>ret__ptr_to_unsigned_long \<noteq> NULL then (sep_fac_list \<^bsup>\<sigma>\<^esup>n \<acute>ret__ptr_to_unsigned_long \<and>\<^sup>*
free_pool (k - (unat \<^bsup>\<sigma>\<^esup>n + 1)))\<^bsup>sep\<^esup> \<and> (unat \<^bsup>\<sigma>\<^esup>n + 1) \<le> k else (free_pool k)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned long *factorial(unsigned long n)
{
unsigned long *p, *q;
if (n == 0) {
p = alloc();
if (!p)
return 0;
*p = 1;
*(p + 1) = 0;
return p;
}
q = factorial(n - 1);
if (!q)
return 0;
p = alloc();
if (!p) {
while (q)
/** INV: "\<lbrace> \<exists>xs. (sep_list xs \<acute>q \<and>\<^sup>* free_pool (k - length xs))\<^bsup>sep\<^esup> \<and>
length xs \<le> k \<rbrace>" */
{
unsigned long *k = (unsigned long *)*(q + 1);
free(q);
q = k;
}
return 0;
}
*p = n * *q;
*(p + 1) = (unsigned long)q;
return p;
}