]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /* |
c0de361f | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. |
28bf4b0b | 3 | ** See ../LICENSE for license information. |
4 | */ | |
5 | /* | |
6 | ** metaStateTable.h | |
7 | ** | |
8 | ** A global table that keeps information on the user-defined states. | |
9 | ** | |
10 | ** For each state definition, we need: | |
11 | ** | |
12 | ** o A name | |
13 | ** o State Type (what kinds of things have this state value) | |
14 | ** o Number of values, and their mnemonics | |
15 | ** o A combination table (stateCombinationTable) for how different states combine as l/rvalues | |
16 | ** o Annotations (and map between annotation and value) | |
17 | ** o Context information (where can annotations be used) | |
18 | */ | |
19 | ||
20 | # ifndef MSTABLE_H | |
21 | # define MSTABLE_H | |
22 | ||
23 | /*@constant null metaStateTable metaStateTable_undefined; @*/ | |
24 | # define metaStateTable_undefined genericTable_undefined | |
25 | ||
0e41eb0e | 26 | extern /*@falsewhennull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ; |
28bf4b0b | 27 | # define metaStateTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) |
28 | ||
0e41eb0e | 29 | extern /*@nullwhentrue@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ; |
28bf4b0b | 30 | # define metaStateTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) |
31 | ||
32 | /*@constant int DEFAULT_MSTABLE_SIZE@*/ | |
33 | # define DEFAULT_MSTABLE_SIZE 32 | |
34 | ||
35 | extern /*@only@*/ metaStateTable metaStateTable_create (void) /*@*/ ; | |
36 | # define metaStateTable_create() ((metaStateTable) genericTable_create (DEFAULT_MSTABLE_SIZE)) | |
37 | ||
38 | extern void metaStateTable_insert (metaStateTable p_h, | |
39 | /*@only@*/ cstring p_key, | |
40 | /*@only@*/ metaStateInfo p_metaState) | |
41 | /*@modifies p_h@*/ ; | |
42 | ||
43 | extern /*@null@*/ /*@dependent@*/ /*@exposed@*/ metaStateInfo | |
44 | metaStateTable_lookup (metaStateTable p_h, cstring p_key) /*@*/ ; | |
45 | ||
393e573f | 46 | /*@access metaStateInfo@*/ |
28bf4b0b | 47 | # define metaStateTable_lookup(p_h,p_key) \ |
393e573f | 48 | ((metaStateInfo) genericTable_lookup ((genericTable) (p_h), p_key)) |
49 | /*@noaccess metaStateInfo@*/ | |
28bf4b0b | 50 | |
51 | extern bool metaStateTable_contains (metaStateTable p_h, cstring p_key) /*@*/ ; | |
52 | # define metaStateTable_contains(p_h,p_key) \ | |
53 | (genericTable_contains ((genericTable) (p_h), p_key)) | |
54 | ||
55 | extern /*@unused@*/ /*@only@*/ cstring metaStateTable_stats(metaStateTable p_h); | |
56 | # define metaStateTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) | |
57 | ||
58 | extern void metaStateTable_free (/*@only@*/ metaStateTable p_h); | |
59 | # define metaStateTable_free(p_h) (genericTable_free ((genericTable) (p_h))) | |
60 | ||
61 | /*@iter metaStateTable_elements (sef metaStateTable p_g, yield exposed cstring m_key, yield exposed metaStateInfo m_el)@*/ | |
62 | ||
63 | /*@access genericTable@*/ | |
64 | # define metaStateTable_elements(p_g, m_key, m_el) \ | |
65 | { int m_ind; if (metaStateTable_isDefined (p_g)) \ | |
66 | { for (m_ind = 0 ; m_ind < (p_g)->size; m_ind++) \ | |
67 | { ghbucket m_hb; m_hb = (p_g)->buckets[m_ind]; \ | |
68 | if (m_hb != NULL) { \ | |
69 | int m_j; \ | |
70 | for (m_j = 0; m_j < (m_hb)->size; m_j++) { \ | |
71 | cstring m_key; metaStateInfo m_el; m_key = (m_hb)->entries[m_j]->key; \ | |
72 | /*@access metaStateInfo@*/ \ | |
73 | m_el = (metaStateInfo) ((m_hb)->entries[m_j]->val); \ | |
74 | /*@noaccess metaStateInfo@*/ | |
75 | # define end_metaStateTable_elements }}}}} | |
76 | /*@noaccess genericTable@*/ | |
77 | ||
78 | extern cstring metaStateTable_unparse (metaStateTable p_h) ; | |
79 | ||
80 | extern int metaStateTable_size (metaStateTable p_h); | |
81 | # define metaStateTable_size(p_h) (genericTable_size(p_h)) | |
82 | ||
83 | # else | |
84 | # error "Multiple include" | |
85 | # endif | |
86 | ||
87 | ||
88 | ||
89 |