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
11/* this file is no longer valid syntax; the pre-post should be
12   replaced by an appropriate FNCALL specification, before the
13   function */
14
15int fact(int n)
16     /** PRE: n > 0
17         POST: fact_ret = FACT n */
18{
19  int c, result;
20  c = n;
21  result = 1;
22  while (c > 1) {
23    result = result * c;
24    c = c - 1;
25  }
26  return result;
27}
28