Fixed problem with NULL being changed.

[splint.git] / src / Headers / guardSet.h

diff --git a/src/Headers/guardSet.h b/src/Headers/guardSet.h
index 9678cde06527c5f39836172decc8fe7863abe9fd..302dd64577d72ba1e109ca7af70252864ce51588 100644 (file)
--- a/src/Headers/guardSet.h
+++ b/src/Headers/guardSet.h
@@ -11,7 +11,7 @@
 
 /* in forwardTypes: typedef struct _guardSet *guardSet; */
 
-/*@null@*/ struct _guardSet
+/*@null@*/ struct s_guardSet
 {
   /*@only@*/ sRefSet tguard; /* guarded on true branch */
   /*@only@*/ sRefSet fguard; /* guarded on false branch */
@@ -20,15 +20,15 @@
 /*@constant null guardSet guardSet_undefined;@*/
 # define guardSet_undefined     ((guardSet)NULL)
 
-extern /*@falsenull@*/ /*@unused@*/ bool 
+extern /*@falsewhennull@*/ /*@unused@*/ bool 
   guardSet_isDefined (guardSet p_g) /*@*/ ;
 # define guardSet_isDefined(g)  ((g) != guardSet_undefined)
 
-extern /*@falsenull@*/ bool guardSet_isEmpty (guardSet p_g);
+extern /*@falsewhennull@*/ bool guardSet_isEmpty (guardSet p_g);
 
 extern /*@only@*/ guardSet guardSet_new (void);
-extern guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet p_g, sRef p_s);
-extern guardSet guardSet_addFalseGuard (/*@returned@*/ guardSet p_g, sRef p_s);
+extern guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet p_g, /*@exposed@*/ sRef p_s);
+extern guardSet guardSet_addFalseGuard (/*@returned@*/ guardSet p_g, /*@exposed@*/ sRef p_s);
 extern guardSet guardSet_or (/*@returned@*/ /*@unique@*/ guardSet p_s, guardSet p_t);
 extern guardSet guardSet_and (/*@returned@*/ /*@unique@*/ guardSet p_s, guardSet p_t);
 extern void guardSet_delete (guardSet p_g, sRef p_s) /*@modifies p_g@*/ ;
@@ -43,7 +43,7 @@ extern guardSet guardSet_union (/*@only@*/ guardSet p_s, guardSet p_t)
 extern /*@only@*/ guardSet guardSet_invert (/*@temp@*/ guardSet p_g) /*@*/ ;
 extern /*@only@*/ guardSet guardSet_copy (/*@temp@*/ guardSet p_g) /*@*/ ;
 extern bool guardSet_isGuarded (guardSet p_g, sRef p_s) /*@*/ ;
-extern bool guardSet_isProbableNull (guardSet p_g, sRef p_s) /*@*/ ;
+extern bool guardSet_mustBeNull (guardSet p_g, sRef p_s) /*@*/ ;
 
 extern guardSet
   guardSet_levelUnion (/*@only@*/ guardSet p_s,