]>
Commit | Line | Data |
---|---|---|
abd7f895 | 1 | /* |
c0de361f | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. |
abd7f895 | 3 | ** See ../LICENSE for license information. |
4 | ** | |
5 | */ | |
6 | /* | |
7 | ** mstring.h | |
8 | */ | |
9 | ||
10 | # ifndef MSTRING_H | |
11 | # define MSTRING_H | |
12 | ||
13 | /* mstring is a non-abstract string (char *) */ | |
14 | ||
15 | typedef /*@concrete@*/ char *mstring; | |
16 | typedef /*@observer@*/ char *ob_mstring; | |
17 | typedef /*@observer@*/ /*@null@*/ char *bn_mstring; | |
18 | ||
19 | extern /*@unused@*/ /*@notnull@*/ /*@observer@*/ char * | |
20 | mstring_safePrint (/*@returned@*/ /*@null@*/ mstring p_s) /*@*/ ; | |
21 | extern char *mstring_spaces (int p_n) /*@*/ ; | |
22 | extern char *mstring_concat (const char *p_s1, const char *p_s2) /*@*/ ; | |
23 | extern char *mstring_concatFree (/*@only@*/ char *p_s1, /*@only@*/ char *p_s2) /*@modifies *p_s1, *p_s2*/ ; | |
24 | extern char *mstring_concatFree1 (/*@only@*/ char *p_s1, const char *p_s2); | |
25 | extern char *mstring_append (/*@only@*/ char *p_s1, char p_c); | |
26 | extern char *mstring_copy (/*@null@*/ char *p_s1) /*@*/ /*@ensures maxRead(result) == maxRead(p_s1) /\ maxSet(result) == maxSet(p_s1) @*/ ; | |
27 | extern bool mstring_equalPrefix (const char *p_c1, const char *p_c2) /*@*/ ; | |
28 | extern bool mstring_equal (/*@null@*/ const char *p_s1, /*@null@*/ const char *p_s2) /*@*/ ; | |
29 | extern bool mstring_containsChar (/*@unique@*/ const char *p_s, char p_c) /*@*/ ; | |
30 | extern bool mstring_containsString (/*@unique@*/ const char *p_s, /*@unique@*/ const char *p_c) /*@*/ ; | |
31 | ||
32 | extern size_t mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; | |
33 | # define mstring_length(s) \ | |
34 | (((s) != NULL) ? strlen (s) : 0) | |
35 | ||
36 | extern /*@falsewhennull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; | |
37 | # define mstring_isDefined(s) ((s) != NULL) | |
38 | ||
39 | extern /*@nullwhentrue@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; | |
40 | # define mstring_isEmpty(s) (mstring_length(s) == 0) | |
41 | ||
42 | extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ; | |
43 | ||
44 | extern /*@notnull@*/ /*@only@*/ char *mstring_create (size_t p_n) | |
45 | /*@*/ | |
46 | /*@ensures maxSet(result) == p_n /\ maxRead(result) == 0 @*/ ; | |
47 | ||
48 | extern /*@notnull@*/ /*@only@*/ char *mstring_createEmpty (void) /*@*/ ; | |
49 | ||
50 | extern void mstring_free (/*@out@*/ /*@only@*/ /*@null@*/ char *p_s); | |
51 | # define mstring_free(s) sfree(s) | |
52 | ||
53 | # define mstring_createEmpty() mstring_create(0) | |
54 | ||
55 | # else | |
56 | # error "Multiple include" | |
57 | # endif | |
58 | ||
59 | ||
60 | ||
61 | ||
62 |