src/Headers/mtDeclarationPiece.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   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 /*@falsewhennull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ;
  32 # define mtDeclarationPiece_isDefined(p_h) ((p_h) != mtDeclarationPiece_undefined)
  33
  34 extern /*@nullwhentrue@*/ 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