blob: eb3c471afd655c6e0bae443252c057a35893ec04 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
#ifndef _ZoO_CORE_INDEX_H_
#define _ZoO_CORE_INDEX_H_
#include "index_types.h"
/*
* Returns a random ZoO_index.
*/
/*@
ensures (\result <= ZoO_INDEX_MAX);
assigns \result;
@*/
ZoO_index ZoO_index_random (void);
/*
* Returns a random ZoO_index, included in [0, limit]
*/
/*@
ensures (\result <= limit);
assigns \result;
@*/
ZoO_index ZoO_index_random_up_to (const ZoO_index limit);
#endif
|
