_Check_return_
_Ret_range_(>=, 0)
int _factorial(_In_range_(0, 12) int n, _Out_range_(>= , 0) _Deref_post_opt_valid_ int* result) {
_Pre_((n >= 0) && (n <= 15));
_Pre_valid_
_Pre_notnull_
_Pre_writable_byte_size_(sizeof(int))
if (n == 0 || n == 1) {
_Post_valid_
_Post_writable_byte_size_(sizeof(int))
*result = 1;
return 0;
}
_Post_valid_
_Post_writable_byte_size_(sizeof(int))
int _fact = 1;
for (int i = 2; i <= n; ++i) _fact *= i;
*result = _fact;
return 0;
}
