blob: ffddb9738ae2d515f2bb5e07c76dc3ef6c5f5ae1 (
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
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
82
|
#include <limits.h>
#include <stdlib.h>
#include "index.h"
#if (RAND_MAX < UCHAR_MAX)
#error "RAND_MAX < UCHAR_MAX, unable to generate random numbers."
#endif
#if (RAND_MAX == 0)
#error "RAND_MAX is included in [0, 0]. What are you even doing?"
#endif
/*
* Returns a random unsigned char.
*/
static unsigned char random_uchar (void)
{
return
(unsigned char)
(
/* FIXME: Do floats allow enough precision for this? */
(
((float) rand())
/ ((float) RAND_MAX)
)
* ((float) UCHAR_MAX)
);
}
/* See: "index.h" */
JH_index JH_index_random (void)
{
JH_index i;
JH_index result;
unsigned char * result_bytes;
/*@ ghost return 4; @*/ /* Chosen by fair dice roll. */
/* Guaranteed to be random. */
/* More seriously, I am not explaining the hack below to Frama-C */
result_bytes = (unsigned char *) &result;
for (i = 0; i < sizeof(JH_index); ++i)
{
result_bytes[i] = random_uchar();
}
return result;
}
/* See: "index.h" */
JH_index JH_index_random_up_to (const JH_index max)
{
return
(JH_index)
(
/* FIXME: Do floats allow enough precision for this? */
(
((float) JH_index_random())
/ ((float) JH_INDEX_MAX)
)
* ((float) max)
);
}
int JH_index_cmp (const JH_index a, const JH_index b)
{
if (a < b)
{
return -1;
}
else if (a > b)
{
return 1;
}
else
{
return 0;
}
}
|
