| 28bf4b0b |
1 | /* |
| 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
| 3 | ** See ../LICENSE for license information. |
| 4 | */ |
| 5 | /* |
| 6 | ** valueTable.h |
| 7 | */ |
| 8 | |
| 9 | /* |
| 10 | ** valueTable is a table of stateValue's. |
| 11 | ** Based on genericTable |
| 12 | */ |
| 13 | |
| 14 | # ifndef VTABLE_H |
| 15 | # define VTABLE_H |
| 16 | |
| 17 | /*@constant null valueTable valueTable_undefined; @*/ |
| 18 | # define valueTable_undefined genericTable_undefined |
| 19 | |
| 0e41eb0e |
20 | extern /*@falsewhennull@*/ bool valueTable_isDefined(valueTable) /*@*/ ; |
| 28bf4b0b |
21 | # define valueTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) |
| 22 | |
| 0e41eb0e |
23 | extern /*@nullwhentrue@*/ bool valueTable_isUndefined(valueTable) /*@*/ ; |
| 28bf4b0b |
24 | # define valueTable_isUndefined(p_h) (genericTable_isUndefined ((genericTable) (p_h))) |
| 25 | |
| 26 | extern /*@only@*/ valueTable valueTable_create(int p_size); |
| 27 | # define valueTable_create(p_s) ((valueTable) genericTable_create (p_s)) |
| 28 | |
| 29 | extern void valueTable_insert (valueTable p_h, |
| 30 | /*@only@*/ cstring p_key, |
| 31 | /*@only@*/ stateValue p_value); |
| 32 | |
| 33 | /*@access stateValue@*/ |
| 34 | extern /*@null@*/ /*@dependent@*/ /*@exposed@*/ stateValue |
| 35 | valueTable_lookup (valueTable p_h, cstring p_key) /*@*/ ; |
| 36 | # define valueTable_lookup(p_h,p_key) \ |
| 37 | ((stateValue) genericTable_lookup ((genericTable) (p_h), p_key)) |
| 38 | /*@noaccess stateValue@*/ |
| 39 | |
| 2c88d156 |
40 | extern bool valueTable_contains (valueTable p_h, cstring p_key) /*@*/ ; |
| 41 | # define valueTable_contains(p_h,p_key) \ |
| 42 | (stateValue_isDefined (valueTable_lookup (p_h, p_key))) |
| 43 | |
| 28bf4b0b |
44 | extern /*@unused@*/ /*@only@*/ cstring valueTable_stats(valueTable p_h); |
| 45 | # define valueTable_stats(p_h) genericTable_stats ((genericTable) (p_h)) |
| 46 | |
| 47 | extern void valueTable_free (/*@only@*/ valueTable p_h); |
| 48 | # define valueTable_free(p_h) (genericTable_free ((genericTable) (p_h))) |
| 49 | |
| 50 | extern /*@only@*/ cstring valueTable_unparse (valueTable p_h) /*@*/ ; |
| 51 | |
| 52 | extern void valueTable_update (valueTable p_h, cstring p_key, /*@owned@*/ stateValue p_newval) /*@modifies p_h@*/ ; |
| 53 | |
| 54 | extern /*@only@*/ valueTable valueTable_copy (valueTable p_s) ; |
| 55 | |
| 56 | /*@iter valueTable_elements (sef valueTable p_g, yield exposed cstring m_key, yield exposed stateValue m_el)@*/ |
| 57 | |
| 393e573f |
58 | # define valueTable_elements(p_g, m_key, m_el) genericTable_elements (p_g, m_key, m_el) |
| 59 | # define end_valueTable_elements end_genericTable_elements |
| 28bf4b0b |
60 | |
| 61 | extern int valueTable_size (valueTable p_h) /*@*/ ; |
| 62 | # define valueTable_size(p_h) (genericTable_size(p_h)) |
| 63 | |
| 64 | |
| 65 | # else |
| 66 | # error "Multiple include" |
| 67 | # endif |
| 68 | |
| 69 | |
| 70 | |
| 71 | |
andersk / splint.git / blame