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
 
    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
 
    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
 
    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;
 } ; 
 
   /*@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);
   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)
 
 /*@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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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
 
 /*@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)))
 
 # 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@*/
 # 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)
 
 
 # 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)
 
 # 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)
 
 /*@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)
 
 # 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);
 
 
 /*@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);
 
 
 /*@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);
 
                                                /*@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);
 
 
 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;
 
   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) ;
 # 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)
 
 
 # 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)
 
 # 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 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);
 # 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)
 
 /*@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))
 
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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 /*@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; @*/
   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)
 
 /*@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)
 
 # 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)
 
 # 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)
 
 # 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)
 
 /*@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)
 
 # 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)
 
   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;
 
 
 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); @*/
 # 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)
 
 /*@constant null fileTable fileTable_undefined; @*/
 # define fileTable_undefined ((fileTable) NULL)
 

-extern /*@unused@*/ /*@truenull@*/ bool 
+extern /*@unused@*/ /*@nullwhentrue@*/ bool 

   fileTable_isUndefined (/*@null@*/ fileTable p_f) /*@*/ ;
   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)
   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))
 
 # 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; @*/
 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
 
   (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))
 
 # 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 ;
 
   /*@reldef@*/ /*@relnull@*/ o_fileloc *elements;
 } *filelocList ;
 

-extern /*@unused@*/ /*@truenull@*/ bool
+extern /*@unused@*/ /*@nullwhentrue@*/ bool

   filelocList_isUndefined (filelocList p_f) /*@*/ ;
   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)
 
 /*@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)
 
 /*@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) /*@*/ ;
 # 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)
 
 /*@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) ;
 # 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
 
 /*@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) /*@*/ ;
 # 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 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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);
 # 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
 
 /*@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))
 
 # 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)
 
 /*@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)
 
   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);
 
 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)
 
 /*@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);
 # 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; */
 
 
 /* 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)
 
 /*@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)
 
 /*@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
 # 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)
 
 /*@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 
 # 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)
 
 /*@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); @*/
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
   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;
 } ;
 
   /*@reldef@*/ /*@relnull@*/ b_metaStateConstraint *elements;
 } ;
 

-extern /*@unused@*/ /*@truenull@*/ bool
+extern /*@unused@*/ /*@nullwhentrue@*/ bool

   metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ;
   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)
 
 /*@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)
 
 /*@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)
 
 # 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
 # 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)
 
 /*@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)
 
 # 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 
 # 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
 
 /*@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)))
 
 # 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@*/
 # 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)
 
 # 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)
 
 # 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;@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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) /*@*/ ;
 # 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
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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;
 
   } 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) /*@*/ ;
 
 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 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) /*@*/ ;
 
 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 }}
 
 
 # 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)
 
 /*@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 /*@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);
 
 # 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)
 
 /*@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)
 
 
 # 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)
 
 /*@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)
 
 # 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);
 # 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 ;
 
   /*@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)
 
 /*@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);
   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)
 
 /*@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 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)
 
 /*@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 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))
 
 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 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);
 # 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 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) /*@*/ ;
 # 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 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);
 
 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 /*@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) /*@*/ ;
 
 
 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 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 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 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) 
 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 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) \
 
 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)))
 
                                  || ((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))
 
 # 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))
 
 # 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))
 
 # 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))
 
 # 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))
 
 # 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 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)
 
 
 # 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)
 
 /*@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)
 
 # 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)
 
 /*@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)
 
 # 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 
 # 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)
 
 /*@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)
   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)
 
 /*@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)
 
 # 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)
 
 # 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)
 
 /*@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);
 # 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)
 
 /*@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)
 
 # 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 
 # 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)
 
 /*@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);
 # 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)
 
 /*@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)
 
 # 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) /*@*/ ;
 # 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;
 
 
 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)
 
 # 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)
 
 # 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)
 
 # 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) /*@*/ ;
 # 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 */
 } ;
 
   /*@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) /*@*/ ;
 # 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 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);
 # 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).
 */
 
 ** 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; @*/
    /*@*/ ;
 
 /*@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 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)
 
 # 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)
 
 # 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))
 
   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))
 
 # 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)))
 
 # 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))
 
 # 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)))
 
 # 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) /*@*/ ;
 
 # 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))
 
 # 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)
 
 # 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)
 
 # 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 /*@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@*/
    /*@*/ ;
    /*@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);
    /*@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@*/ /*@*/ ;
    /*@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@*/ 
    /*@*/ ;
 
    /*@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@*/ /*@*/ ;
    /*@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@*/ /*@*/ ;
 
    /*@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@*/
    /*@*/ ;
 
    /*@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@*/
    /*@*/ ;
 
    /*@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
 
 
 # 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)
 
 
 # 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)
 
 /*@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)
 
 # 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); @*/ 
 # 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
 
 /*@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)
 
 /*@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
 
 /*@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)
 
 /*@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
 
 /*@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)))
 
 # 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);
 # 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
 
 /*@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)))
 
 # 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);
 # 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)
 
 /*@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)
 
 # 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 /*@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) /*@*/ ;
 
 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)); } 
 "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)); }
 "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 } ,
   { "special", QSPECIAL } ,
   { "truenull", QTRUENULL } ,
   { "falsenull", QFALSENULL } ,

+  { "nullwhentrue", QTRUENULL } ,
+  { "falsewhennull", QFALSENULL } ,

   { "keep", QKEEP } ,
   { "kept", QKEPT } ,
   { "notnull", QNOTNULL } ,
   { "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@*/ ;
 
 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); 
 }
 { 
   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
 
 /*@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); 
 }
 { 
   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 ("");
   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 ("   /*@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");
   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)));
 }
 
          && (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)));
 }
 
 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) 
 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);
 }
 
   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
 {
   return (usymtab_isDefined (u) && 
          (u->kind == US_TBRANCH || u->kind == US_FBRANCH