src/Headers/functionClause.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 /*
   7 ** functionClause.h
   8 */
   9
  10 # ifndef FUNCTIONCLAUSE_H
  11 # define FUNCTIONCLAUSE_H
  12
  13 /*@private@*/ typedef enum {
  14   FCK_GLOBALS,
  15   FCK_MODIFIES,
  16   FCK_WARN,
  17   FCK_STATE,
  18   FCK_ENSURES,
  19   FCK_REQUIRES,
  20   FCK_MTENSURES,
  21   FCK_MTREQUIRES,
  22   FCK_DEAD
  23 } functionClauseKind;
  24
  25 struct s_functionClause {
  26   functionClauseKind kind;
  27   union {
  28     globalsClause globals;
  29     modifiesClause modifies;
  30     warnClause warn;
  31     stateClause state;
  32     constraintList ensures;
  33     constraintList requires;
  34     metaStateConstraint mtconstraint;
  35   } val;
  36 } ;
  37
  38 /* functionClause defined in forwardTypes.h */
  39
  40 /*@constant null functionClause functionClause_undefined; @*/
  41 # define functionClause_undefined NULL
  42
  43 extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
  44 # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined)
  45
  46 extern bool functionClause_isGlobals (functionClause) /*@*/ ;
  47 # define functionClause_isGlobals(p_h) (functionClause_matchKind(p_h, FCK_GLOBALS))
  48
  49 extern bool functionClause_isNoMods (/*@sef@*/ functionClause) /*@*/ ;
  50 # define functionClause_isNoMods(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES) && modifiesClause_isNoMods (functionClause_getModifies (p_h)))
  51 extern bool functionClause_isModifies (functionClause) /*@*/ ;
  52 # define functionClause_isModifies(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES))
  53
  54 extern bool functionClause_isState (functionClause) /*@*/ ;
  55 # define functionClause_isState(p_h) (functionClause_matchKind(p_h, FCK_STATE))
  56
  57 extern bool functionClause_isWarn (functionClause) /*@*/ ;
  58 # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN))
  59
  60 extern bool functionClause_isEnsures (functionClause) /*@*/ ;
  61 # define functionClause_isEnsures(p_h) (functionClause_matchKind(p_h, FCK_ENSURES))
  62
  63 extern bool functionClause_isRequires (functionClause) /*@*/ ;
  64 # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
  65
  66 extern bool functionClause_isMetaRequires (functionClause) /*@*/ ;
  67 # define functionClause_isMetaRequires(p_h) (functionClause_matchKind(p_h, FCK_MTREQUIRES))
  68
  69 extern bool functionClause_isMetaEnsures (functionClause) /*@*/ ;
  70 # define functionClause_isMetaEnsures(p_h) (functionClause_matchKind(p_h, FCK_MTENSURES))
  71
  72 extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
  73 # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
  74
  75 extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ;
  76 extern functionClause functionClause_createModifies (/*@only@*/ modifiesClause) /*@*/ ;
  77 extern functionClause functionClause_createWarn (/*@only@*/ warnClause) /*@*/ ;
  78 extern functionClause functionClause_createState (/*@only@*/ stateClause) /*@*/ ;
  79 extern functionClause functionClause_createEnsures (/*@only@*/ constraintList) /*@*/ ;
  80 extern functionClause functionClause_createRequires (/*@only@*/ constraintList) /*@*/ ;
  81 extern functionClause functionClause_createMetaEnsures (/*@only@*/ metaStateConstraint) /*@*/ ;
  82 extern functionClause functionClause_createMetaRequires (/*@only@*/ metaStateConstraint) /*@*/ ;
  83
  84 extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ;
  85 extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ;
  86 extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ;
  87 extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ;
  88 extern /*@exposed@*/ constraintList functionClause_getEnsures (functionClause) /*@*/ ;
  89 extern /*@exposed@*/ constraintList functionClause_getRequires (functionClause) /*@*/ ;
  90 extern /*@exposed@*/ metaStateConstraint functionClause_getMetaConstraint (functionClause) /*@*/ ;
  91
  92 extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ;
  93 extern /*@only@*/ constraintList functionClause_takeEnsures (functionClause p_fc) /*@modifies p_fc@*/ ;
  94 extern /*@only@*/ constraintList functionClause_takeRequires (functionClause p_fc) /*@modifies p_fc@*/ ;
  95 extern /*@only@*/ metaStateConstraint functionClause_takeMetaConstraint (functionClause p_fc) /*@modifies p_fc@*/ ;
  96 extern /*@only@*/ warnClause functionClause_takeWarn (functionClause p_fc) /*@modifies p_fc@*/ ;
  97
  98 extern bool functionClause_matchKind (functionClause p_p, functionClauseKind p_kind) /*@*/ ;
  99
 100 extern void functionClause_free (/*@only@*/ functionClause p_node) ;
 101 extern /*@only@*/ cstring functionClause_unparse (functionClause p_p) /*@*/ ;
 102
 103 # else
 104 # error "Multiple include"
 105 # endif