]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /* |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. | |
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 | ||
26 | extern /*@falsenull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ; | |
27 | # define metaStateTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) | |
28 | ||
29 | extern /*@truenull@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ; | |
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 | ||
46 | # define metaStateTable_lookup(p_h,p_key) \ | |
47 | (/*@i523@*/ /*@access metaStateInfo@*/ (metaStateInfo) genericTable_lookup ((genericTable) (p_h), p_key) /*@noaccess metaStateInfo@*/) | |
48 | ||
49 | extern bool metaStateTable_contains (metaStateTable p_h, cstring p_key) /*@*/ ; | |
50 | # define metaStateTable_contains(p_h,p_key) \ | |
51 | (genericTable_contains ((genericTable) (p_h), p_key)) | |
52 | ||
53 | extern /*@unused@*/ /*@only@*/ cstring metaStateTable_stats(metaStateTable p_h); | |
54 | # define metaStateTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) | |
55 | ||
56 | extern void metaStateTable_free (/*@only@*/ metaStateTable p_h); | |
57 | # define metaStateTable_free(p_h) (genericTable_free ((genericTable) (p_h))) | |
58 | ||
59 | /*@iter metaStateTable_elements (sef metaStateTable p_g, yield exposed cstring m_key, yield exposed metaStateInfo m_el)@*/ | |
60 | ||
61 | /*@access genericTable@*/ | |
62 | # define metaStateTable_elements(p_g, m_key, m_el) \ | |
63 | { int m_ind; if (metaStateTable_isDefined (p_g)) \ | |
64 | { for (m_ind = 0 ; m_ind < (p_g)->size; m_ind++) \ | |
65 | { ghbucket m_hb; m_hb = (p_g)->buckets[m_ind]; \ | |
66 | if (m_hb != NULL) { \ | |
67 | int m_j; \ | |
68 | for (m_j = 0; m_j < (m_hb)->size; m_j++) { \ | |
69 | cstring m_key; metaStateInfo m_el; m_key = (m_hb)->entries[m_j]->key; \ | |
70 | /*@access metaStateInfo@*/ \ | |
71 | m_el = (metaStateInfo) ((m_hb)->entries[m_j]->val); \ | |
72 | /*@noaccess metaStateInfo@*/ | |
73 | # define end_metaStateTable_elements }}}}} | |
74 | /*@noaccess genericTable@*/ | |
75 | ||
76 | extern cstring metaStateTable_unparse (metaStateTable p_h) ; | |
77 | ||
78 | extern int metaStateTable_size (metaStateTable p_h); | |
79 | # define metaStateTable_size(p_h) (genericTable_size(p_h)) | |
80 | ||
81 | # else | |
82 | # error "Multiple include" | |
83 | # endif | |
84 | ||
85 | ||
86 | ||
87 |