]>
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 | /* | |
7 | ** mtDeclarationPiece.h | |
8 | */ | |
9 | ||
10 | # ifndef MTDECLARATIONPIECE_H | |
11 | # define MTDECLARATIONPIECE_H | |
12 | ||
13 | /*@private@*/ typedef enum { | |
14 | MTP_DEAD, | |
15 | MTP_CONTEXT, MTP_VALUES, MTP_DEFAULTS, MTP_DEFAULTVALUE, | |
16 | MTP_ANNOTATIONS, MTP_MERGE, | |
17 | MTP_TRANSFERS, MTP_PRECONDITIONS, MTP_POSTCONDITIONS, | |
18 | MTP_LOSERS | |
19 | } mtPieceKind; | |
20 | ||
21 | struct s_mtDeclarationPiece { | |
22 | mtPieceKind kind; | |
23 | /*@relnull@*/ void *node; /* oneof mt*Node or mttok */ | |
24 | } ; | |
25 | ||
26 | /* mtDeclarationPiece defined in forwardTypes.h */ | |
27 | ||
28 | /*@constant null mtDeclarationPiece mtDeclarationPiece_undefined; @*/ | |
29 | # define mtDeclarationPiece_undefined NULL | |
30 | ||
31 | extern /*@falsenull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ; | |
32 | # define mtDeclarationPiece_isDefined(p_h) ((p_h) != mtDeclarationPiece_undefined) | |
33 | ||
34 | extern /*@truenull@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ; | |
35 | # define mtDeclarationPiece_isUndefined(p_h) ((p_h) == mtDeclarationPiece_undefined) | |
36 | ||
37 | extern mtDeclarationPiece mtDeclarationPiece_createContext (/*@only@*/ mtContextNode) /*@*/ ; | |
38 | extern mtDeclarationPiece mtDeclarationPiece_createValues (/*@only@*/ mtValuesNode) /*@*/ ; | |
39 | extern mtDeclarationPiece mtDeclarationPiece_createDefaults (/*@only@*/ mtDefaultsNode) /*@*/ ; | |
40 | extern mtDeclarationPiece mtDeclarationPiece_createValueDefault (/*@only@*/ mttok) /*@*/ ; | |
41 | extern mtDeclarationPiece mtDeclarationPiece_createAnnotations (/*@only@*/ mtAnnotationsNode) /*@*/ ; | |
42 | extern mtDeclarationPiece mtDeclarationPiece_createMerge (/*@only@*/ mtMergeNode) /*@*/ ; | |
43 | extern mtDeclarationPiece mtDeclarationPiece_createTransfers (/*@only@*/ mtTransferClauseList) /*@*/ ; | |
44 | extern mtDeclarationPiece mtDeclarationPiece_createPostconditions (/*@only@*/ mtTransferClauseList) /*@*/ ; | |
45 | extern mtDeclarationPiece mtDeclarationPiece_createPreconditions (/*@only@*/ mtTransferClauseList) /*@*/ ; | |
46 | extern mtDeclarationPiece mtDeclarationPiece_createLosers (/*@only@*/ mtLoseReferenceList) /*@*/ ; | |
47 | ||
48 | extern /*@observer@*/ mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece) /*@*/ ; | |
49 | extern /*@only@*/ mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece p_node) /*@modifies p_node@*/ ; | |
50 | ||
51 | extern /*@observer@*/ mtValuesNode mtDeclarationPiece_getValues (mtDeclarationPiece) /*@*/ ; | |
52 | extern /*@observer@*/ mtDefaultsNode mtDeclarationPiece_getDefaults (mtDeclarationPiece) /*@*/ ; | |
53 | extern /*@observer@*/ mtAnnotationsNode mtDeclarationPiece_getAnnotations (mtDeclarationPiece) /*@*/ ; | |
54 | extern /*@observer@*/ mtMergeNode mtDeclarationPiece_getMerge (mtDeclarationPiece) /*@*/ ; | |
55 | extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getTransfers (mtDeclarationPiece) /*@*/ ; | |
56 | extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece) /*@*/ ; | |
57 | extern /*@observer@*/ mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPiece) /*@*/ ; | |
58 | extern /*@observer@*/ cstring mtDeclarationPiece_getDefaultValue (mtDeclarationPiece) /*@*/ ; | |
59 | ||
60 | extern /*@observer@*/ mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece) /*@*/ ; | |
61 | ||
62 | extern bool mtDeclarationPiece_matchKind (mtDeclarationPiece p_p, mtPieceKind p_kind) /*@*/ ; | |
63 | ||
64 | extern void mtDeclarationPiece_free (/*@only@*/ mtDeclarationPiece p_node) ; | |
65 | extern /*@only@*/ cstring mtDeclarationPiece_unparse (mtDeclarationPiece p_p) /*@*/ ; | |
66 | ||
67 | # else | |
68 | # error "Multiple include" | |
69 | # endif |