src/core/index.h


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

#ifndef _JH_CORE_INDEX_H_
#define _JH_CORE_INDEX_H_

#include "index_types.h"

#if JH_INDEX_MAX >= SIZE_MAX
#define JH_index_cannot_allocate_more(type_size, counter) \
      (\
         (((size_t) (counter)) == SIZE_MAX) \
         || ((counter) == JH_INDEX_MAX) \
         || ((((size_t) (counter)) + 1) > (SIZE_MAX / (type_size))) \
      )
#else
#define JH_index_cannot_allocate_more(type_size, counter) \
      (\
         ((counter) == JH_INDEX_MAX) \
         || ((((size_t) (counter)) + 1) > (SIZE_MAX / (type_size))) \
      )
#endif

/*
 * Returns a random JH_index.
 */
/*@
   ensures (\result <= JH_INDEX_MAX);
   assigns \result;
@*/
JH_index JH_index_random (void);

/*
 * Returns a random JH_index, included in [0, limit]
 */
/*@
   ensures (\result <= limit);
   assigns \result;
@*/
JH_index JH_index_random_up_to (const JH_index limit);

int JH_index_cmp (const JH_index a, const JH_index b);

#endif