]>
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 | ** stateValue.h | |
7 | */ | |
8 | ||
9 | # ifndef STATEVALUE_H | |
10 | # define STATEVALUE_H | |
11 | ||
12 | /* | |
13 | ** Keeps track of the value of a state variable, as well as tracking | |
14 | ** information about its history. | |
15 | */ | |
16 | ||
17 | struct s_stateValue | |
18 | { | |
19 | int value; | |
2c88d156 | 20 | bool implicit; |
28bf4b0b | 21 | /*@only@*/ stateInfo info; |
22 | }; | |
23 | ||
2c88d156 | 24 | extern /*@notnull@*/ stateValue stateValue_create (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ; |
25 | extern /*@notnull@*/ stateValue stateValue_createImplicit (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ; | |
28bf4b0b | 26 | |
27 | /*@constant null stateValue stateValue_undefined@*/ | |
28 | # define stateValue_undefined (NULL) | |
29 | ||
30 | extern /*@truenull@*/ bool stateValue_isUndefined (stateValue) /*@*/ ; | |
31 | # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined) | |
32 | ||
33 | extern /*@falsenull@*/ bool stateValue_isDefined (stateValue) /*@*/ ; | |
34 | # define stateValue_isDefined(p_s) ((p_s) != NULL) | |
35 | ||
2c88d156 | 36 | extern bool stateValue_isImplicit (stateValue) /*@*/ ; |
37 | ||
28bf4b0b | 38 | extern int stateValue_getValue (stateValue p_s) /*@*/ ; |
39 | ||
40 | extern void stateValue_update (stateValue p_res, stateValue p_val) /*@modifies p_res@*/ ; | |
41 | ||
42 | extern /*@observer@*/ fileloc stateValue_getLoc (stateValue p_s) /*@*/ ; | |
43 | # define stateValue_getLoc(p_s) (stateInfo_getLoc (stateValue_getInfo (p_s))) | |
44 | ||
45 | extern bool stateValue_hasLoc (stateValue p_s) /*@*/ ; | |
46 | ||
47 | extern /*@observer@*/ stateInfo stateValue_getInfo (stateValue p_s) /*@*/ ; | |
48 | ||
49 | extern void stateValue_updateValue (/*@sef@*/ stateValue p_s, int p_value, /*@only@*/ stateInfo p_info) /*@modifies p_s@*/ ; | |
50 | ||
51 | extern void stateValue_updateValueLoc (stateValue p_s, int p_value, fileloc p_loc) /*@modifies p_s@*/ ; | |
52 | ||
53 | extern void stateValue_show (stateValue p_s, metaStateInfo p_msinfo) ; | |
54 | ||
55 | extern stateValue stateValue_copy (stateValue p_s) /*@*/ ; | |
56 | ||
2c88d156 | 57 | extern /*@only@*/ cstring |
28bf4b0b | 58 | stateValue_unparseValue (stateValue p_s, metaStateInfo p_msinfo) /*@*/ ; |
59 | ||
60 | extern cstring stateValue_unparse (stateValue p_s) /*@*/ ; | |
61 | ||
62 | extern bool stateValue_sameValue (stateValue p_s1, stateValue p_s2) /*@*/ ; | |
63 | ||
ccf0a4a8 | 64 | extern bool stateValue_isError (/*@sef@*/ stateValue p_s) /*@*/ ; |
65 | # define stateValue_isError(p_s) (stateValue_isDefined (p_s) && (stateValue_getValue (p_s) == stateValue_error)) | |
28bf4b0b | 66 | |
67 | /*@constant int stateValue_error@*/ | |
68 | # define stateValue_error -1 | |
69 | ||
70 | # else | |
71 | # error "Multiple include" | |
72 | # endif |