]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
2 | ** filelocList.h (from slist_templace.h) | |
3 | */ | |
4 | ||
5 | # ifndef filelocLIST_H | |
6 | # define filelocLIST_H | |
7 | ||
28bf4b0b | 8 | abst_typedef /*@null@*/ struct |
885824d3 | 9 | { |
10 | int nelements; | |
11 | int free; | |
12 | /*@reldef@*/ /*@relnull@*/ o_fileloc *elements; | |
13 | } *filelocList ; | |
14 | ||
0e41eb0e | 15 | extern /*@unused@*/ /*@nullwhentrue@*/ bool |
885824d3 | 16 | filelocList_isUndefined (filelocList p_f) /*@*/ ; |
0e41eb0e | 17 | extern /*@falsewhennull@*/ bool filelocList_isDefined (filelocList p_f); |
885824d3 | 18 | |
19 | /*@constant null filelocList filelocList_undefined; @*/ | |
20 | # define filelocList_undefined (NULL) | |
21 | # define filelocList_isDefined(f) ((f) != filelocList_undefined) | |
22 | # define filelocList_isUndefined(f) ((f) == filelocList_undefined) | |
23 | ||
24 | /*@iter filelocList_elements (sef filelocList x, yield exposed fileloc el); @*/ | |
25 | # define filelocList_elements(x, m_el) \ | |
26 | { if (filelocList_isDefined (x)) { \ | |
27 | int m_ind; fileloc *m_elements = &((x)->elements[0]); \ | |
28 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
29 | { fileloc m_el = *(m_elements++); | |
30 | ||
31 | # define end_filelocList_elements }}} | |
32 | ||
33 | extern int filelocList_realSize (filelocList p_s) /*@*/ ; | |
34 | ||
35 | extern int filelocList_size (/*@sef@*/ filelocList p_s) /*@*/ ; | |
36 | # define filelocList_size(s) (filelocList_isDefined (s) ? (s)->nelements : 0) | |
37 | ||
38 | extern bool filelocList_isEmpty (/*@sef@*/ filelocList p_s); | |
39 | # define filelocList_isEmpty(s) (filelocList_size(s) == 0) | |
40 | ||
41 | extern filelocList | |
42 | filelocList_append (/*@returned@*/ filelocList p_s, /*@only@*/ filelocList p_t); | |
efd360a3 | 43 | |
885824d3 | 44 | extern /*@only@*/ filelocList filelocList_new (void) /*@*/ ; |
45 | extern filelocList | |
46 | filelocList_add (/*@returned@*/ filelocList p_s, /*@only@*/ fileloc p_el) | |
47 | /*@modifies p_s@*/ ; | |
48 | ||
49 | extern filelocList | |
50 | filelocList_addDifferentFile (/*@returned@*/ filelocList p_s, | |
51 | fileloc p_where, fileloc p_loc) | |
52 | /*@modifies p_s@*/ ; | |
53 | ||
54 | extern filelocList filelocList_addUndefined (/*@returned@*/ filelocList p_s) | |
55 | /*@modifies p_s@*/ ; | |
56 | ||
57 | extern /*@only@*/ cstring filelocList_unparseUses (filelocList p_s); | |
58 | extern /*@unused@*/ /*@only@*/ cstring filelocList_unparse (filelocList p_s) ; | |
59 | extern void filelocList_free (/*@only@*/ filelocList p_s) ; | |
60 | ||
61 | /*@constant int filelocListBASESIZE;@*/ | |
62 | # define filelocListBASESIZE MIDBASESIZE | |
63 | ||
64 | # endif | |
65 | ||
66 | ||
67 | ||
68 |