2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
7 ** mtDeclarationPiece.h
10 # ifndef MTDECLARATIONPIECE_H
11 # define MTDECLARATIONPIECE_H
13 /*@private@*/ typedef enum {
15 MTP_CONTEXT, MTP_VALUES, MTP_DEFAULTS, MTP_DEFAULTVALUE,
16 MTP_ANNOTATIONS, MTP_MERGE,
17 MTP_TRANSFERS, MTP_PRECONDITIONS, MTP_POSTCONDITIONS,
21 struct s_mtDeclarationPiece {
23 /*@relnull@*/ void *node; /* oneof mt*Node or mttok */
26 /* mtDeclarationPiece defined in forwardTypes.h */
28 /*@constant null mtDeclarationPiece mtDeclarationPiece_undefined; @*/
29 # define mtDeclarationPiece_undefined NULL
31 extern /*@falsewhennull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ;
32 # define mtDeclarationPiece_isDefined(p_h) ((p_h) != mtDeclarationPiece_undefined)
34 extern /*@nullwhentrue@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ;
35 # define mtDeclarationPiece_isUndefined(p_h) ((p_h) == mtDeclarationPiece_undefined)
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) /*@*/ ;
48 extern /*@observer@*/ mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece) /*@*/ ;
49 extern /*@only@*/ mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece p_node) /*@modifies p_node@*/ ;
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) /*@*/ ;
60 extern /*@observer@*/ mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece) /*@*/ ;
62 extern bool mtDeclarationPiece_matchKind (mtDeclarationPiece p_p, mtPieceKind p_kind) /*@*/ ;
64 extern void mtDeclarationPiece_free (/*@only@*/ mtDeclarationPiece p_node) ;
65 extern /*@only@*/ cstring mtDeclarationPiece_unparse (mtDeclarationPiece p_p) /*@*/ ;
68 # error "Multiple include"