Renamed truenull nullwhentrue and falsenull falsewhennull

diff --git a/README b/README
index 6b72cc0cef3adb5c9c27461dfe7ab15baae1a459..608139806499e95dd24d20806a585f0043e74854 100644 (file)
--- a/README
+++ b/README
@@ -61,10 +61,10 @@ the derived grammar files.  This is not recommended however.
 
    LARCH_PATH - path to search for splint libraries and
    initializations files. If you are using the standard directories, this
-   should be .:<base-directory>/splint-3.0.0.9/lib.
+   should be .:<base-directory>/splint-3.0.0.20/lib.
 
    LCLIMPORTDIR - directory containing lcl imports files. If you are using
-   the standard directories, this is <base-directory>/splint-3.0.0.9/imports.
+   the standard directories, this is <base-directory>/splint-3.0.0.20/imports.
 
    Put the commands to set these variables (the actual commands will depend
    on the shell you are using) in one of your initialization dotfiles

diff --git a/src/Headers/aliasTable.h b/src/Headers/aliasTable.h
index 4aaceb31847d2ecbfe597185c7cfb2f0d8e6c37f..9075ab35f975448edb04a1055026e6ef00462629 100644 (file)
--- a/src/Headers/aliasTable.h
+++ b/src/Headers/aliasTable.h
@@ -21,10 +21,10 @@ struct s_aliasTable /*@i32 reserved works for struct identifiers@*/
   /*@reldef@*/ /*@only@*/ o_sRefSet *values;
 } ; 
 
-extern /*@unused@*/ /*@truenull@*/ bool aliasTable_isUndefined (aliasTable p_s);
-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@unused@*/ /*@nullwhentrue@*/ bool aliasTable_isUndefined (aliasTable p_s);
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 
   aliasTable_isEmpty (/*@sef@*/ aliasTable p_s);
-extern /*@falsenull@*/ bool aliasTable_isDefined (aliasTable p_s);
+extern /*@falsewhennull@*/ bool aliasTable_isDefined (aliasTable p_s);
 
 /*@constant null aliasTable aliasTable_undefined; @*/
 # define aliasTable_undefined      ((aliasTable) NULL)

diff --git a/src/Headers/annotationInfo.h b/src/Headers/annotationInfo.h
index 0ce3da9b17260c3964c110c48ce9d778f93ed700..1e1dac74350a7630c3e306f2e6b715a3505373a9 100644 (file)
--- a/src/Headers/annotationInfo.h
+++ b/src/Headers/annotationInfo.h
@@ -26,10 +26,10 @@ struct s_annotationInfo {
 /*@constant null annotationInfo annotationInfo_undefined; @*/
 # define annotationInfo_undefined    ((annotationInfo) NULL)
 
-extern /*@falsenull@*/ bool annotationInfo_isDefined (annotationInfo) /*@*/ ;
+extern /*@falsewhennull@*/ bool annotationInfo_isDefined (annotationInfo) /*@*/ ;
 # define annotationInfo_isDefined(p_info) ((p_info) != annotationInfo_undefined)
 
-extern /*@truenull@*/ bool annotationInfo_isUndefined (annotationInfo) /*@*/ ;
+extern /*@nullwhentrue@*/ bool annotationInfo_isUndefined (annotationInfo) /*@*/ ;
 # define annotationInfo_isUndefined(p_info) ((p_info) == annotationInfo_undefined)
 
 extern bool annotationInfo_equal (annotationInfo, annotationInfo) /*@*/ ;

diff --git a/src/Headers/annotationTable.h b/src/Headers/annotationTable.h
index 054e1ecf4da3b3462755054aea8f6dbae022bbd8..25898b5908b4f92f5587e8e08e7389f22f335ad5 100644 (file)
--- a/src/Headers/annotationTable.h
+++ b/src/Headers/annotationTable.h
@@ -21,10 +21,10 @@
 /*@constant null annotationTable annotationTable_undefined; @*/
 # define annotationTable_undefined genericTable_undefined
 
-extern /*@falsenull@*/ bool annotationTable_isDefined(annotationTable) /*@*/ ;
+extern /*@falsewhennull@*/ bool annotationTable_isDefined(annotationTable) /*@*/ ;
 # define annotationTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
-extern /*@truenull@*/ bool annotationTable_isUndefined(annotationTable) /*@*/ ;
+extern /*@nullwhentrue@*/ bool annotationTable_isUndefined(annotationTable) /*@*/ ;
 # define annotationTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
 /*@constant int DEFAULT_ANNOTTABLE_SIZE@*/

diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h
index 0f248391142e7868f224ac45eba7faf5513e14b5..22f89419e90dc6a0a8f3ea7496ae7ae85acf5a2e 100644 (file)
--- a/src/Headers/constraint.h
+++ b/src/Headers/constraint.h
@@ -23,9 +23,9 @@ struct s_constraint {
 
 # define constraint_undefined ((constraint)NULL)
 
-extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
-extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ;
 
 # define constraint_isDefined(e)        ((e) != constraint_undefined)
 # define constraint_isUndefined(e)      ((e) == constraint_undefined)

diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h
index 64208e666909872d1556b2394eee07b11cc9752a..5035a54f0341c957f50f4bbd05defb64556100b3 100644 (file)
--- a/src/Headers/constraintExpr.h
+++ b/src/Headers/constraintExpr.h
@@ -20,9 +20,9 @@ struct s_constraintExpr {
 /*@constant null constraintExpr constraintExpr_undefined; @*/
 # define constraintExpr_undefined ((constraintExpr)NULL)
 
-extern /*@falsenull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ;
 
 # define constraintExpr_isDefined(e)        ((e) != constraintExpr_undefined)
 # define constraintExpr_isUndefined(e)      ((e) == constraintExpr_undefined)
@@ -83,7 +83,7 @@ constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr
 
 /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/  constraintExpr p_expr, /*@observer@*/ exprNode p_fcnCall);
 
-/*@falsenull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ;
+/*@falsewhennull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ;
 
 /*@only@*/ constraintExpr constraintExpr_makeAddExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent);
 
@@ -104,7 +104,7 @@ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr p_ex
                                                /*@out@*/ bool * p_propagate,
                                                  /*@out@*/ int *p_literal);
 
-/*@falsenull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ;
+/*@falsewhennull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ;
 
 extern void  constraintExpr_dump (/*@observer@*/ /*@temp@*/ constraintExpr p_expr,  FILE *p_f);
 

diff --git a/src/Headers/constraintExprData.h b/src/Headers/constraintExprData.h
index 4f7564fc7581630b1cd13317051c60f4a105ce10..ffa97ac6de1dc8c41b0788a6bc9e5fb131eb3a90 100644 (file)
--- a/src/Headers/constraintExprData.h
+++ b/src/Headers/constraintExprData.h
@@ -41,7 +41,7 @@ typedef union constraintExprData
   constraintTerm term;
 } *constraintExprData;
 
-extern /*@falsenull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ;
 # define constraintExprData_isDefined(e)      ((e) != NULL)
 
 extern void constraintExprData_freeBinaryExpr (/*@only@*/ constraintExprData) ;

diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h
index 277093234f543c5a00c18c3360db60290d4c6a10..816e8e63d4eb9ccbe6ee6f1d19c1b48e5d62b33e 100644 (file)
--- a/src/Headers/constraintList.h
+++ b/src/Headers/constraintList.h
@@ -18,9 +18,9 @@ struct s_constraintList
 
 # define constraintList_undefined ((constraintList)NULL)
 
-extern /*@falsenull@*/ bool constraintList_isDefined (constraintList p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool constraintList_isUndefined (constraintList p_e) /*@*/ ;
-extern /*@truenull@*/ /*@unused@*/ bool constraintList_isError (constraintList p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool constraintList_isDefined (constraintList p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintList_isUndefined (constraintList p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool constraintList_isError (constraintList p_e) /*@*/ ;
 
 # define constraintList_isDefined(e)    ((e) != constraintList_undefined)
 # define constraintList_isUndefined(e)  ((e) == constraintList_undefined)

diff --git a/src/Headers/constraintList2.h b/src/Headers/constraintList2.h
index 7e8cbbff12aad720302d7b2e4cc3fa8c17f18deb..72df086e4ee945392a212e921d71870ca946df50 100644 (file)
--- a/src/Headers/constraintList2.h
+++ b/src/Headers/constraintList2.h
@@ -32,7 +32,7 @@ extern int constraintList_size (/*@sef@*/ constraintList);
 extern bool constraintList_empty (/*@sef@*/ constraintList);
 # define constraintList_empty(s) (constraintList_size(s) == 0)
 
-extern /*@falsenull@*/ bool constraintList_isDefined (constraintList p_t);
+extern /*@falsewhennull@*/ bool constraintList_isDefined (constraintList p_t);
 # define constraintList_isDefined(s) ((s) != (constraintList) 0)
 
 extern /*@only@*/ constraintList constraintList_makeNew(void);

diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h
index 8a4ce5aa06120e241bee67f42d561b120efa08f5..7755f554a57d1d0a13561278fe1c1817f3bc8e64 100644 (file)
--- a/src/Headers/cstring.h
+++ b/src/Headers/cstring.h
@@ -129,11 +129,11 @@ extern void cstring_free (/*@only@*/ cstring p_s);
 /*@constant null cstring cstring_undefined;@*/
 # define cstring_undefined     ((cstring)NULL)
 
-extern /*@falsenull@*/ bool cstring_isDefined (cstring p_s) /*@*/ ;
-extern /*@truenull@*/ bool cstring_isUndefined (cstring p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstring_isDefined (cstring p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool cstring_isUndefined (cstring p_s) /*@*/ ;
 
-extern /*@truenull@*/ bool cstring_isEmpty (cstring p_s) /*@*/ ;
-extern /*@falsenull@*/ bool cstring_isNonEmpty (cstring p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool cstring_isEmpty (cstring p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstring_isNonEmpty (cstring p_s) /*@*/ ;
 
 # define cstring_isDefined(s)   ((s) != cstring_undefined)
 # define cstring_isUndefined(s) (!cstring_isDefined(s))

diff --git a/src/Headers/cstringList.h b/src/Headers/cstringList.h
index 3c912346d6b7b867c5976e0f601c6718af7562fd..6a655075dc2cf696748db47d1b4346a7eecbae15 100644 (file)
--- a/src/Headers/cstringList.h
+++ b/src/Headers/cstringList.h
@@ -16,13 +16,13 @@ abst_typedef /*@null@*/ struct s_cstringList
 /*@constant null cstringList cstringList_undefined;@*/
 # define cstringList_undefined ((cstringList) NULL)
 
-extern /*@falsenull@*/ bool cstringList_isDefined (cstringList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstringList_isDefined (cstringList p_s) /*@*/ ;
 # define cstringList_isDefined(s)   ((s) != cstringList_undefined)
 
 extern int cstringList_size (/*@sef@*/ cstringList) /*@*/ ;
 # define cstringList_size(s) (cstringList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool cstringList_empty (/*@sef@*/ cstringList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool cstringList_empty (/*@sef@*/ cstringList) /*@*/ ;
 # define cstringList_empty(s) (cstringList_size(s) == 0)
 
 extern cstring cstringList_unparseSep (cstringList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/cstringSList.h b/src/Headers/cstringSList.h
index dbf4e0b4bbdb7a7c139158f40d68ba5736a7b843..609878796ed348d9e9a380e4f64b7f371f9d8f58 100644 (file)
--- a/src/Headers/cstringSList.h
+++ b/src/Headers/cstringSList.h
@@ -18,13 +18,13 @@ abst_typedef /*@null@*/ struct s_cstringSList
 /*@constant null cstringSList cstringSList_undefined;@*/
 # define cstringSList_undefined ((cstringSList) NULL)
 
-extern /*@falsenull@*/ bool cstringSList_isDefined (cstringSList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstringSList_isDefined (cstringSList p_s) /*@*/ ;
 # define cstringSList_isDefined(s)   ((s) != cstringSList_undefined)
 
 extern int cstringSList_size (/*@sef@*/ cstringSList) /*@*/ ;
 # define cstringSList_size(s) (cstringSList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@falsenull@*/ bool cstringSList_empty (/*@sef@*/ cstringSList) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstringSList_empty (/*@sef@*/ cstringSList) /*@*/ ;
 # define cstringSList_empty(s) (cstringSList_size(s) == 0)
 
 extern /*@unused@*/ cstring cstringSList_unparseSep (cstringSList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/cstringTable.h b/src/Headers/cstringTable.h
index 576aa485dcc0e18c7a93f4277e44801c99e780b5..053c4da3cf2bad41c1527276b3e587a1e3cd081d 100644 (file)
--- a/src/Headers/cstringTable.h
+++ b/src/Headers/cstringTable.h
@@ -48,10 +48,10 @@ struct s_cstringTable
 /*@constant null cstringTable cstringTable_undefined; @*/
 # define cstringTable_undefined      ((cstringTable) NULL)
 
-extern /*@falsenull@*/ bool cstringTable_isDefined(cstringTable) /*@*/ ;
+extern /*@falsewhennull@*/ bool cstringTable_isDefined(cstringTable) /*@*/ ;
 # define cstringTable_isDefined(p_h) ((p_h) != cstringTable_undefined)
 
-extern /*@truenull@*/ /*@unused@*/ bool cstringTable_isUndefined(cstringTable) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool cstringTable_isUndefined(cstringTable) /*@*/ ;
 # define cstringTable_isUndefined(p_h) ((p_h) == cstringTable_undefined)
 
 extern /*@only@*/ cstringTable cstringTable_create(int p_size) /*@*/ ;

diff --git a/src/Headers/ctypeList.h b/src/Headers/ctypeList.h
index 32f1c8cfec4b018c34e7c761542648cedd84af38..7c3fecce2007ce2d9545c0f238699885cb6937fb 100644 (file)
--- a/src/Headers/ctypeList.h
+++ b/src/Headers/ctypeList.h
@@ -35,8 +35,8 @@ extern ctypeList ctypeList_add (/*@only@*/ ctypeList p_s, ctype p_el) /*@modifie
 extern /*@unused@*/ /*@only@*/ cstring ctypeList_unparse (ctypeList) /*@*/ ;
 extern void ctypeList_free (/*@only@*/ /*@only@*/ ctypeList p_s) /*@modifies p_s@*/;
 
-extern /*@falsenull@*/ bool ctypeList_isDefined (/*@null@*/ ctypeList p_ct) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@falsewhennull@*/ bool ctypeList_isDefined (/*@null@*/ ctypeList p_ct) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 
   ctypeList_isUndefined (/*@null@*/ ctypeList p_ct) /*@*/ ;
 
 /*@constant null ctypeList ctypeList_undefined; @*/

diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h
index 327fadaad525f1c1064235d904891e8b1e122a4e..cd6d69cbe200c6f856d8937857ad37555039ca75 100644 (file)
--- a/src/Headers/exprNode.h
+++ b/src/Headers/exprNode.h
@@ -174,9 +174,9 @@ struct s_exprNode
 /*@constant null exprNode exprNode_undefined; @*/
 # define exprNode_undefined ((exprNode)NULL)
 
-extern /*@falsenull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
-extern /*@truenull@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ;
+extern /*@nullwhentrue@*/ bool exprNode_isError (exprNode p_e) /*@*/ ;
 
 # define exprNode_isDefined(e)        ((e) != exprNode_undefined)
 # define exprNode_isUndefined(e)      ((e) == exprNode_undefined)
@@ -191,7 +191,7 @@ extern ctype exprNode_getType (/*@sef@*/ exprNode p_e) /*@*/ ;
 # define exprNode_getType(e) \
   (exprNode_isDefined(e) ? (e)->typ : ctype_unknown)
 
-extern /*@unused@*/ /*@falsenull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ;
 # define exprNode_isInParens(e) \
   (exprNode_isDefined(e) && (e)->kind == XPR_PARENS)
 

diff --git a/src/Headers/fcnNodeList.h b/src/Headers/fcnNodeList.h
index 93b61b93b6ad0d3e4766629ef3553f7c9b43c88f..c2be6857d4f1345c469ce95a9f0168a0c289ce37 100644 (file)
--- a/src/Headers/fcnNodeList.h
+++ b/src/Headers/fcnNodeList.h
@@ -28,10 +28,10 @@ abst_typedef /*@null@*/ struct
 /*@constant null fcnNodeList fcnNodeList_undefined; @*/
 # define fcnNodeList_undefined ((fcnNodeList)0)
 
-extern /*@falsenull@*/ bool fcnNodeList_isDefined (fcnNodeList p_f);
+extern /*@falsewhennull@*/ bool fcnNodeList_isDefined (fcnNodeList p_f);
 # define fcnNodeList_isDefined(f) ((f) != fcnNodeList_undefined)
 
-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 
   fcnNodeList_isUndefined (fcnNodeList p_f);
 # define fcnNodeList_isUndefined(f) ((f) == fcnNodeList_undefined)
 

diff --git a/src/Headers/fileIdList.h b/src/Headers/fileIdList.h
index 46fce9a376d343e66ccb850e6dbe7d74c1c42820..0e5b171a62bf6369ab63118139461c0b799057b7 100644 (file)
--- a/src/Headers/fileIdList.h
+++ b/src/Headers/fileIdList.h
@@ -15,7 +15,7 @@
 
 abst_typedef /*@null@*/ ctypeList fileIdList;
 
-extern /*@falsenull@*/ bool fileIdList_isDefined (fileIdList p_f);
+extern /*@falsewhennull@*/ bool fileIdList_isDefined (fileIdList p_f);
 # define fileIdList_isDefined(f)  (ctypeList_isDefined (f))
 
 /*@iter fileIdList_elements (sef fileIdList x, yield fileId el); @*/

diff --git a/src/Headers/fileTable.h b/src/Headers/fileTable.h
index 832e2aaa921abce93c7dc9be8635537c078f7887..d1dd875a3b5c4369eb671bac85fe9c5d0687508f 100644 (file)
--- a/src/Headers/fileTable.h
+++ b/src/Headers/fileTable.h
@@ -57,9 +57,9 @@ abst_typedef /*@null@*/ struct
 /*@constant null fileTable fileTable_undefined; @*/
 # define fileTable_undefined ((fileTable) NULL)
 
-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 
   fileTable_isUndefined (/*@null@*/ fileTable p_f) /*@*/ ;
-extern /*@unused@*/ /*@falsenull@*/ bool 
+extern /*@unused@*/ /*@falsewhennull@*/ bool 
   fileTable_isDefined (/*@null@*/ fileTable p_f) /*@*/ ;
 
 # define fileTable_isUndefined(ft) ((ft) == fileTable_undefined)

diff --git a/src/Headers/fileloc.h b/src/Headers/fileloc.h
index 21e98bbe268b056ab7031a2235a92a33aa22ad1b..d8dc68cbe0c3d5debd1710010dddebf89746ee2a 100644 (file)
--- a/src/Headers/fileloc.h
+++ b/src/Headers/fileloc.h
@@ -83,8 +83,8 @@ extern bool fileloc_isExternal (/*@sef@*/ fileloc p_f) /*@*/;
 # define fileloc_isExternal(f) \
      (fileloc_isDefined(f) && ((f)->kind == FL_EXTERNAL))
 
-extern /*@falsenull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ;
-extern /*@truenull@*/ bool fileloc_isUndefined (/*@null@*/ fileloc p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ;
+extern /*@nullwhentrue@*/ bool fileloc_isUndefined (/*@null@*/ fileloc p_f) /*@*/ ;
 extern bool fileloc_isInvalid (/*@sef@*/ /*@null@*/ fileloc p_f) /*@*/ ;
 
 /*@constant null fileloc fileloc_undefined; @*/
@@ -120,7 +120,7 @@ extern void fileloc_setColumnUndefined (/*@sef@*/ fileloc p_f) /*@modifies p_f@*
   (fileloc_isDefined(f) ? (f)->column = UNKNOWN_COLUMN : UNKNOWN_COLUMN)
 # endif
 
-extern /*@falsenull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f);
+extern /*@falsewhennull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f);
 # define fileloc_isValid(f) \
   (fileloc_isDefined(f) && ((f)->lineno >= 0))
 

diff --git a/src/Headers/filelocList.h b/src/Headers/filelocList.h
index 3a734372662736fe7af48f7dcbb7c39f47d62207..c14eb65d8a3d433c04fc43e93a2c97909cd79358 100644 (file)
--- a/src/Headers/filelocList.h
+++ b/src/Headers/filelocList.h
@@ -12,9 +12,9 @@ abst_typedef /*@null@*/ struct
   /*@reldef@*/ /*@relnull@*/ o_fileloc *elements;
 } *filelocList ;
 
-extern /*@unused@*/ /*@truenull@*/ bool
+extern /*@unused@*/ /*@nullwhentrue@*/ bool
   filelocList_isUndefined (filelocList p_f) /*@*/ ;
-extern /*@falsenull@*/ bool filelocList_isDefined (filelocList p_f);
+extern /*@falsewhennull@*/ bool filelocList_isDefined (filelocList p_f);
 
 /*@constant null filelocList filelocList_undefined; @*/
 # define filelocList_undefined (NULL)

diff --git a/src/Headers/filelocStack.h b/src/Headers/filelocStack.h
index 067bce85dac3c36ab56dcee477d5bf7bbd1957e2..278b47c30b2c7fd9d171a0fdaf1cff82d5c4e184 100644 (file)
--- a/src/Headers/filelocStack.h
+++ b/src/Headers/filelocStack.h
@@ -15,7 +15,7 @@ abst_typedef /*@null@*/ struct
 /*@constant null filelocStack filelocStack_undefined; @*/
 # define filelocStack_undefined (NULL)
 
-extern /*@falsenull@*/ bool filelocStack_isDefined (filelocStack p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool filelocStack_isDefined (filelocStack p_f) /*@*/ ;
 # define filelocStack_isDefined(f)   ((f) != filelocStack_undefined)
 
 extern int filelocStack_size (/*@sef@*/ filelocStack p_s) /*@*/ ;

diff --git a/src/Headers/flagSpec.h b/src/Headers/flagSpec.h
index fc35025c604c0f34202744f7af4686f74e596fc5..493f1dfd47e5bb9c7c7dfb4e329ed99ffb785299 100644 (file)
--- a/src/Headers/flagSpec.h
+++ b/src/Headers/flagSpec.h
@@ -28,7 +28,7 @@ struct s_flagSpec
 /*@constant null flagSpec flagSpec_undefined; @*/
 # define flagSpec_undefined  ((flagSpec) NULL)
 
-extern /*@falsenull@*/ bool flagSpec_isDefined (flagSpec p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool flagSpec_isDefined (flagSpec p_e) /*@*/ ;
 # define flagSpec_isDefined(e)        ((e) != flagSpec_undefined)
 
 extern /*@only@*/ flagSpec flagSpec_createPlain (/*@only@*/ cstring) ;

diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h
index cb57af88311c30f772836fea37f396478af7dd0e..681491473fa9d6ed4336719ab9bdf6a4df17fee5 100644 (file)
--- a/src/Headers/functionClause.h
+++ b/src/Headers/functionClause.h
@@ -36,7 +36,7 @@ struct s_functionClause {
 /*@constant null functionClause functionClause_undefined; @*/
 # define functionClause_undefined NULL
 
-extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
+extern /*@falsewhennull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
 # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined)
 
 extern bool functionClause_isGlobals (functionClause) /*@*/ ;
@@ -59,7 +59,7 @@ extern bool functionClause_isEnsures (functionClause) /*@*/ ;
 extern bool functionClause_isRequires (functionClause) /*@*/ ;
 # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
 
-extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
+extern /*@nullwhentrue@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
 # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
 
 extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ;

diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h
index 829e96c39b2d147e4ebe4602cb72e492cc477cb7..471949bc3b05b033ee971a924cab8f41e561ad90 100644 (file)
--- a/src/Headers/functionClauseList.h
+++ b/src/Headers/functionClauseList.h
@@ -19,16 +19,16 @@ struct s_functionClauseList
 /*@constant null functionClauseList functionClauseList_undefined;@*/
 # define functionClauseList_undefined ((functionClauseList) NULL)
 
-extern /*@falsenull@*/ bool functionClauseList_isDefined (functionClauseList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool functionClauseList_isDefined (functionClauseList p_s) /*@*/ ;
 # define functionClauseList_isDefined(s)   ((s) != functionClauseList_undefined)
 
-extern /*@truenull@*/ bool functionClauseList_isUndefined (functionClauseList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool functionClauseList_isUndefined (functionClauseList p_s) /*@*/ ;
 # define functionClauseList_isUndefined(s)   ((s) == functionClauseList_undefined)
 
 extern int functionClauseList_size (/*@sef@*/ functionClauseList) /*@*/ ;
 # define functionClauseList_size(s) (functionClauseList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool functionClauseList_empty (/*@sef@*/ functionClauseList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool functionClauseList_empty (/*@sef@*/ functionClauseList) /*@*/ ;
 # define functionClauseList_empty(s) (functionClauseList_size(s) == 0)
 
 extern cstring functionClauseList_unparseSep (functionClauseList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/functionConstraint.h b/src/Headers/functionConstraint.h
index 0a5dcf47763e577d6a183bfe4282901cc1df8325..83035c631e23a0759e7d15211cbc15cc77eb60b3 100644 (file)
--- a/src/Headers/functionConstraint.h
+++ b/src/Headers/functionConstraint.h
@@ -26,10 +26,10 @@ struct s_functionConstraint {
 /*@constant null functionConstraint functionConstraint_undefined; @*/
 # define functionConstraint_undefined    ((functionConstraint) NULL)
 
-extern /*@falsenull@*/ bool functionConstraint_isDefined (functionConstraint) /*@*/ ;
+extern /*@falsewhennull@*/ bool functionConstraint_isDefined (functionConstraint) /*@*/ ;
 # define functionConstraint_isDefined(p_info) ((p_info) != NULL)
 
-extern /*@truenull@*/ bool functionConstraint_isUndefined (functionConstraint) /*@*/ ;
+extern /*@nullwhentrue@*/ bool functionConstraint_isUndefined (functionConstraint) /*@*/ ;
 # define functionConstraint_isUndefined(p_info) ((p_info) == NULL)
 
 extern functionConstraint functionConstraint_copy (functionConstraint) /*@*/ ;

diff --git a/src/Headers/genericTable.h b/src/Headers/genericTable.h
index 042c1cd4b685d6c2c179d4744f5dfa364f27baed..a405041d9ef3b153065d6528e056a7be32f81c9b 100644 (file)
--- a/src/Headers/genericTable.h
+++ b/src/Headers/genericTable.h
@@ -44,10 +44,10 @@ struct s_genericTable
 /*@constant null genericTable genericTable_undefined; @*/
 # define genericTable_undefined      ((genericTable) NULL)
 
-extern /*@falsenull@*/ bool genericTable_isDefined(genericTable) /*@*/ ;
+extern /*@falsewhennull@*/ bool genericTable_isDefined(genericTable) /*@*/ ;
 # define genericTable_isDefined(p_h) ((p_h) != genericTable_undefined)
 
-extern /*@truenull@*/ /*@unused@*/ bool genericTable_isUndefined(genericTable) /*@*/ ;
+extern /*@nullwhentrue@*/ /*@unused@*/ bool genericTable_isUndefined(genericTable) /*@*/ ;
 # define genericTable_isUndefined(p_h) ((p_h) == genericTable_undefined)
 
 extern /*@only@*/ genericTable genericTable_create (int p_size);

diff --git a/src/Headers/globSet.h b/src/Headers/globSet.h
index c0f2588b5e3f414f3c9346bb2022c64f5f6cfc4a..21d2d3347fe5b219a8a1f2e1c7748f628f0d39ba 100644 (file)
--- a/src/Headers/globSet.h
+++ b/src/Headers/globSet.h
@@ -50,8 +50,8 @@ extern void globSet_clear (globSet p_g);
 /*@constant null globSet globSet_undefined;@*/
 # define globSet_undefined sRefSet_undefined
 
-extern /*@falsenull@*/ bool globSet_isDefined (/*@null@*/ globSet p_s) /*@*/ ;
-extern /*@truenull@*/ bool globSet_isUndefined (/*@null@*/ globSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool globSet_isDefined (/*@null@*/ globSet p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool globSet_isUndefined (/*@null@*/ globSet p_s) /*@*/ ;
 
 # define globSet_isDefined(s)   (sRefSet_isDefined (s))
 # define globSet_isUndefined(s) (sRefSet_isUndefined (s))

diff --git a/src/Headers/guardSet.h b/src/Headers/guardSet.h
index 6952cd46db265bee62d4723a2eedbf417e78de3d..302dd64577d72ba1e109ca7af70252864ce51588 100644 (file)
--- a/src/Headers/guardSet.h
+++ b/src/Headers/guardSet.h
@@ -20,11 +20,11 @@
 /*@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, /*@exposed@*/ sRef p_s);

diff --git a/src/Headers/idDecl.h b/src/Headers/idDecl.h
index 9f39203d0443f58e1411bc7a5628d3a060b21faa..98749b559bc3e0c4e8d8eacbb77958cf06ca8db0 100644 (file)
--- a/src/Headers/idDecl.h
+++ b/src/Headers/idDecl.h
@@ -20,7 +20,7 @@ struct s_idDecl
 /*@constant null idDecl idDecl_undefined; @*/
 # define idDecl_undefined ((idDecl) NULL)
 
-extern /*@falsenull@*/ bool idDecl_isDefined (idDecl p_t) /*@*/ ;
+extern /*@falsewhennull@*/ bool idDecl_isDefined (idDecl p_t) /*@*/ ;
 # define idDecl_isDefined(t) ((t) != idDecl_undefined)
 
 extern void idDecl_free (/*@only@*/ idDecl p_t);

diff --git a/src/Headers/inputStream.h b/src/Headers/inputStream.h
index fa8c5c403b77934a18d2a8ba23acac2a9c167e8d..d50c82640defbb4fbb8915d989f9a4aedfafd9d2 100644 (file)
--- a/src/Headers/inputStream.h
+++ b/src/Headers/inputStream.h
@@ -26,8 +26,8 @@ struct s_inputStream {
 
 /* in forwardTypes.h: abst_typedef null struct _inputStream *inputStream; */
 
-extern /*@falsenull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
-extern /*@truenull@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ;
+extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ;
 
 /*@constant null inputStream inputStream_undefined; @*/
 # define inputStream_undefined      ((inputStream) NULL)

diff --git a/src/Headers/lclTypeSpecNode.h b/src/Headers/lclTypeSpecNode.h
index d3ba22b892e20f418921ebc4971ce0f8af45731b..b3e8841de900aecda0e677e1c9b67ecc7eb8f080 100644 (file)
--- a/src/Headers/lclTypeSpecNode.h
+++ b/src/Headers/lclTypeSpecNode.h
@@ -33,7 +33,7 @@ struct s_lclTypeSpecNode {
 /*@constant null lclTypeSpecNode lclTypeSpecNode_undefined; @*/
 # define lclTypeSpecNode_undefined ((lclTypeSpecNode) 0)
 
-extern /*@falsenull@*/ bool lclTypeSpecNode_isDefined (lclTypeSpecNode p_x) /*@*/ ;
+extern /*@falsewhennull@*/ bool lclTypeSpecNode_isDefined (lclTypeSpecNode p_x) /*@*/ ;
 # define lclTypeSpecNode_isDefined(x) ((x) != lclTypeSpecNode_undefined)
 
 extern /*@null@*/ /*@only@*/ lclTypeSpecNode

diff --git a/src/Headers/lslOpSet.h b/src/Headers/lslOpSet.h
index 5e92eadfcbedf6247fc046162eafa48978e65b3a..ccc2b0cf7b420a6b93c5ed848c54a1633c1f6f4c 100644 (file)
--- a/src/Headers/lslOpSet.h
+++ b/src/Headers/lslOpSet.h
@@ -30,7 +30,7 @@ abst_typedef /*@null@*/ struct
 /*@constant null lslOpSet lslOpSet_undefined;@*/
 # define lslOpSet_undefined ((lslOpSet) NULL)
 
-extern /*@falsenull@*/ bool lslOpSet_isDefined (lslOpSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool lslOpSet_isDefined (lslOpSet p_s) /*@*/ ;
 # define lslOpSet_isDefined(s) ((s) != lslOpSet_undefined)
 
 extern /*@unused@*/ int 

diff --git a/src/Headers/lsymbolSet.h b/src/Headers/lsymbolSet.h
index a380c34797503dfb0a2c92317d4cdd6a808e3bae..2b657e06775793b2cb472a360105a45cba98bee9 100644 (file)
--- a/src/Headers/lsymbolSet.h
+++ b/src/Headers/lsymbolSet.h
@@ -22,7 +22,7 @@ abst_typedef /*@null@*/ struct
 /*@constant null lsymbolSet lsymbolSet_undefined; @*/
 # define lsymbolSet_undefined (NULL)
 
-extern /*@falsenull@*/ bool lsymbolSet_isDefined (lsymbolSet p_l) /*@*/ ;
+extern /*@falsewhennull@*/ bool lsymbolSet_isDefined (lsymbolSet p_l) /*@*/ ;
 # define lsymbolSet_isDefined(l) ((l) != lsymbolSet_undefined)
  
 /*@iter lsymbolSet_elements (sef lsymbolSet s, yield lsymbol el); @*/

diff --git a/src/Headers/ltoken.h b/src/Headers/ltoken.h
index 685a1bd0fd54f2f9a85e6ee76d884b20f4ca1304..ef9f3f3da07e38c176b1c18d209714f5321f321d 100644 (file)
--- a/src/Headers/ltoken.h
+++ b/src/Headers/ltoken.h
@@ -46,10 +46,10 @@ typedef /*@only@*/ ltoken o_ltoken;
 /*@constant null ltoken ltoken_undefined; @*/
 # define ltoken_undefined  ((ltoken)NULL)
 
-extern /*@falsenull@*/ bool ltoken_isValid (ltoken p_tok);
+extern /*@falsewhennull@*/ bool ltoken_isValid (ltoken p_tok);
 # define ltoken_isValid(t) ((t) != ltoken_undefined)
 
-extern /*@truenull@*/ bool ltoken_isUndefined (ltoken p_tok);
+extern /*@nullwhentrue@*/ bool ltoken_isUndefined (ltoken p_tok);
 # define ltoken_isUndefined(t) ((t) == ltoken_undefined)
 
 extern bool ltoken_isStateDefined (/*@sef@*/ ltoken p_tok) /*@*/ ;

diff --git a/src/Headers/ltokenList.h b/src/Headers/ltokenList.h
index 3bcf1ef08b6e1cb835cf3586e4b1bcde7979480f..72b4957ae2b94ef2c79214c2037819fd7913fc71 100644 (file)
--- a/src/Headers/ltokenList.h
+++ b/src/Headers/ltokenList.h
@@ -32,10 +32,10 @@ abst_typedef /*@null@*/ struct
 /*@constant null ltokenList ltokenList_undefined;@*/
 # define ltokenList_undefined NULL
 
-extern /*@falsenull@*/ bool ltokenList_isDefined (ltokenList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool ltokenList_isDefined (ltokenList p_s) /*@*/ ;
 # define ltokenList_isDefined(s) ((s) != ltokenList_undefined)
 
-extern /*@truenull@*/ bool ltokenList_isUndefined (ltokenList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool ltokenList_isUndefined (ltokenList p_s) /*@*/ ;
 # define ltokenList_isUndefined(s) ((s) == ltokenList_undefined)
 
 extern int ltokenList_size (/*@sef@*/ ltokenList p_s) /*@*/ ;

diff --git a/src/Headers/messageLog.h b/src/Headers/messageLog.h
index 5221959280d7f56faa0225de00a698023c3e26f5..beaf2055d92a8c6150bb1dc99b418e18cefdfd06 100644 (file)
--- a/src/Headers/messageLog.h
+++ b/src/Headers/messageLog.h
@@ -28,7 +28,7 @@ abst_typedef /*@null@*/ struct
 /*@constant null messageLog messageLog_undefined; @*/
 # define messageLog_undefined ((messageLog)0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool 
+extern /*@unused@*/ /*@falsewhennull@*/ bool 
   messageLog_isDefined (messageLog p_s) /*@*/ ;
 # define messageLog_isDefined(c) ((c) != messageLog_undefined)
 

diff --git a/src/Headers/metaStateConstraintList.h b/src/Headers/metaStateConstraintList.h
index e62047b746d303f0df21dad8283b2419b67c08d7..c50201e9fb5c17de21c3866bb5e89b4ea1c754a8 100644 (file)
--- a/src/Headers/metaStateConstraintList.h
+++ b/src/Headers/metaStateConstraintList.h
@@ -14,9 +14,9 @@ struct s_metaStateConstraintList
   /*@reldef@*/ /*@relnull@*/ b_metaStateConstraint *elements;
 } ;
 
-extern /*@unused@*/ /*@truenull@*/ bool
+extern /*@unused@*/ /*@nullwhentrue@*/ bool
   metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ;
-extern /*@falsenull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ;
 
 /*@constant null metaStateConstraintList metaStateConstraintList_undefined; @*/
 # define metaStateConstraintList_undefined (NULL)

diff --git a/src/Headers/metaStateExpression.h b/src/Headers/metaStateExpression.h
index 805d68cde1f83feda2f5e83ac891fa0fa9c0c881..7980c4556f9b5f83bcd840781b3481062add203f 100644 (file)
--- a/src/Headers/metaStateExpression.h
+++ b/src/Headers/metaStateExpression.h
@@ -17,10 +17,10 @@ struct s_metaStateExpression {
 /*@constant null metaStateExpression metaStateExpression_undefined; @*/
 # define metaStateExpression_undefined    ((metaStateExpression) NULL)
 
-extern /*@falsenull@*/ bool metaStateExpression_isDefined (metaStateExpression) /*@*/ ;
+extern /*@falsewhennull@*/ bool metaStateExpression_isDefined (metaStateExpression) /*@*/ ;
 # define metaStateExpression_isDefined(p_info) ((p_info) != NULL)
 
-extern /*@truenull@*/ bool metaStateExpression_isUndefined (metaStateExpression) /*@*/ ;
+extern /*@nullwhentrue@*/ bool metaStateExpression_isUndefined (metaStateExpression) /*@*/ ;
 # define metaStateExpression_isUndefined(p_info) ((p_info) == NULL)
 
 extern /*@notnull@*/ metaStateExpression

diff --git a/src/Headers/metaStateInfo.h b/src/Headers/metaStateInfo.h
index 1919764d5d3e06883280ae765994e0743b430a1d..0aa412181f685fdbc70ab5d0765720dfe5c76ac7 100644 (file)
--- a/src/Headers/metaStateInfo.h
+++ b/src/Headers/metaStateInfo.h
@@ -41,10 +41,10 @@ struct s_metaStateInfo {
 /*@constant null metaStateInfo metaStateInfo_undefined; @*/
 # define metaStateInfo_undefined    ((metaStateInfo) NULL)
 
-extern /*@falsenull@*/ bool metaStateInfo_isDefined (metaStateInfo) /*@*/ ;
+extern /*@falsewhennull@*/ bool metaStateInfo_isDefined (metaStateInfo) /*@*/ ;
 # define metaStateInfo_isDefined(p_info) ((p_info) != NULL)
 
-extern /*@truenull@*/ bool metaStateInfo_isUndefined (metaStateInfo) /*@*/ ;
+extern /*@nullwhentrue@*/ bool metaStateInfo_isUndefined (metaStateInfo) /*@*/ ;
 # define metaStateInfo_isUndefined(p_info) ((p_info) == NULL)
 
 extern /*@notnull@*/ metaStateInfo 

diff --git a/src/Headers/metaStateTable.h b/src/Headers/metaStateTable.h
index 9420cd91b83f9095e2db12bdb10c90ade9197908..b1a504189010f6fe31c14df652e35d77a8379a92 100644 (file)
--- a/src/Headers/metaStateTable.h
+++ b/src/Headers/metaStateTable.h
@@ -23,10 +23,10 @@
 /*@constant null metaStateTable metaStateTable_undefined; @*/
 # define metaStateTable_undefined genericTable_undefined
 
-extern /*@falsenull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ;
+extern /*@falsewhennull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ;
 # define metaStateTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
-extern /*@truenull@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ;
+extern /*@nullwhentrue@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ;
 # define metaStateTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
 /*@constant int DEFAULT_MSTABLE_SIZE@*/

diff --git a/src/Headers/misc.h b/src/Headers/misc.h
index 8db1da73ccbeb8a38e4cfb31e033e0932448af20..726263de2d3aefe630b8871fd31683dbca76dc17 100644 (file)
--- a/src/Headers/misc.h
+++ b/src/Headers/misc.h
@@ -57,10 +57,10 @@ extern int mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
 # define mstring_length(s) \
   (((s) != NULL) ? size_toInt (strlen (s)) : 0)
 
-extern /*@falsenull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
 # define mstring_isDefined(s) ((s) != NULL)
 
-extern /*@truenull@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ;
 # define mstring_isEmpty(s) (mstring_length(s) == 0)
 
 extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ;

diff --git a/src/Headers/mtAnnotationList.h b/src/Headers/mtAnnotationList.h
index 43632e47de7053c0e89f97237bef99e08e7ff258..c99a8f9d657862741c4f1e7eefc47922550d7aa8 100644 (file)
--- a/src/Headers/mtAnnotationList.h
+++ b/src/Headers/mtAnnotationList.h
@@ -16,13 +16,13 @@ struct s_mtAnnotationList
 /*@constant null mtAnnotationList mtAnnotationList_undefined;@*/
 # define mtAnnotationList_undefined ((mtAnnotationList) NULL)
 
-extern /*@falsenull@*/ bool mtAnnotationList_isDefined (mtAnnotationList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtAnnotationList_isDefined (mtAnnotationList p_s) /*@*/ ;
 # define mtAnnotationList_isDefined(s)   ((s) != mtAnnotationList_undefined)
 
 extern int mtAnnotationList_size (/*@sef@*/ mtAnnotationList) /*@*/ ;
 # define mtAnnotationList_size(s) (mtAnnotationList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool mtAnnotationList_empty (/*@sef@*/ mtAnnotationList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool mtAnnotationList_empty (/*@sef@*/ mtAnnotationList) /*@*/ ;
 # define mtAnnotationList_empty(s) (mtAnnotationList_size(s) == 0)
 
 extern cstring mtAnnotationList_unparseSep (mtAnnotationList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/mtContextNode.h b/src/Headers/mtContextNode.h
index 567d2a9211b74097ed1fb830d05de4aa59eba03a..6797aad55a1e2fdd49a494b2e61e3edaaf5e3884 100644 (file)
--- a/src/Headers/mtContextNode.h
+++ b/src/Headers/mtContextNode.h
@@ -28,7 +28,7 @@ struct s_mtContextNode {
 /*@constant null mtContextNode mtContextNode_undefined@*/
 # define mtContextNode_undefined ((mtContextNode) 0)
 
-extern /*@falsenull@*/ bool mtContextNode_isDefined (mtContextNode p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtContextNode_isDefined (mtContextNode p_s) /*@*/ ;
 # define mtContextNode_isDefined(s) ((s) != mtContextNode_undefined)
 
 extern cstring mtContextNode_unparse (mtContextNode) /*@*/ ;

diff --git a/src/Headers/mtDeclarationPiece.h b/src/Headers/mtDeclarationPiece.h
index 9cfb196232eb2ddcec11879f5b2071cad2201be6..d9ae03f0ded07349286846f261cf7016a2cec0cf 100644 (file)
--- a/src/Headers/mtDeclarationPiece.h
+++ b/src/Headers/mtDeclarationPiece.h
@@ -28,10 +28,10 @@ struct s_mtDeclarationPiece {
 /*@constant null mtDeclarationPiece mtDeclarationPiece_undefined; @*/
 # define mtDeclarationPiece_undefined NULL
 
-extern /*@falsenull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ;
 # define mtDeclarationPiece_isDefined(p_h) ((p_h) != mtDeclarationPiece_undefined)
 
-extern /*@truenull@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ;
+extern /*@nullwhentrue@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ;
 # define mtDeclarationPiece_isUndefined(p_h) ((p_h) == mtDeclarationPiece_undefined)
 
 extern mtDeclarationPiece mtDeclarationPiece_createContext (/*@only@*/ mtContextNode) /*@*/ ;

diff --git a/src/Headers/mtDeclarationPieces.h b/src/Headers/mtDeclarationPieces.h
index 26be9cdc0b9394f62daeb6338d14be4d6cb7e5f2..a6b51318bf5570ca28dfb7e811bab7bfb8b2b359 100644 (file)
--- a/src/Headers/mtDeclarationPieces.h
+++ b/src/Headers/mtDeclarationPieces.h
@@ -20,10 +20,10 @@ struct s_mtDeclarationPieces {
 /*@constant null mtDeclarationPieces mtDeclarationPieces_undefined; @*/
 # define mtDeclarationPieces_undefined NULL
 
-extern /*@falsenull@*/ bool mtDeclarationPieces_isDefined(mtDeclarationPieces) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtDeclarationPieces_isDefined(mtDeclarationPieces) /*@*/ ;
 # define mtDeclarationPieces_isDefined(p_h) ((p_h) != mtDeclarationPieces_undefined)
 
-extern /*@truenull@*/ bool mtDeclarationPieces_isUndefined(mtDeclarationPieces) /*@*/ ;
+extern /*@nullwhentrue@*/ bool mtDeclarationPieces_isUndefined(mtDeclarationPieces) /*@*/ ;
 # define mtDeclarationPieces_isUndefined(p_h) ((p_h) == mtDeclarationPieces_undefined)
 
 extern mtDeclarationPieces mtDeclarationPieces_create (void) /*@*/ ;

diff --git a/src/Headers/mtDefaultsDeclList.h b/src/Headers/mtDefaultsDeclList.h
index 3fb005bbf4c3ed94c596824275ac9d0465887b5f..fcff2767f7b5ab84b949b1be5cb24a1c79853419 100644 (file)
--- a/src/Headers/mtDefaultsDeclList.h
+++ b/src/Headers/mtDefaultsDeclList.h
@@ -19,13 +19,13 @@ struct s_mtDefaultsDeclList
 /*@constant null mtDefaultsDeclList mtDefaultsDeclList_undefined;@*/
 # define mtDefaultsDeclList_undefined ((mtDefaultsDeclList) NULL)
 
-extern /*@falsenull@*/ bool mtDefaultsDeclList_isDefined (mtDefaultsDeclList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtDefaultsDeclList_isDefined (mtDefaultsDeclList p_s) /*@*/ ;
 # define mtDefaultsDeclList_isDefined(s)   ((s) != mtDefaultsDeclList_undefined)
 
 extern int mtDefaultsDeclList_size (/*@sef@*/ mtDefaultsDeclList) /*@*/ ;
 # define mtDefaultsDeclList_size(s) (mtDefaultsDeclList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool mtDefaultsDeclList_empty (/*@sef@*/ mtDefaultsDeclList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool mtDefaultsDeclList_empty (/*@sef@*/ mtDefaultsDeclList) /*@*/ ;
 # define mtDefaultsDeclList_empty(s) (mtDefaultsDeclList_size(s) == 0)
 
 extern cstring mtDefaultsDeclList_unparseSep (mtDefaultsDeclList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/mtLoseReferenceList.h b/src/Headers/mtLoseReferenceList.h
index c58b9c26b8ddbdc9b64f291e0278498256064071..a0ef72b29c90331583908e1b20c639b8fc9f7796 100644 (file)
--- a/src/Headers/mtLoseReferenceList.h
+++ b/src/Headers/mtLoseReferenceList.h
@@ -19,13 +19,13 @@ struct s_mtLoseReferenceList
 /*@constant null mtLoseReferenceList mtLoseReferenceList_undefined;@*/
 # define mtLoseReferenceList_undefined ((mtLoseReferenceList) NULL)
 
-extern /*@falsenull@*/ bool mtLoseReferenceList_isDefined (mtLoseReferenceList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtLoseReferenceList_isDefined (mtLoseReferenceList p_s) /*@*/ ;
 # define mtLoseReferenceList_isDefined(s)   ((s) != mtLoseReferenceList_undefined)
 
 extern int mtLoseReferenceList_size (/*@sef@*/ mtLoseReferenceList) /*@*/ ;
 # define mtLoseReferenceList_size(s) (mtLoseReferenceList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool mtLoseReferenceList_empty (/*@sef@*/ mtLoseReferenceList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool mtLoseReferenceList_empty (/*@sef@*/ mtLoseReferenceList) /*@*/ ;
 # define mtLoseReferenceList_empty(s) (mtLoseReferenceList_size(s) == 0)
 
 extern cstring mtLoseReferenceList_unparseSep (mtLoseReferenceList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/mtMergeClauseList.h b/src/Headers/mtMergeClauseList.h
index 30c7c1bee29c7b63cb454220e72ae6b05b570948..12f5d5b57ae7178e937c7283e51fa26b4e436587 100644 (file)
--- a/src/Headers/mtMergeClauseList.h
+++ b/src/Headers/mtMergeClauseList.h
@@ -19,13 +19,13 @@ struct s_mtMergeClauseList
 /*@constant null mtMergeClauseList mtMergeClauseList_undefined;@*/
 # define mtMergeClauseList_undefined ((mtMergeClauseList) NULL)
 
-extern /*@falsenull@*/ bool mtMergeClauseList_isDefined (mtMergeClauseList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtMergeClauseList_isDefined (mtMergeClauseList p_s) /*@*/ ;
 # define mtMergeClauseList_isDefined(s)   ((s) != mtMergeClauseList_undefined)
 
 extern int mtMergeClauseList_size (/*@sef@*/ mtMergeClauseList) /*@*/ ;
 # define mtMergeClauseList_size(s) (mtMergeClauseList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool mtMergeClauseList_empty (/*@sef@*/ mtMergeClauseList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool mtMergeClauseList_empty (/*@sef@*/ mtMergeClauseList) /*@*/ ;
 # define mtMergeClauseList_empty(s) (mtMergeClauseList_size(s) == 0)
 
 extern cstring mtMergeClauseList_unparseSep (mtMergeClauseList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/mtTransferClauseList.h b/src/Headers/mtTransferClauseList.h
index 12bd70da7fef84813e64b3ce8fa7a7385fefa098..15b327c8f23c82f2552b63c21b2eee2056c75788 100644 (file)
--- a/src/Headers/mtTransferClauseList.h
+++ b/src/Headers/mtTransferClauseList.h
@@ -19,13 +19,13 @@ struct s_mtTransferClauseList
 /*@constant null mtTransferClauseList mtTransferClauseList_undefined;@*/
 # define mtTransferClauseList_undefined ((mtTransferClauseList) NULL)
 
-extern /*@falsenull@*/ bool mtTransferClauseList_isDefined (mtTransferClauseList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool mtTransferClauseList_isDefined (mtTransferClauseList p_s) /*@*/ ;
 # define mtTransferClauseList_isDefined(s)   ((s) != mtTransferClauseList_undefined)
 
 extern int mtTransferClauseList_size (/*@sef@*/ mtTransferClauseList) /*@*/ ;
 # define mtTransferClauseList_size(s) (mtTransferClauseList_isDefined (s) ? (s)->nelements : 0)
 
-extern /*@unused@*/ /*@falsenull@*/ bool mtTransferClauseList_empty (/*@sef@*/ mtTransferClauseList) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool mtTransferClauseList_empty (/*@sef@*/ mtTransferClauseList) /*@*/ ;
 # define mtTransferClauseList_empty(s) (mtTransferClauseList_size(s) == 0)
 
 extern cstring mtTransferClauseList_unparseSep (mtTransferClauseList p_s, cstring p_sep) /*@*/ ;

diff --git a/src/Headers/multiVal.h b/src/Headers/multiVal.h
index ff80e0c425ff13ce85aaee4c53264b7cdd161d56..71b88c2f43020f9151926311d3f5aeaefb9639c2 100644 (file)
--- a/src/Headers/multiVal.h
+++ b/src/Headers/multiVal.h
@@ -19,9 +19,9 @@ typedef /*@null@*/ struct
   } value;
 } *multiVal;
 
-extern /*@falsenull@*/ bool multiVal_isDefined (multiVal p_m) /*@*/ ;
-extern /*@truenull@*/ bool multiVal_isUndefined (multiVal p_m) /*@*/ ;
-extern /*@truenull@*/ bool multiVal_isUnknown (multiVal p_m) /*@*/ ;
+extern /*@falsewhennull@*/ bool multiVal_isDefined (multiVal p_m) /*@*/ ;
+extern /*@nullwhentrue@*/ bool multiVal_isUndefined (multiVal p_m) /*@*/ ;
+extern /*@nullwhentrue@*/ bool multiVal_isUnknown (multiVal p_m) /*@*/ ;
 
 extern multiVal multiVal_add (multiVal p_m1, multiVal p_m2) /*@*/ ;
 extern multiVal multiVal_subtract (multiVal p_m1, multiVal p_m2) /*@*/ ;
@@ -50,10 +50,10 @@ extern void multiVal_free (/*@only@*/ multiVal p_m);
 
 extern multiVal multiVal_invert (multiVal p_m) /*@*/ ;
 
-extern /*@falsenull@*/ bool multiVal_isInt (multiVal p_m) /*@*/ ;
-extern /*@falsenull@*/ bool multiVal_isChar (multiVal p_m) /*@*/ ;
-extern /*@falsenull@*/ bool multiVal_isDouble (multiVal p_m) /*@*/ ;
-extern /*@falsenull@*/ bool multiVal_isString (multiVal p_m) /*@*/ ;
+extern /*@falsewhennull@*/ bool multiVal_isInt (multiVal p_m) /*@*/ ;
+extern /*@falsewhennull@*/ bool multiVal_isChar (multiVal p_m) /*@*/ ;
+extern /*@falsewhennull@*/ bool multiVal_isDouble (multiVal p_m) /*@*/ ;
+extern /*@falsewhennull@*/ bool multiVal_isString (multiVal p_m) /*@*/ ;
 
 extern /*@only@*/ multiVal multiVal_undump (char **p_s) /*@modifies *p_s;@*/ ;
 extern /*@only@*/ cstring multiVal_dump (multiVal p_m) /*@*/ ;

diff --git a/src/Headers/pairNodeList.h b/src/Headers/pairNodeList.h
index a904d9b76719dab9671ca2b9c7be453600777762..c66009209a9b0aa4c7dc6d0fa608745e199147e9 100644 (file)
--- a/src/Headers/pairNodeList.h
+++ b/src/Headers/pairNodeList.h
@@ -24,7 +24,7 @@ abst_typedef /*@null@*/ struct
 
 # define end_pairNodeList_elements }}
 
-extern /*@falsenull@*/ bool pairNodeList_isDefined (pairNodeList p_p) /*@*/ ;
+extern /*@falsewhennull@*/ bool pairNodeList_isDefined (pairNodeList p_p) /*@*/ ;
 
 /*@constant null pairNodeList pairNodeList_undefined; @*/
 # define pairNodeList_undefined    ((pairNodeList)0)

diff --git a/src/Headers/paramNodeList.h b/src/Headers/paramNodeList.h
index 97ba6e023cc174c913b51f3eb208b37a8e9037df..1fe049a6564e09444a68f5c6ee9feffdb5389572 100644 (file)
--- a/src/Headers/paramNodeList.h
+++ b/src/Headers/paramNodeList.h
@@ -33,7 +33,7 @@ extern bool paramNodeList_empty (/*@sef@*/ paramNodeList p_s);
 
 extern /*@only@*/ paramNodeList paramNodeList_single (/*@keep@*/ paramNode p_p);
 
-extern /*@falsenull@*/ bool paramNodeList_isDefined (paramNodeList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool paramNodeList_isDefined (paramNodeList p_s) /*@*/ ;
 # define paramNodeList_isDefined(s) ((s) != (paramNodeList)0)
 extern /*@only@*/ paramNodeList paramNodeList_new (void);
 
@@ -52,7 +52,7 @@ extern /*@only@*/ cstring paramNodeList_unparseComments (paramNodeList p_s);
 /*@constant null paramNodeList paramNodeList_undefined; @*/
 # define paramNodeList_undefined ((paramNodeList) 0)
 
-extern /*@truenull@*/ bool paramNodeList_isNull (/*@null@*/ paramNodeList p_p);
+extern /*@nullwhentrue@*/ bool paramNodeList_isNull (/*@null@*/ paramNodeList p_p);
 
 # define paramNodeList_isNull(p) ((p) == paramNodeList_undefined)
 

diff --git a/src/Headers/qtype.h b/src/Headers/qtype.h
index 88275f66f389152060ab9905fd0524a83e157c9c..d4682dbb89be7d78cd66b6e7b8d0d1769c1d9bc2 100644 (file)
--- a/src/Headers/qtype.h
+++ b/src/Headers/qtype.h
@@ -21,10 +21,10 @@ abst_typedef /*@null@*/ struct
 /*@constant null qtype qtype_undefined;@*/
 # define qtype_undefined ((qtype) NULL)
 
-extern /*@truenull@*/ bool qtype_isUndefined (qtype p_q);
+extern /*@nullwhentrue@*/ bool qtype_isUndefined (qtype p_q);
 # define qtype_isUndefined(q) ((q) == qtype_undefined)
 
-extern /*@falsenull@*/ bool qtype_isDefined (qtype p_q);
+extern /*@falsewhennull@*/ bool qtype_isDefined (qtype p_q);
 # define qtype_isDefined(q)   ((q) != qtype_undefined)
 
 extern ctype qtype_getType (/*@sef@*/ qtype p_q);

diff --git a/src/Headers/qualList.h b/src/Headers/qualList.h
index 8e80eb701d70acede7a695cd44585f805971af77..38bab620afa5d2b5d3875d0998f3149b951a023e 100644 (file)
--- a/src/Headers/qualList.h
+++ b/src/Headers/qualList.h
@@ -12,8 +12,8 @@ abst_typedef /*@null@*/ struct
   /*@reldef@*/ /*@relnull@*/ qual *elements;
 } *qualList ;
 
-extern /*@falsenull@*/ bool qualList_isDefined (qualList p_s);
-extern /*@unused@*/ /*@truenull@*/ bool qualList_isUndefined (qualList p_s);
+extern /*@falsewhennull@*/ bool qualList_isDefined (qualList p_s);
+extern /*@unused@*/ /*@nullwhentrue@*/ bool qualList_isUndefined (qualList p_s);
 
 /*@constant null qualList qualList_undefined; @*/
 # define qualList_undefined ((qualList) NULL)

diff --git a/src/Headers/rangeTable.h b/src/Headers/rangeTable.h
index 829df887c7edc9a040a0df3204b17daffcae92b4..c46e30793a77083e0a8c29f54d0576fb8d5d2170 100644 (file)
--- a/src/Headers/rangeTable.h
+++ b/src/Headers/rangeTable.h
@@ -43,10 +43,10 @@ struct _rangeTable
     
 } ; 
 
-extern /*@unused@*/ /*@truenull@*/ bool rangeTable_isUndefined (rangeTable p_s);
-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@unused@*/ /*@nullwhentrue@*/ bool rangeTable_isUndefined (rangeTable p_s);
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 
   rangeTable_isEmpty (/*@sef@*/ rangeTable p_s);
-extern /*@falsenull@*/ bool rangeTable_isDefined (rangeTable p_s);
+extern /*@falsewhennull@*/ bool rangeTable_isDefined (rangeTable p_s);
 
 /*@constant null rangeTable rangeTable_undefined; @*/
 # define rangeTable_undefined      ((rangeTable) NULL)

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index 2381642249d9e3f06d77cb2bc64fb1b96bf3d3e9..77033ac9c88d3064d3ea23f26fe7bce23a08c9f4 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -150,8 +150,8 @@ extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc)
 extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
 extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
 
-extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
 
 /*@constant null sRef sRef_undefined; @*/
 # define sRef_undefined    ((sRef) NULL)
@@ -165,11 +165,11 @@ extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
 
 extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
                                                      
-extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
 
 extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
 # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
@@ -202,7 +202,7 @@ extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
 
-extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isConj(s)           (sRef_isValid(s) && (s)->kind == SK_CONJ)
 
 extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
@@ -234,7 +234,7 @@ extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
 
 extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
 
-extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
 
 extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
@@ -255,13 +255,13 @@ extern ctype sRef_getType (sRef p_s) /*@*/ ;
 
 extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ;
 
-extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; 
-extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; 
+extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
 
 extern void sRef_setType (sRef p_s, ctype p_t);
 extern void sRef_setTypeFull (sRef p_s, ctype p_t);
@@ -323,7 +323,7 @@ extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t)
 extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t);
 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ;
 
-extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ;
 
 extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ;
 
@@ -428,18 +428,18 @@ extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ;
 
 extern int sRef_getScope (sRef p_s) /*@*/ ;
 extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ;
 
 /* must be real function (passed as function param) */
-extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isDead (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ;
 extern bool sRef_isStateLive (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
-extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ;
 extern bool sRef_isUnuseable (sRef p_s) /*@*/ ;
 
 extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t) 
@@ -450,7 +450,7 @@ extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t)
 
 extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ;
 
-extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ;
 
 extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isUndefGlob(s) \
@@ -489,7 +489,7 @@ extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ;
                                  || ((s)->defstate == SS_RELDEF) \
                                  || ((s)->defstate == SS_PARTIAL)))
 
-extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isPdefined(s) \
   ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED))
 
@@ -499,15 +499,15 @@ extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isStateUnknown(s) \
   ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN))
 
-extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isRefCounted(s) \
   ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED))
 
-extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isNewRef(s) \
   ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF))
 
-extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isKillRef(s) \
   ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF))
 

diff --git a/src/Headers/sRefList.h b/src/Headers/sRefList.h
index 4bb32c39641185b4ae417246e7949b57702b612c..cf776230989cb2e7e204b4369e2a36ac7f1d69ce 100644 (file)
--- a/src/Headers/sRefList.h
+++ b/src/Headers/sRefList.h
@@ -29,9 +29,9 @@ struct s_sRefList
 
 extern int sRefList_size (sRefList p_s) /*@*/ ;
 
-extern /*@truenull@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ;
-extern /*@unused@*/ /*@falsenull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ;
 
 # define sRefList_isEmpty(s) (sRefList_size(s) == 0)
 

diff --git a/src/Headers/sRefSet.h b/src/Headers/sRefSet.h
index d70d5aa9e5ed7f2dd66ba024686157ddfac795db..969fa0d7102a2009f651a5c9cdf44d45774b75c0 100644 (file)
--- a/src/Headers/sRefSet.h
+++ b/src/Headers/sRefSet.h
@@ -52,9 +52,9 @@ struct s_sRefSet
 /*@constant null sRefSet sRefSet_undefined;@*/
 # define sRefSet_undefined ((sRefSet) 0)
 
-extern /*@truenull@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ;
-extern /*@truenull@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ;
 
 # define sRefSet_isUndefined(s) ((s) == sRefSet_undefined)
 # define sRefSet_isDefined(s)   ((s) != sRefSet_undefined)

diff --git a/src/Headers/sRefSetList.h b/src/Headers/sRefSetList.h
index e90e9cf690f309c4e917311ac8560cd58693f74a..4b2dd04a8e1cf4b1eef0d48817437f3594331adb 100644 (file)
--- a/src/Headers/sRefSetList.h
+++ b/src/Headers/sRefSetList.h
@@ -27,10 +27,10 @@ abst_typedef /*@null@*/ struct
 /*@constant null sRefSetList sRefSetList_undefined; @*/
 # define sRefSetList_undefined  ((sRefSetList) NULL)
 
-extern /*@falsenull@*/ bool sRefSetList_isDefined (sRefSetList p_s);
+extern /*@falsewhennull@*/ bool sRefSetList_isDefined (sRefSetList p_s);
 # define sRefSetList_isDefined(s) ((s) != sRefSetList_undefined)
 
-extern /*@unused@*/ /*@truenull@*/ bool sRefSetList_isUndefined (sRefSetList p_s);
+extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefSetList_isUndefined (sRefSetList p_s);
 # define sRefSetList_isUndefined(s) ((s) == sRefSetList_undefined)
 
 extern sRefSetList 

diff --git a/src/Headers/sRefTable.h b/src/Headers/sRefTable.h
index 6ed695f4606bc042791a8539ec86cea0b488faea..24853e1ed004ab4aa511c64ebd6a96abfe0aa92d 100644 (file)
--- a/src/Headers/sRefTable.h
+++ b/src/Headers/sRefTable.h
@@ -27,9 +27,9 @@ abst_typedef /*@null@*/ struct
 /*@constant null sRefTable sRefTable_undefined; @*/
 # define sRefTable_undefined ((sRefTable) NULL)
 
-extern /*@truenull@*/ bool sRefTable_isNull (sRefTable p_s) /*@*/ ;
-extern /*@truenull@*/ bool sRefTable_isEmpty (/*@sef@*/ sRefTable p_s) /*@*/ ;
-extern /*@unused@*/ /*@falsenull@*/ bool 
+extern /*@nullwhentrue@*/ bool sRefTable_isNull (sRefTable p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRefTable_isEmpty (/*@sef@*/ sRefTable p_s) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool 
   sRefTable_isDefined (sRefTable p_s) /*@*/ ;
 
 # define sRefTable_isNull(s) ((s) == sRefTable_undefined)

diff --git a/src/Headers/sigNodeSet.h b/src/Headers/sigNodeSet.h
index e576d71511838778bb5fa08a36ce31420f2216cf..ac1bec6d89aab1e9b7ec1687082694e1d763b2d7 100644 (file)
--- a/src/Headers/sigNodeSet.h
+++ b/src/Headers/sigNodeSet.h
@@ -33,11 +33,11 @@ abst_typedef /*@null@*/ struct
 /*@constant null sigNodeSet sigNodeSet_undefined; @*/
 # define sigNodeSet_undefined ((sigNodeSet) 0)
 
-extern /*@falsenull@*/ bool sigNodeSet_isDefined (sigNodeSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sigNodeSet_isDefined (sigNodeSet p_s) /*@*/ ;
 # define sigNodeSet_isDefined(s) \
   ((s) != sigNodeSet_undefined)
 
-extern /*@truenull@*/ bool sigNodeSet_isUndefined (sigNodeSet p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sigNodeSet_isUndefined (sigNodeSet p_s) /*@*/ ;
 # define sigNodeSet_isUndefined(s) \
   ((s) == sigNodeSet_undefined)
 

diff --git a/src/Headers/sortSet.h b/src/Headers/sortSet.h
index 7639dbc3d01d4c4a9e20c0cba701ba51634022f6..a1f5d303c7e1f0d214c8cc66f7f88444d47a0681 100644 (file)
--- a/src/Headers/sortSet.h
+++ b/src/Headers/sortSet.h
@@ -29,7 +29,7 @@ abst_typedef /*@null@*/ struct
 
 /*@constant null sortSet sortSet_undefined; @*/
 # define sortSet_undefined ((sortSet) NULL)
-extern /*@falsenull@*/ bool sortSet_isDefined (sortSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sortSet_isDefined (sortSet p_s) /*@*/ ;
 # define sortSet_isDefined(s) ((s) != sortSet_undefined)
 
 extern int sortSet_size (/*@sef@*/ sortSet p_s);

diff --git a/src/Headers/stateClauseList.h b/src/Headers/stateClauseList.h
index 79b33487f1f760543c06982406b994a12338aa4f..5049d115c517e37ff2634368fe5dbe9335444a4f 100644 (file)
--- a/src/Headers/stateClauseList.h
+++ b/src/Headers/stateClauseList.h
@@ -22,10 +22,10 @@ extern void stateClauseList_checkAll (uentry p_ue)
 /*@constant null stateClauseList stateClauseList_undefined@*/
 # define stateClauseList_undefined ((stateClauseList) 0)
 
-extern /*@falsenull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ;
 # define stateClauseList_isDefined(s) ((s) != stateClauseList_undefined)
 
-extern /*@truenull@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ;
 # define stateClauseList_isUndefined(s) ((s) == stateClauseList_undefined)
 
 extern /*@unused@*/ int 

diff --git a/src/Headers/stateInfo.h b/src/Headers/stateInfo.h
index a5d0fcbd880807091e19ffc8c80f798a6b60f38d..2e2d2237e11ca3e5c9aad4ba95686efd052907e9 100644 (file)
--- a/src/Headers/stateInfo.h
+++ b/src/Headers/stateInfo.h
@@ -19,7 +19,7 @@ typedef /*@null@*/ struct
 /*@constant null stateInfo stateInfo_undefined@*/
 # define stateInfo_undefined (NULL)
 
-extern /*@falsenull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ;
 # define stateInfo_isDefined(p_s) ((p_s) != stateInfo_undefined)
 
 extern void stateInfo_free (/*@only@*/ stateInfo p_a);

diff --git a/src/Headers/stateValue.h b/src/Headers/stateValue.h
index d535074273312f86b5a69042a70f3ab26ce5d0c5..5f8700dbb39d7cad23c69343babffdf2b9761605 100644 (file)
--- a/src/Headers/stateValue.h
+++ b/src/Headers/stateValue.h
@@ -27,10 +27,10 @@ extern /*@notnull@*/ stateValue stateValue_createImplicit (int p_value, /*@only@
 /*@constant null stateValue stateValue_undefined@*/
 # define stateValue_undefined (NULL)
 
-extern /*@truenull@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
+extern /*@nullwhentrue@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
 # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined)
 
-extern /*@falsenull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
+extern /*@falsewhennull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
 # define stateValue_isDefined(p_s) ((p_s) != NULL)
 
 extern bool stateValue_isImplicit (stateValue) /*@*/ ;

diff --git a/src/Headers/symtable.h b/src/Headers/symtable.h
index aed7481b43fff24c36e63b3c08e9c3057ccf4aa1..e9a72a932f44d5f3a899e509899c200f251e67bb 100644 (file)
--- a/src/Headers/symtable.h
+++ b/src/Headers/symtable.h
@@ -133,16 +133,16 @@ typedef struct {
 
 typedef struct s_symtableStruct *symtable;
 
-extern /*@falsenull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti);
+extern /*@falsewhennull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti);
 # define typeInfo_exists(ti)  ((ti) != NULL)
 
-extern /*@falsenull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi);
+extern /*@falsewhennull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi);
 # define varInfo_exists(vi)   ((vi) != NULL)
 
-extern /*@falsenull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi);
+extern /*@falsewhennull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi);
 # define tagInfo_exists(ti)   ((ti) != NULL)
 
-extern /*@falsenull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi);
+extern /*@falsewhennull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi);
 # define opInfo_exists(oi)    ((oi) != NULL)
 
 extern /*@only@*/ symtable symtable_new (void) /*@*/ ;

diff --git a/src/Headers/termNode.h b/src/Headers/termNode.h
index 35b4541b642732d14053f1a28bcf49a9bc63bc0c..219a4fc0ef30cd52dd9f1531211ac3b8ee3f36e8 100644 (file)
--- a/src/Headers/termNode.h
+++ b/src/Headers/termNode.h
@@ -23,7 +23,7 @@ struct s_termNode
   /*@reldef@*/ lclTypeSpecNode sizeofField; /* only for TRM_SIZEOF */
 } ;
 
-extern /*@falsenull@*/ bool termNode_isDefined (/*@null@*/ termNode p_t) /*@*/ ;
+extern /*@falsewhennull@*/ bool termNode_isDefined (/*@null@*/ termNode p_t) /*@*/ ;
 # define termNode_isDefined(t) ((t) != NULL)
 
 extern termNode termNode_copySafe (termNode p_t) /*@*/ ;

diff --git a/src/Headers/termNodeList.h b/src/Headers/termNodeList.h
index 0adeec9cad43db14248201217bbe14036174fd22..6efc415dcb82c388b590fb4fdd3d97a466ee6df6 100644 (file)
--- a/src/Headers/termNodeList.h
+++ b/src/Headers/termNodeList.h
@@ -32,7 +32,7 @@ extern int termNodeList_size (/*@sef@*/ termNodeList);
 extern bool termNodeList_empty (/*@sef@*/ termNodeList);
 # define termNodeList_empty(s) (termNodeList_size(s) == 0)
 
-extern /*@falsenull@*/ bool termNodeList_isDefined (termNodeList p_t);
+extern /*@falsewhennull@*/ bool termNodeList_isDefined (termNodeList p_t);
 # define termNodeList_isDefined(s) ((s) != (termNodeList) 0)
 
 extern /*@only@*/ termNodeList termNodeList_new(void);

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index 1d1f4fc691dced8dc46a057658ee8afbc5eb0e77..00eef1fc9c7d8e61889b0577d42194bb5b252780 100644 (file)
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -169,11 +169,11 @@ struct s_uentry
 ** uentry_isDefined).
 */
 
-extern /*@truenull@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) 
+extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) 
    /*@*/ ;
-extern /*@truenull@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) 
+extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) 
    /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) 
+extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) 
    /*@*/ ;
 
 /*@constant null uentry uentry_undefined; @*/
@@ -193,51 +193,51 @@ extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ;
 extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ;
 extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
+extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e);
 # define uentry_isLset(e) \
   (uentry_isValid(e) && (e)->lset)
 
-extern /*@falsenull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
+extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e);
 # define uentry_isUsed(e)         (uentry_isValid(e) && (e)->used)
 
-extern /*@unused@*/ /*@falsenull@*/ bool 
+extern /*@unused@*/ /*@falsewhennull@*/ bool 
   uentry_isAbstractType (uentry p_e) /*@*/ ;
 # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e))
 
-extern /*@falsenull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isConstant(e) \
   (uentry_isValid(e) && ekind_isConst ((e)->ukind))
 
-extern /*@falsenull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isEitherConstant(e) \
   (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind)))
 
-extern /*@falsenull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isEnumConstant(e) \
   (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind))
 
-extern /*@falsenull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isExternal(c) \
   (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c)))
 
-extern /*@falsenull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isExtern(c) \
   (uentry_isValid(c) && (c)->storageclass == SCEXTERN)
 
 extern bool uentry_isForward (uentry p_e) /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isFunction(e) \
   (uentry_isValid(e) && ekind_isFunction ((e)->ukind))
 
-extern /*@falsenull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isPriv(e) \
   (uentry_isValid(e) && (e)->isPrivate)
 
-extern /*@falsenull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ;
 # define uentry_isStatic(c) \
   (uentry_isValid(c) && (c)->storageclass == SCSTATIC)
 
@@ -284,49 +284,49 @@ extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ;
 extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ;
 extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ;
 extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue)
    /*@uses p_ue->ukind@*/
    /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) 
+extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) 
    /*@uses p_e->whereDeclared@*/ /*@*/ ;
 
 extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ;
 extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ;
 
 extern void uentry_showWhereDefined (uentry p_spec);
-extern /*@falsenull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue)
    /*@uses p_ue->ukind@*/ /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) 
+extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) 
    /*@uses p_u->ukind, p_u->info@*/ 
    /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ;
+extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) 
+extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) 
    /*@uses p_ue->ukind@*/ /*@*/ ;
-extern /*@falsenull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
+extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue)
    /*@uses p_ue->ukind@*/ /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) 
+extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) 
    /*@uses p_e->ukind@*/
    /*@*/ ;
 
-extern /*@falsenull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) 
+extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) 
    /*@uses p_e->ukind@*/
    /*@*/ ;
 

diff --git a/src/Headers/uentryList.h b/src/Headers/uentryList.h
index 7aae25b331e0184da7e9445494e3b6ad62c45ccb..c736e16d5e631734dfb6af2180eee501362eadc1 100644 (file)
--- a/src/Headers/uentryList.h
+++ b/src/Headers/uentryList.h
@@ -34,10 +34,10 @@ extern /*@only@*/ uentryList uentryList_makeMissingParams (void);
 
 # define uentryList_makeMissingParams() uentryList_missingParams
 
-extern /*@truenull@*/ bool uentryList_isMissingParams (uentryList p_s) /*@*/ ;
-extern /*@truenull@*/ bool uentryList_isUndefined (uentryList p_s) /*@*/ ;
-extern /*@unused@*/ /*@truenull@*/ bool uentryList_isEmpty (uentryList p_s) /*@*/ ;
-extern /*@unused@*/ /*@falsenull@*/ bool uentryList_isDefined (uentryList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool uentryList_isMissingParams (uentryList p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool uentryList_isUndefined (uentryList p_s) /*@*/ ;
+extern /*@unused@*/ /*@nullwhentrue@*/ bool uentryList_isEmpty (uentryList p_s) /*@*/ ;
+extern /*@unused@*/ /*@falsewhennull@*/ bool uentryList_isDefined (uentryList p_s) /*@*/ ;
 
 # define uentryList_isEmpty(s) (uentryList_size(s) == 0)
 

diff --git a/src/Headers/usymIdSet.h b/src/Headers/usymIdSet.h
index 4ec5cdf683e4ae8ae2bc1f7fa80ce2e901f5470a..2e2b115573cb13d8284ccd0b117a6b57a5501a52 100644 (file)
--- a/src/Headers/usymIdSet.h
+++ b/src/Headers/usymIdSet.h
@@ -43,10 +43,10 @@ extern /*@only@*/ usymIdSet
 /*@constant null usymIdSet usymIdSet_undefined; @*/
 # define usymIdSet_undefined    ((usymIdSet) NULL)
 
-extern /*@falsenull@*/ bool usymIdSet_isDefined (usymIdSet p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool usymIdSet_isDefined (usymIdSet p_s) /*@*/ ;
 # define usymIdSet_isDefined(s) ((s) != usymIdSet_undefined)
 
-extern /*@truenull@*/ bool usymIdSet_isUndefined (usymIdSet p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool usymIdSet_isUndefined (usymIdSet p_s) /*@*/ ;
 # define usymIdSet_isUndefined(s) ((s) == usymIdSet_undefined)
 
 /*@iter usymIdSet_elements (sef usymIdSet u, yield usymId el); @*/ 

diff --git a/src/Headers/usymtab-branch.h b/src/Headers/usymtab-branch.h
index 2eae7a32ff41275e31ba1d38a38a9c3d585bfe30..94016430d6c9d8d87353a09fe9f2eb0bf0e65735 100644 (file)
--- a/src/Headers/usymtab-branch.h
+++ b/src/Headers/usymtab-branch.h
@@ -414,7 +414,7 @@ extern void usymtab_popCaseBranch (void)
 /*@constant int functionScope;@*/
 # define functionScope 3
 
-extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
 
 /*@constant null usymtab usymtab_undefined; @*/
 # define usymtab_undefined ((usymtab)NULL)

diff --git a/src/Headers/usymtab.h b/src/Headers/usymtab.h
index 09840ae72c2cc860c3723c668224fdfabe197cde..e6a5ada4e1d819dab7bae7160019bd67f5db2984 100644 (file)
--- a/src/Headers/usymtab.h
+++ b/src/Headers/usymtab.h
@@ -394,7 +394,7 @@ extern void usymtab_popCaseBranch (void)
 /*@constant int functionScope;@*/
 # define functionScope 3
 
-extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
+extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
 
 /*@constant null usymtab usymtab_undefined; @*/
 # define usymtab_undefined ((usymtab)NULL)

diff --git a/src/Headers/valueMatrix.h b/src/Headers/valueMatrix.h
index d7efcbe2ec1b165dbc36d68a9d2ce3b6f64e745e..aff4e6149358a38d31aeac76103e2f604822babf 100644 (file)
--- a/src/Headers/valueMatrix.h
+++ b/src/Headers/valueMatrix.h
@@ -21,10 +21,10 @@ abst_typedef genericTable valueMatrix;
 /*@constant null valueMatrix valueMatrix_undefined; @*/
 # define valueMatrix_undefined genericTable_undefined
 
-extern /*@falsenull@*/ bool valueMatrix_isDefined(valueMatrix) /*@*/ ;
+extern /*@falsewhennull@*/ bool valueMatrix_isDefined(valueMatrix) /*@*/ ;
 # define valueMatrix_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
-extern /*@truenull@*/ bool valueMatrix_isUndefined(valueMatrix) /*@*/ ;
+extern /*@nullwhentrue@*/ bool valueMatrix_isUndefined(valueMatrix) /*@*/ ;
 # define valueMatrix_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
 extern /*@only@*/ valueMatrix valueMatrix_create(int p_size);

diff --git a/src/Headers/valueTable.h b/src/Headers/valueTable.h
index 6860e3c5f983c5d53c5e302c9be1623c8992a590..f18892010eaeb24bf91709b5c5e34f7a32a3ff53 100644 (file)
--- a/src/Headers/valueTable.h
+++ b/src/Headers/valueTable.h
@@ -17,10 +17,10 @@
 /*@constant null valueTable valueTable_undefined; @*/
 # define valueTable_undefined genericTable_undefined
 
-extern /*@falsenull@*/ bool valueTable_isDefined(valueTable) /*@*/ ;
+extern /*@falsewhennull@*/ bool valueTable_isDefined(valueTable) /*@*/ ;
 # define valueTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h)))
 
-extern /*@truenull@*/ bool valueTable_isUndefined(valueTable) /*@*/ ;
+extern /*@nullwhentrue@*/ bool valueTable_isUndefined(valueTable) /*@*/ ;
 # define valueTable_isUndefined(p_h) (genericTable_isUndefined ((genericTable) (p_h)))
 
 extern /*@only@*/ valueTable valueTable_create(int p_size);

diff --git a/src/Headers/warnClause.h b/src/Headers/warnClause.h
index 4f41bb00aac83c9b4ba418d5b82974c605552846..bb3d1d9fb98df64f9f4b8d33a04abf3003818254 100644 (file)
--- a/src/Headers/warnClause.h
+++ b/src/Headers/warnClause.h
@@ -20,8 +20,8 @@ struct s_warnClause
 /*@constant null warnClause warnClause_undefined; @*/
 # define warnClause_undefined    ((warnClause) NULL)
 
-extern /*@falsenull@*/ bool warnClause_isDefined (/*@null@*/ warnClause p_f) /*@*/ ;
-extern /*@truenull@*/ bool warnClause_isUndefined (/*@null@*/ warnClause p_f) /*@*/ ;
+extern /*@falsewhennull@*/ bool warnClause_isDefined (/*@null@*/ warnClause p_f) /*@*/ ;
+extern /*@nullwhentrue@*/ bool warnClause_isUndefined (/*@null@*/ warnClause p_f) /*@*/ ;
 
 # define warnClause_isDefined(f)   ((f) != warnClause_undefined)
 # define warnClause_isUndefined(f) ((f) == warnClause_undefined)
@@ -37,7 +37,7 @@ extern /*@observer@*/ flagSpec warnClause_getFlag (warnClause p_w) /*@*/ ;
 extern /*@only@*/ cstring warnClause_dump (warnClause p_wc) /*@*/ ;
 extern /*@only@*/ warnClause warnClause_undump (char **p_s) /*@modifies p_s@*/ ;
 
-extern /*@falsenull@*/ bool warnClause_hasMessage (warnClause p_w) /*@*/ ;
+extern /*@falsewhennull@*/ bool warnClause_hasMessage (warnClause p_w) /*@*/ ;
 
 extern /*@observer@*/ cstring warnClause_getMessage (warnClause p_w) /*@*/ ;
 extern /*@only@*/ cstring warnClause_unparse (warnClause p_w) /*@*/ ;

diff --git a/src/cscanner.l b/src/cscanner.l
index aac8219e238b29d532cd64b81340d445b2f11f15..d20f4f3f722e33ef3c8a6fa540e8cbc4b79db470 100644 (file)
--- a/src/cscanner.l
+++ b/src/cscanner.l
@@ -288,6 +288,8 @@ L\"(\\.|[^\\"])*\"([ \t\n]*\"(\\.|[^\\"])*\")* { RETURN_EXPR (processWideString
 "isnull"                { return (processSpec (QISNULL)); } 
 "truenull"              { return (processSpec (QTRUENULL)); } 
 "falsenull"             { return (processSpec (QFALSENULL)); } 
+"nullwhentrue"          { return (processSpec (QTRUENULL)); } 
+"nullwhenfalse"             { return (processSpec (QFALSENULL)); } 
 "relnull"               { return (processSpec (QRELNULL)); }
 "reldef"                { return (processSpec (QRELDEF)); }
 "exposed"               { return (processSpec (QEXPOSED)); }
@@ -632,6 +634,8 @@ struct skeyword s_keytable[] = {
   { "special", QSPECIAL } ,
   { "truenull", QTRUENULL } ,
   { "falsenull", QFALSENULL } ,
+  { "nullwhentrue", QTRUENULL } ,
+  { "falsewhennull", QFALSENULL } ,
   { "keep", QKEEP } ,
   { "kept", QKEPT } ,
   { "notnull", QNOTNULL } ,

diff --git a/src/cstringTable.c b/src/cstringTable.c
index 1fb90c128b9f953ba8443cc2875d1051702cdba0..0f5f970eba00a17c07ce1490361ac73ea21fced1 100644 (file)
--- a/src/cstringTable.c
+++ b/src/cstringTable.c
@@ -44,7 +44,7 @@ static void
 cstringTable_addEntry (/*@notnull@*/ cstringTable p_h, /*@only@*/ hentry p_e) 
      /*@modifies p_h@*/ ;
 
-static /*@truenull@*/ bool hbucket_isNull (/*@null@*/ hbucket h) 
+static /*@nullwhentrue@*/ bool hbucket_isNull (/*@null@*/ hbucket h) 
 { 
   return (h == hbucket_undefined); 
 }

diff --git a/src/genericTable.c b/src/genericTable.c
index 35274e9123f3a622d8ae5a6fd9b59d524b436420..e2c00d770fdabf28d42b61c332418431ba883e52 100644 (file)
--- a/src/genericTable.c
+++ b/src/genericTable.c
@@ -35,7 +35,7 @@
 /*@constant null ghbucket ghbucket_undefined; @*/
 # define ghbucket_undefined 0
 
-static /*@truenull@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h) 
+static /*@nullwhentrue@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h) 
 { 
   return (h == ghbucket_undefined); 
 }

diff --git a/src/llmain.c b/src/llmain.c
index 1d9c6b544f77ccde96134120b2a75cd7361058c2..66d911521470a2c1ea8d523f086cdde19907f75c 100644 (file)
--- a/src/llmain.c
+++ b/src/llmain.c
@@ -1928,12 +1928,12 @@ printAnnotations (void)
   llmsglit ("");
   llmsglit ("Null State:");
   llmsglit ("   /*@null@*/ - possibly null pointer");
-  llmsglit ("   /*@notnull@*/ - non-null pointer");
+  llmsglit ("   /*@notnull@*/ - definitely non-null pointer");
   llmsglit ("   /*@relnull@*/ - relax null checking");
   llmsglit ("");
   llmsglit ("Null Predicates:");
-  llmsglit ("   /*@truenull@*/ - if result is TRUE, first parameter is NULL");
-  llmsglit ("   /*@falsenull@*/ - if result is TRUE, first parameter is not NULL");
+  llmsglit ("   /*@nullwhentrue@*/ - if result is TRUE, first parameter is NULL");
+  llmsglit ("   /*@falsewhennull@*/ - if result is TRUE, first parameter is not NULL");
   llmsglit ("");
   llmsglit ("Execution:");
   llmsglit ("   /*@noreturn@*/ - function never returns");

diff --git a/src/sRef.c b/src/sRef.c
index 060c91b75a7ef0eef97417719e5f1c0f4fda5a5b..9a18b79b21bb86e22d628371d1832784be9422d1 100644 (file)
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -588,14 +588,14 @@ static bool
          && (fileloc_isDefined (s->aliasinfo->loc)));
 }
 
-static /*@falsenull@*/ bool
+static /*@falsewhennull@*/ bool
 sRef_hasStateInfoLoc (sRef s)
 {
   return (sRef_isValid (s) && (s->definfo != NULL) 
          && (fileloc_isDefined (s->definfo->loc)));
 }
 
-static /*@falsenull@*/ bool
+static /*@falsewhennull@*/ bool
 sRef_hasExpInfoLoc (sRef s)
 {
   return (sRef_isValid (s) 

diff --git a/src/usymtab.c b/src/usymtab.c
index 43ab21ec6a4d474bce8bbcfb7ed0d1926d614870..d9073d5481b40c9118e3359a9601feb1d2ba5876 100644 (file)
--- a/src/usymtab.c
+++ b/src/usymtab.c
@@ -193,7 +193,7 @@ static void clearFunctionTypes (void)
   uentryList_clear (functypes);
 }
 
-static /*@falsenull@*/ bool usymtab_isBranch (usymtab u)
+static /*@falsewhennull@*/ bool usymtab_isBranch (usymtab u)
 {
   return (usymtab_isDefined (u) && 
          (u->kind == US_TBRANCH || u->kind == US_FBRANCH