9 ** guardSet is usually empty, so allow NULL to represent this.
12 /* in forwardTypes: typedef struct _guardSet *guardSet; */
14 /*@null@*/ struct s_guardSet
16 /*@only@*/ sRefSet tguard; /* guarded on true branch */
17 /*@only@*/ sRefSet fguard; /* guarded on false branch */
20 /*@constant null guardSet guardSet_undefined;@*/
21 # define guardSet_undefined ((guardSet)NULL)
23 extern /*@falsewhennull@*/ /*@unused@*/ bool
24 guardSet_isDefined (guardSet p_g) /*@*/ ;
25 # define guardSet_isDefined(g) ((g) != guardSet_undefined)
27 extern /*@falsewhennull@*/ bool guardSet_isEmpty (guardSet p_g);
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)
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) /*@*/ ;
49 guardSet_levelUnion (/*@only@*/ guardSet p_s,
50 guardSet p_t, int p_lexlevel)
53 guardSet_levelUnionFree (/*@returned@*/ /*@unique@*/ guardSet p_s,
54 /*@only@*/ guardSet p_t, int p_lexlevel)
55 /*@modifies p_t, p_s@*/ ;
57 extern void guardSet_flip (guardSet p_g);
60 # error "Multiple include"