blob: c9c30f131a5d113c6ff0a94dc7749d0f83332ba1 (
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
|
#include <stdlib.h>
#include <string.h>
#include "../core/index.h"
#include "sequence.h"
/* See "sequence.h" */
/*@
requires
(
\valid(sequence_a+ (0 .. sequence_a_length))
|| (sequence_a_length == 0)
);
requires
(
\valid(sequence_b+ (0 .. sequence_b_length))
|| (sequence_b_length == 0)
);
assigns \result;
@*/
int JH_sequence_cmp
(
const JH_index sequence_a [const restrict static 1],
const JH_index sequence_b [const restrict static 1],
const JH_index length
)
{
JH_index i, a, b;
for (i = 0; i < length; ++i)
{
a = sequence_a[i];
b = sequence_b[i];
if (a < b)
{
return -1;
}
else if (a > b)
{
return 1;
}
}
return 0;
}
|