src/Headers/stateClause.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** stateClause.h
   7 */
   8
   9 # ifndef STATECLAUSE_H
  10 # define STATECLAUSE_H
  11
  12 typedef enum
  13 {
  14   SP_USES,
  15   SP_DEFINES,
  16   SP_ALLOCATES,
  17   SP_RELEASES,
  18   SP_SETS,
  19   SP_QUAL,
  20   SP_GLOBAL
  21 } stateClauseKind ;
  22
  23 typedef enum
  24 {
  25   TK_BEFORE,
  26   TK_AFTER,
  27   TK_BOTH
  28 } stateConstraint;
  29
  30 struct s_stateClause
  31 {
  32   stateConstraint state;
  33   stateClauseKind kind;
  34   qual squal; /* only for SP_QUAL and SP_GLOBAL */
  35   sRefSet refs;
  36   fileloc loc;
  37 } ;
  38
  39 /* in forwardTypes.h: abst_typedef struct _stateClause *stateClause; */
  40
  41 typedef /*@only@*/ stateClause o_stateClause;
  42
  43 extern /*@unused@*/ cstring stateClause_unparse (stateClause p_s) /*@*/ ;
  44
  45 extern /*@null@*/ sRefMod
  46   stateClause_getEffectFunction (stateClause p_cl) /*@*/ ;
  47
  48 extern /*@null@*/ sRefModVal
  49   stateClause_getEnsuresFunction (stateClause p_cl) /*@*/ ;
  50
  51 extern /*@null@*/ sRefModVal
  52   stateClause_getRequiresBodyFunction (stateClause p_cl) /*@*/ ;
  53
  54 extern int
  55   stateClause_getStateParameter (stateClause p_cl) /*@*/ ;
  56
  57 extern /*@null@*/ sRefMod
  58   stateClause_getReturnEffectFunction (stateClause p_cl) /*@*/ ;
  59
  60 extern /*@null@*/ sRefMod
  61   stateClause_getEntryFunction (stateClause p_cl) /*@*/ ;
  62
  63 extern bool stateClause_isGlobal (stateClause p_cl) /*@*/ ;
  64 # define stateClause_isGlobal(cl) ((cl)->kind == SP_GLOBAL)
  65
  66 extern bool stateClause_isBefore (stateClause p_cl) /*@*/ ;
  67 extern bool stateClause_isBeforeOnly (stateClause p_cl) /*@*/ ;
  68 extern bool stateClause_isAfter (stateClause p_cl) /*@*/ ;
  69 extern bool stateClause_isEnsures (stateClause p_cl) /*@*/ ;
  70
  71 extern bool stateClause_sameKind (stateClause p_s1, stateClause p_s2) /*@*/ ;
  72
  73 extern /*@observer@*/ sRefSet stateClause_getRefs (stateClause p_cl) /*@*/ ;
  74 # define stateClause_getRefs(cl) ((cl)->refs)
  75
  76 extern flagcode stateClause_preErrorCode (stateClause p_cl) /*@*/ ;
  77 extern /*@observer@*/ cstring
  78   stateClause_preErrorString (stateClause p_cl, sRef p_sr) /*@*/ ;
  79
  80 extern flagcode stateClause_postErrorCode (stateClause p_cl) /*@*/ ;
  81 extern /*@observer@*/ cstring
  82   stateClause_postErrorString (stateClause p_cl, sRef p_sr) /*@*/ ;
  83
  84 extern sRefTest stateClause_getPreTestFunction (stateClause p_cl) /*@*/ ;
  85 extern sRefTest stateClause_getPostTestFunction (stateClause p_cl) /*@*/ ;
  86 extern sRefShower stateClause_getPostTestShower (stateClause p_cl) /*@*/ ;
  87
  88 extern stateClause
  89   stateClause_create (lltok p_tok, qual p_q, /*@only@*/ sRefSet p_s) /*@*/ ;
  90
  91 extern stateClause
  92   stateClause_createPlain (lltok p_tok, /*@only@*/ sRefSet p_s) /*@*/ ;
  93
  94 extern stateClause stateClause_createDefines (/*@only@*/ sRefSet p_s) /*@*/ ;
  95 extern stateClause stateClause_createUses (/*@only@*/ sRefSet p_s) /*@*/ ;
  96 extern stateClause stateClause_createAllocates (/*@only@*/ sRefSet p_s) /*@*/ ;
  97 extern stateClause stateClause_createReleases (/*@only@*/ sRefSet p_s) /*@*/ ;
  98 extern stateClause stateClause_createSets (/*@only@*/ sRefSet p_s) /*@*/ ;
  99
 100 extern /*@observer@*/ fileloc stateClause_loc (stateClause) /*@*/ ;
 101 extern bool stateClause_isMemoryAllocation (stateClause p_cl) /*@*/ ;
 102 extern bool stateClause_isQual (stateClause p_cl) /*@*/ ;
 103
 104 extern void stateClause_free (/*@only@*/ stateClause p_s) ;
 105 extern cstring stateClause_dump (stateClause p_s) /*@*/ ;
 106 extern stateClause stateClause_undump (char **p_s) /*@modifies *p_s@*/ ;
 107 extern stateClause stateClause_copy (stateClause p_s) /*@*/ ;
 108 extern bool stateClause_matchKind (stateClause p_s1, stateClause p_s2) /*@*/ ;
 109
 110 extern bool stateClause_hasEnsures (stateClause p_cl) /*@*/ ;
 111 extern bool stateClause_hasRequires (stateClause p_cl) /*@*/ ;
 112
 113 extern bool stateClause_setsMetaState (stateClause p_cl) /*@*/ ;
 114 extern qual stateClause_getMetaQual (stateClause p_cl) /*@*/ ;
 115
 116 extern bool stateClause_hasEmptyReferences (stateClause p_s);
 117
 118 extern bool stateClause_isMetaState (stateClause p_s);
 119
 120 # else
 121 # error "Multiple include"
 122 # endif
 123
 124