]>
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 | ** annotationInfo.h | |
7 | ** | |
8 | ** A record that keeps information on a user-defined annotations including: | |
9 | ** | |
10 | */ | |
11 | ||
12 | # ifndef ANNOTINFO_H | |
13 | # define ANNOTINFO_H | |
14 | ||
15 | struct s_annotationInfo { | |
16 | cstring name; | |
17 | /*@dependent@*/ /*@observer@*/ metaStateInfo state; | |
18 | /* associated metaStateInfo entry */ | |
19 | fileloc loc; | |
20 | int value; | |
21 | mtContextNode context; | |
22 | } ; | |
23 | ||
24 | /* typedef struct _annotationInfo *annotationInfo; */ | |
25 | ||
26 | /*@constant null annotationInfo annotationInfo_undefined; @*/ | |
27 | # define annotationInfo_undefined ((annotationInfo) NULL) | |
28 | ||
0e41eb0e | 29 | extern /*@falsewhennull@*/ bool annotationInfo_isDefined (annotationInfo) /*@*/ ; |
28bf4b0b | 30 | # define annotationInfo_isDefined(p_info) ((p_info) != annotationInfo_undefined) |
31 | ||
0e41eb0e | 32 | extern /*@nullwhentrue@*/ bool annotationInfo_isUndefined (annotationInfo) /*@*/ ; |
28bf4b0b | 33 | # define annotationInfo_isUndefined(p_info) ((p_info) == annotationInfo_undefined) |
34 | ||
35 | extern bool annotationInfo_equal (annotationInfo, annotationInfo) /*@*/ ; | |
36 | # define annotationInfo_equal(p_info1, p_info2) ((p_info1) == (p_info2)) | |
37 | ||
38 | extern bool annotationInfo_matchesContext (annotationInfo, uentry) /*@*/ ; | |
39 | extern bool annotationInfo_matchesContextRef (annotationInfo, sRef) /*@*/ ; | |
40 | ||
41 | extern /*@observer@*/ metaStateInfo annotationInfo_getState (annotationInfo) /*@*/ ; | |
42 | extern int annotationInfo_getValue (annotationInfo) /*@*/ ; | |
43 | extern /*@observer@*/ cstring annotationInfo_getName (annotationInfo) /*@*/ ; | |
44 | ||
45 | extern /*@only@*/ annotationInfo | |
46 | annotationInfo_create (/*@only@*/ cstring p_name, | |
47 | /*@dependent@*/ /*@exposed@*/ metaStateInfo p_state, | |
48 | /*@only@*/ mtContextNode p_context, | |
49 | int p_value, /*@only@*/ fileloc p_loc) /*@*/ ; | |
50 | ||
53306cab | 51 | extern /*@observer@*/ cstring annotationInfo_unparse (annotationInfo p_a); |
52 | extern /*@observer@*/ fileloc annotationInfo_getLoc (annotationInfo p_a) /*@*/ ; | |
28bf4b0b | 53 | |
54 | extern void annotationInfo_free (/*@only@*/ annotationInfo) ; | |
55 | ||
56 | extern /*@observer@*/ cstring annotationInfo_dump (annotationInfo) ; | |
57 | extern /*@observer@*/ annotationInfo annotationInfo_undump (char **p_s) /*@modifies *p_s@*/ ; | |
58 | ||
b7e84605 | 59 | extern void annotationInfo_showContextRefError (annotationInfo, sRef) /*@*/ ; |
60 | ||
28bf4b0b | 61 | # else |
62 | # error "Multiple include" | |
63 | # endif | |
64 | ||
65 | ||
66 | ||
67 |