src/Headers/guardSet.h

   1 /*
   2 ** guardSet.h
   3 */
   4
   5 # ifndef GUARDSET_H
   6 # define GUARDSET_H
   7
   8 /*
   9 ** guardSet is usually empty, so allow NULL to represent this.
  10 */
  11
  12 /* in forwardTypes: typedef struct _guardSet *guardSet; */
  13
  14 /*@null@*/ struct s_guardSet
  15 {
  16   /*@only@*/ sRefSet tguard; /* guarded on true branch */
  17   /*@only@*/ sRefSet fguard; /* guarded on false branch */
  18 } ;
  19
  20 /*@constant null guardSet guardSet_undefined;@*/
  21 # define guardSet_undefined     ((guardSet)NULL)
  22
  23 extern /*@falsewhennull@*/ /*@unused@*/ bool
  24   guardSet_isDefined (guardSet p_g) /*@*/ ;
  25 # define guardSet_isDefined(g)  ((g) != guardSet_undefined)
  26
  27 extern /*@falsewhennull@*/ bool guardSet_isEmpty (guardSet p_g);
  28
  29 extern /*@only@*/ guardSet guardSet_new (void);
  30 extern guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet p_g, /*@exposed@*/ sRef p_s);
  31 extern guardSet guardSet_addFalseGuard (/*@returned@*/ guardSet p_g, /*@exposed@*/ sRef p_s);
  32 extern guardSet guardSet_or (/*@returned@*/ /*@unique@*/ guardSet p_s, guardSet p_t);
  33 extern guardSet guardSet_and (/*@returned@*/ /*@unique@*/ guardSet p_s, guardSet p_t);
  34 extern void guardSet_delete (guardSet p_g, sRef p_s) /*@modifies p_g@*/ ;
  35 extern /*@only@*/ cstring guardSet_unparse (guardSet p_g);
  36 extern void guardSet_free (/*@only@*/ /*@only@*/ guardSet p_g);
  37 extern /*@dependent@*/ /*@exposed@*/ sRefSet
  38   guardSet_getTrueGuards (guardSet p_g) /*@*/ ;
  39 extern /*@dependent@*/ /*@exposed@*/ sRefSet
  40   guardSet_getFalseGuards (guardSet p_g) /*@*/ ;
  41 extern guardSet guardSet_union (/*@only@*/ guardSet p_s, guardSet p_t)
  42    /*@modifies p_s@*/ ;
  43 extern /*@only@*/ guardSet guardSet_invert (/*@temp@*/ guardSet p_g) /*@*/ ;
  44 extern /*@only@*/ guardSet guardSet_copy (/*@temp@*/ guardSet p_g) /*@*/ ;
  45 extern bool guardSet_isGuarded (guardSet p_g, sRef p_s) /*@*/ ;
  46 extern bool guardSet_mustBeNull (guardSet p_g, sRef p_s) /*@*/ ;
  47
  48 extern guardSet
  49   guardSet_levelUnion (/*@only@*/ guardSet p_s,
  50                        guardSet p_t, int p_lexlevel)
  51   /*@modifies p_s@*/ ;
  52 extern guardSet
  53   guardSet_levelUnionFree (/*@returned@*/ /*@unique@*/ guardSet p_s,
  54                            /*@only@*/ guardSet p_t, int p_lexlevel)
  55   /*@modifies p_t, p_s@*/ ;
  56
  57 extern void guardSet_flip (guardSet p_g);
  58
  59 # else
  60 # error "Multiple include"
  61 # endif