]>
Commit | Line | Data |
---|---|---|
885824d3 | 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 | ||
28bf4b0b | 14 | /*@null@*/ struct s_guardSet |
885824d3 | 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 /*@falsenull@*/ /*@unused@*/ bool | |
24 | guardSet_isDefined (guardSet p_g) /*@*/ ; | |
25 | # define guardSet_isDefined(g) ((g) != guardSet_undefined) | |
26 | ||
27 | extern /*@falsenull@*/ bool guardSet_isEmpty (guardSet p_g); | |
28 | ||
29 | extern /*@only@*/ guardSet guardSet_new (void); | |
28bf4b0b | 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); | |
885824d3 | 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) /*@*/ ; | |
28bf4b0b | 46 | extern bool guardSet_mustBeNull (guardSet p_g, sRef p_s) /*@*/ ; |
885824d3 | 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 |