blob: 2b4a35580280880e04590b1c2c476733d320074d (
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
|
#ifndef _ZoO_CORE_CHAR_H_
#define _ZoO_CORE_CHAR_H_
#include "char_types.h"
/* Compares two words. {word_a} does not have to be null terminated. */
/*@
@ requires null_terminated_string(word_b);
@ requires ((length(word_a) * sizeof(ZoO_char)) == word_a_size);
@ ensures ((\result == 1) || (\result == 0) || (\result == -1));
@*/
int ZoO_word_cmp
(
const ZoO_char word_a [const static 1],
const size_t word_a_size,
const ZoO_char word_b [const static 1]
);
/*
* Returns the lowercase equivalent of ZoO_char that are included in ['A','Z'].
* Other ZoO_char are returned untouched.
*/
ZoO_char ZoO_char_to_lowercase (const ZoO_char c);
/*
* Returns '1' iff {c} should be considered as an punctuation character, '0'
* otherwise.
*/
/*@
@ ensures ((\result == 1) || (\result == 0));
@*/
int ZoO_char_is_punctuation (const ZoO_char c);
/*
* Returns '1' iff containing {c} means the word should not be learned. '0'
* otherwise.
*/
/*@
@ ensures ((\result == 1) || (\result == 0));
@*/
int ZoO_word_char_is_banned (const ZoO_char c);
#endif
|
