From 0e41eb0e650b136b06564fd3c32ea5a1d16c68c8 Mon Sep 17 00:00:00 2001 From: evans1629 Date: Sat, 5 Jan 2002 04:16:14 +0000 Subject: [PATCH] Renamed truenull nullwhentrue and falsenull falsewhennull --- README | 4 +- src/Headers/aliasTable.h | 6 +-- src/Headers/annotationInfo.h | 4 +- src/Headers/annotationTable.h | 4 +- src/Headers/constraint.h | 6 +-- src/Headers/constraintExpr.h | 10 ++-- src/Headers/constraintExprData.h | 2 +- src/Headers/constraintList.h | 6 +-- src/Headers/constraintList2.h | 2 +- src/Headers/cstring.h | 8 +-- src/Headers/cstringList.h | 4 +- src/Headers/cstringSList.h | 4 +- src/Headers/cstringTable.h | 4 +- src/Headers/ctypeList.h | 4 +- src/Headers/exprNode.h | 8 +-- src/Headers/fcnNodeList.h | 4 +- src/Headers/fileIdList.h | 2 +- src/Headers/fileTable.h | 4 +- src/Headers/fileloc.h | 6 +-- src/Headers/filelocList.h | 4 +- src/Headers/filelocStack.h | 2 +- src/Headers/flagSpec.h | 2 +- src/Headers/functionClause.h | 4 +- src/Headers/functionClauseList.h | 6 +-- src/Headers/functionConstraint.h | 4 +- src/Headers/genericTable.h | 4 +- src/Headers/globSet.h | 4 +- src/Headers/guardSet.h | 4 +- src/Headers/idDecl.h | 2 +- src/Headers/inputStream.h | 4 +- src/Headers/lclTypeSpecNode.h | 2 +- src/Headers/lslOpSet.h | 2 +- src/Headers/lsymbolSet.h | 2 +- src/Headers/ltoken.h | 4 +- src/Headers/ltokenList.h | 4 +- src/Headers/messageLog.h | 2 +- src/Headers/metaStateConstraintList.h | 4 +- src/Headers/metaStateExpression.h | 4 +- src/Headers/metaStateInfo.h | 4 +- src/Headers/metaStateTable.h | 4 +- src/Headers/misc.h | 4 +- src/Headers/mtAnnotationList.h | 4 +- src/Headers/mtContextNode.h | 2 +- src/Headers/mtDeclarationPiece.h | 4 +- src/Headers/mtDeclarationPieces.h | 4 +- src/Headers/mtDefaultsDeclList.h | 4 +- src/Headers/mtLoseReferenceList.h | 4 +- src/Headers/mtMergeClauseList.h | 4 +- src/Headers/mtTransferClauseList.h | 4 +- src/Headers/multiVal.h | 14 ++--- src/Headers/pairNodeList.h | 2 +- src/Headers/paramNodeList.h | 4 +- src/Headers/qtype.h | 4 +- src/Headers/qualList.h | 4 +- src/Headers/rangeTable.h | 6 +-- src/Headers/sRef.h | 56 ++++++++++---------- src/Headers/sRefList.h | 6 +-- src/Headers/sRefSet.h | 6 +-- src/Headers/sRefSetList.h | 4 +- src/Headers/sRefTable.h | 6 +-- src/Headers/sigNodeSet.h | 4 +- src/Headers/sortSet.h | 2 +- src/Headers/stateClauseList.h | 4 +- src/Headers/stateInfo.h | 2 +- src/Headers/stateValue.h | 4 +- src/Headers/symtable.h | 8 +-- src/Headers/termNode.h | 2 +- src/Headers/termNodeList.h | 2 +- src/Headers/uentry.h | 76 +++++++++++++-------------- src/Headers/uentryList.h | 8 +-- src/Headers/usymIdSet.h | 4 +- src/Headers/usymtab-branch.h | 2 +- src/Headers/usymtab.h | 2 +- src/Headers/valueMatrix.h | 4 +- src/Headers/valueTable.h | 4 +- src/Headers/warnClause.h | 6 +-- src/cscanner.l | 4 ++ src/cstringTable.c | 2 +- src/genericTable.c | 2 +- src/llmain.c | 6 +-- src/sRef.c | 4 +- src/usymtab.c | 2 +- 82 files changed, 234 insertions(+), 230 deletions(-) diff --git a/README b/README index 6b72cc0..6081398 100644 --- a/README +++ b/README @@ -61,10 +61,10 @@ the derived grammar files. This is not recommended however. LARCH_PATH - path to search for splint libraries and initializations files. If you are using the standard directories, this - should be .:/splint-3.0.0.9/lib. + should be .:/splint-3.0.0.20/lib. LCLIMPORTDIR - directory containing lcl imports files. If you are using - the standard directories, this is /splint-3.0.0.9/imports. + the standard directories, this is /splint-3.0.0.20/imports. Put the commands to set these variables (the actual commands will depend on the shell you are using) in one of your initialization dotfiles diff --git a/src/Headers/aliasTable.h b/src/Headers/aliasTable.h index 4aaceb3..9075ab3 100644 --- a/src/Headers/aliasTable.h +++ b/src/Headers/aliasTable.h @@ -21,10 +21,10 @@ struct s_aliasTable /*@i32 reserved works for struct identifiers@*/ /*@reldef@*/ /*@only@*/ o_sRefSet *values; } ; -extern /*@unused@*/ /*@truenull@*/ bool aliasTable_isUndefined (aliasTable p_s); -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool aliasTable_isUndefined (aliasTable p_s); +extern /*@unused@*/ /*@nullwhentrue@*/ bool aliasTable_isEmpty (/*@sef@*/ aliasTable p_s); -extern /*@falsenull@*/ bool aliasTable_isDefined (aliasTable p_s); +extern /*@falsewhennull@*/ bool aliasTable_isDefined (aliasTable p_s); /*@constant null aliasTable aliasTable_undefined; @*/ # define aliasTable_undefined ((aliasTable) NULL) diff --git a/src/Headers/annotationInfo.h b/src/Headers/annotationInfo.h index 0ce3da9..1e1dac7 100644 --- a/src/Headers/annotationInfo.h +++ b/src/Headers/annotationInfo.h @@ -26,10 +26,10 @@ struct s_annotationInfo { /*@constant null annotationInfo annotationInfo_undefined; @*/ # define annotationInfo_undefined ((annotationInfo) NULL) -extern /*@falsenull@*/ bool annotationInfo_isDefined (annotationInfo) /*@*/ ; +extern /*@falsewhennull@*/ bool annotationInfo_isDefined (annotationInfo) /*@*/ ; # define annotationInfo_isDefined(p_info) ((p_info) != annotationInfo_undefined) -extern /*@truenull@*/ bool annotationInfo_isUndefined (annotationInfo) /*@*/ ; +extern /*@nullwhentrue@*/ bool annotationInfo_isUndefined (annotationInfo) /*@*/ ; # define annotationInfo_isUndefined(p_info) ((p_info) == annotationInfo_undefined) extern bool annotationInfo_equal (annotationInfo, annotationInfo) /*@*/ ; diff --git a/src/Headers/annotationTable.h b/src/Headers/annotationTable.h index 054e1ec..25898b5 100644 --- a/src/Headers/annotationTable.h +++ b/src/Headers/annotationTable.h @@ -21,10 +21,10 @@ /*@constant null annotationTable annotationTable_undefined; @*/ # define annotationTable_undefined genericTable_undefined -extern /*@falsenull@*/ bool annotationTable_isDefined(annotationTable) /*@*/ ; +extern /*@falsewhennull@*/ bool annotationTable_isDefined(annotationTable) /*@*/ ; # define annotationTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) -extern /*@truenull@*/ bool annotationTable_isUndefined(annotationTable) /*@*/ ; +extern /*@nullwhentrue@*/ bool annotationTable_isUndefined(annotationTable) /*@*/ ; # define annotationTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) /*@constant int DEFAULT_ANNOTTABLE_SIZE@*/ diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 0f24839..22f8941 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -23,9 +23,9 @@ struct s_constraint { # define constraint_undefined ((constraint)NULL) -extern /*@falsenull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ; -extern /*@truenull@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool constraint_isDefined (constraint p_e) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool constraint_isUndefined (constraint p_e) /*@*/ ; +extern /*@nullwhentrue@*/ /*@unused@*/ bool constraint_isError (constraint p_e) /*@*/ ; # define constraint_isDefined(e) ((e) != constraint_undefined) # define constraint_isUndefined(e) ((e) == constraint_undefined) diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h index 64208e6..5035a54 100644 --- a/src/Headers/constraintExpr.h +++ b/src/Headers/constraintExpr.h @@ -20,9 +20,9 @@ struct s_constraintExpr { /*@constant null constraintExpr constraintExpr_undefined; @*/ # define constraintExpr_undefined ((constraintExpr)NULL) -extern /*@falsenull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool constraintExpr_isDefined (constraintExpr p_e) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isUndefined (constraintExpr p_e) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintExpr_isError (constraintExpr p_e) /*@*/ ; # define constraintExpr_isDefined(e) ((e) != constraintExpr_undefined) # define constraintExpr_isUndefined(e) ((e) == constraintExpr_undefined) @@ -83,7 +83,7 @@ constraintExpr constraintExpr_doSRefFixBaseParam ( /*@returned@*/ constraintExpr /*@only@*/ constraintExpr constraintExpr_doFixResult (/*@only@*/ constraintExpr p_expr, /*@observer@*/ exprNode p_fcnCall); -/*@falsenull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ; +/*@falsewhennull@*/ bool constraintExpr_isLit (constraintExpr p_expr) /*@*/ ; /*@only@*/ constraintExpr constraintExpr_makeAddExpr (/*@only@*/ constraintExpr p_expr, /*@only@*/ constraintExpr p_addent); @@ -104,7 +104,7 @@ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr p_ex /*@out@*/ bool * p_propagate, /*@out@*/ int *p_literal); -/*@falsenull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ; +/*@falsewhennull@*/ bool constraintExpr_isBinaryExpr (/*@observer@*/ /*@temp@*/ constraintExpr p_c) /*@*/ ; extern void constraintExpr_dump (/*@observer@*/ /*@temp@*/ constraintExpr p_expr, FILE *p_f); diff --git a/src/Headers/constraintExprData.h b/src/Headers/constraintExprData.h index 4f7564f..ffa97ac 100644 --- a/src/Headers/constraintExprData.h +++ b/src/Headers/constraintExprData.h @@ -41,7 +41,7 @@ typedef union constraintExprData constraintTerm term; } *constraintExprData; -extern /*@falsenull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool constraintExprData_isDefined (/*@temp@*/ /*@observer@*/ /*@reldef@*/ constraintExprData p_e) /*@*/ ; # define constraintExprData_isDefined(e) ((e) != NULL) extern void constraintExprData_freeBinaryExpr (/*@only@*/ constraintExprData) ; diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index 2770932..816e8e6 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -18,9 +18,9 @@ struct s_constraintList # define constraintList_undefined ((constraintList)NULL) -extern /*@falsenull@*/ bool constraintList_isDefined (constraintList p_e) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool constraintList_isUndefined (constraintList p_e) /*@*/ ; -extern /*@truenull@*/ /*@unused@*/ bool constraintList_isError (constraintList p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool constraintList_isDefined (constraintList p_e) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool constraintList_isUndefined (constraintList p_e) /*@*/ ; +extern /*@nullwhentrue@*/ /*@unused@*/ bool constraintList_isError (constraintList p_e) /*@*/ ; # define constraintList_isDefined(e) ((e) != constraintList_undefined) # define constraintList_isUndefined(e) ((e) == constraintList_undefined) diff --git a/src/Headers/constraintList2.h b/src/Headers/constraintList2.h index 7e8cbbf..72df086 100644 --- a/src/Headers/constraintList2.h +++ b/src/Headers/constraintList2.h @@ -32,7 +32,7 @@ extern int constraintList_size (/*@sef@*/ constraintList); extern bool constraintList_empty (/*@sef@*/ constraintList); # define constraintList_empty(s) (constraintList_size(s) == 0) -extern /*@falsenull@*/ bool constraintList_isDefined (constraintList p_t); +extern /*@falsewhennull@*/ bool constraintList_isDefined (constraintList p_t); # define constraintList_isDefined(s) ((s) != (constraintList) 0) extern /*@only@*/ constraintList constraintList_makeNew(void); diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h index 8a4ce5a..7755f55 100644 --- a/src/Headers/cstring.h +++ b/src/Headers/cstring.h @@ -129,11 +129,11 @@ extern void cstring_free (/*@only@*/ cstring p_s); /*@constant null cstring cstring_undefined;@*/ # define cstring_undefined ((cstring)NULL) -extern /*@falsenull@*/ bool cstring_isDefined (cstring p_s) /*@*/ ; -extern /*@truenull@*/ bool cstring_isUndefined (cstring p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool cstring_isDefined (cstring p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool cstring_isUndefined (cstring p_s) /*@*/ ; -extern /*@truenull@*/ bool cstring_isEmpty (cstring p_s) /*@*/ ; -extern /*@falsenull@*/ bool cstring_isNonEmpty (cstring p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool cstring_isEmpty (cstring p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool cstring_isNonEmpty (cstring p_s) /*@*/ ; # define cstring_isDefined(s) ((s) != cstring_undefined) # define cstring_isUndefined(s) (!cstring_isDefined(s)) diff --git a/src/Headers/cstringList.h b/src/Headers/cstringList.h index 3c91234..6a65507 100644 --- a/src/Headers/cstringList.h +++ b/src/Headers/cstringList.h @@ -16,13 +16,13 @@ abst_typedef /*@null@*/ struct s_cstringList /*@constant null cstringList cstringList_undefined;@*/ # define cstringList_undefined ((cstringList) NULL) -extern /*@falsenull@*/ bool cstringList_isDefined (cstringList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool cstringList_isDefined (cstringList p_s) /*@*/ ; # define cstringList_isDefined(s) ((s) != cstringList_undefined) extern int cstringList_size (/*@sef@*/ cstringList) /*@*/ ; # define cstringList_size(s) (cstringList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool cstringList_empty (/*@sef@*/ cstringList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool cstringList_empty (/*@sef@*/ cstringList) /*@*/ ; # define cstringList_empty(s) (cstringList_size(s) == 0) extern cstring cstringList_unparseSep (cstringList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/cstringSList.h b/src/Headers/cstringSList.h index dbf4e0b..6098787 100644 --- a/src/Headers/cstringSList.h +++ b/src/Headers/cstringSList.h @@ -18,13 +18,13 @@ abst_typedef /*@null@*/ struct s_cstringSList /*@constant null cstringSList cstringSList_undefined;@*/ # define cstringSList_undefined ((cstringSList) NULL) -extern /*@falsenull@*/ bool cstringSList_isDefined (cstringSList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool cstringSList_isDefined (cstringSList p_s) /*@*/ ; # define cstringSList_isDefined(s) ((s) != cstringSList_undefined) extern int cstringSList_size (/*@sef@*/ cstringSList) /*@*/ ; # define cstringSList_size(s) (cstringSList_isDefined (s) ? (s)->nelements : 0) -extern /*@falsenull@*/ bool cstringSList_empty (/*@sef@*/ cstringSList) /*@*/ ; +extern /*@falsewhennull@*/ bool cstringSList_empty (/*@sef@*/ cstringSList) /*@*/ ; # define cstringSList_empty(s) (cstringSList_size(s) == 0) extern /*@unused@*/ cstring cstringSList_unparseSep (cstringSList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/cstringTable.h b/src/Headers/cstringTable.h index 576aa48..053c4da 100644 --- a/src/Headers/cstringTable.h +++ b/src/Headers/cstringTable.h @@ -48,10 +48,10 @@ struct s_cstringTable /*@constant null cstringTable cstringTable_undefined; @*/ # define cstringTable_undefined ((cstringTable) NULL) -extern /*@falsenull@*/ bool cstringTable_isDefined(cstringTable) /*@*/ ; +extern /*@falsewhennull@*/ bool cstringTable_isDefined(cstringTable) /*@*/ ; # define cstringTable_isDefined(p_h) ((p_h) != cstringTable_undefined) -extern /*@truenull@*/ /*@unused@*/ bool cstringTable_isUndefined(cstringTable) /*@*/ ; +extern /*@nullwhentrue@*/ /*@unused@*/ bool cstringTable_isUndefined(cstringTable) /*@*/ ; # define cstringTable_isUndefined(p_h) ((p_h) == cstringTable_undefined) extern /*@only@*/ cstringTable cstringTable_create(int p_size) /*@*/ ; diff --git a/src/Headers/ctypeList.h b/src/Headers/ctypeList.h index 32f1c8c..7c3fecc 100644 --- a/src/Headers/ctypeList.h +++ b/src/Headers/ctypeList.h @@ -35,8 +35,8 @@ extern ctypeList ctypeList_add (/*@only@*/ ctypeList p_s, ctype p_el) /*@modifie extern /*@unused@*/ /*@only@*/ cstring ctypeList_unparse (ctypeList) /*@*/ ; extern void ctypeList_free (/*@only@*/ /*@only@*/ ctypeList p_s) /*@modifies p_s@*/; -extern /*@falsenull@*/ bool ctypeList_isDefined (/*@null@*/ ctypeList p_ct) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@falsewhennull@*/ bool ctypeList_isDefined (/*@null@*/ ctypeList p_ct) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool ctypeList_isUndefined (/*@null@*/ ctypeList p_ct) /*@*/ ; /*@constant null ctypeList ctypeList_undefined; @*/ diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h index 327fada..cd6d69c 100644 --- a/src/Headers/exprNode.h +++ b/src/Headers/exprNode.h @@ -174,9 +174,9 @@ struct s_exprNode /*@constant null exprNode exprNode_undefined; @*/ # define exprNode_undefined ((exprNode)NULL) -extern /*@falsenull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ; -extern /*@truenull@*/ bool exprNode_isError (exprNode p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool exprNode_isDefined (exprNode p_e) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool exprNode_isUndefined (exprNode p_e) /*@*/ ; +extern /*@nullwhentrue@*/ bool exprNode_isError (exprNode p_e) /*@*/ ; # define exprNode_isDefined(e) ((e) != exprNode_undefined) # define exprNode_isUndefined(e) ((e) == exprNode_undefined) @@ -191,7 +191,7 @@ extern ctype exprNode_getType (/*@sef@*/ exprNode p_e) /*@*/ ; # define exprNode_getType(e) \ (exprNode_isDefined(e) ? (e)->typ : ctype_unknown) -extern /*@unused@*/ /*@falsenull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool exprNode_isInParens (/*@sef@*/ exprNode p_e) /*@*/ ; # define exprNode_isInParens(e) \ (exprNode_isDefined(e) && (e)->kind == XPR_PARENS) diff --git a/src/Headers/fcnNodeList.h b/src/Headers/fcnNodeList.h index 93b61b9..c2be685 100644 --- a/src/Headers/fcnNodeList.h +++ b/src/Headers/fcnNodeList.h @@ -28,10 +28,10 @@ abst_typedef /*@null@*/ struct /*@constant null fcnNodeList fcnNodeList_undefined; @*/ # define fcnNodeList_undefined ((fcnNodeList)0) -extern /*@falsenull@*/ bool fcnNodeList_isDefined (fcnNodeList p_f); +extern /*@falsewhennull@*/ bool fcnNodeList_isDefined (fcnNodeList p_f); # define fcnNodeList_isDefined(f) ((f) != fcnNodeList_undefined) -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool fcnNodeList_isUndefined (fcnNodeList p_f); # define fcnNodeList_isUndefined(f) ((f) == fcnNodeList_undefined) diff --git a/src/Headers/fileIdList.h b/src/Headers/fileIdList.h index 46fce9a..0e5b171 100644 --- a/src/Headers/fileIdList.h +++ b/src/Headers/fileIdList.h @@ -15,7 +15,7 @@ abst_typedef /*@null@*/ ctypeList fileIdList; -extern /*@falsenull@*/ bool fileIdList_isDefined (fileIdList p_f); +extern /*@falsewhennull@*/ bool fileIdList_isDefined (fileIdList p_f); # define fileIdList_isDefined(f) (ctypeList_isDefined (f)) /*@iter fileIdList_elements (sef fileIdList x, yield fileId el); @*/ diff --git a/src/Headers/fileTable.h b/src/Headers/fileTable.h index 832e2aa..d1dd875 100644 --- a/src/Headers/fileTable.h +++ b/src/Headers/fileTable.h @@ -57,9 +57,9 @@ abst_typedef /*@null@*/ struct /*@constant null fileTable fileTable_undefined; @*/ # define fileTable_undefined ((fileTable) NULL) -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool fileTable_isUndefined (/*@null@*/ fileTable p_f) /*@*/ ; -extern /*@unused@*/ /*@falsenull@*/ bool +extern /*@unused@*/ /*@falsewhennull@*/ bool fileTable_isDefined (/*@null@*/ fileTable p_f) /*@*/ ; # define fileTable_isUndefined(ft) ((ft) == fileTable_undefined) diff --git a/src/Headers/fileloc.h b/src/Headers/fileloc.h index 21e98bb..d8dc68c 100644 --- a/src/Headers/fileloc.h +++ b/src/Headers/fileloc.h @@ -83,8 +83,8 @@ extern bool fileloc_isExternal (/*@sef@*/ fileloc p_f) /*@*/; # define fileloc_isExternal(f) \ (fileloc_isDefined(f) && ((f)->kind == FL_EXTERNAL)) -extern /*@falsenull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ; -extern /*@truenull@*/ bool fileloc_isUndefined (/*@null@*/ fileloc p_f) /*@*/ ; +extern /*@falsewhennull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ; +extern /*@nullwhentrue@*/ bool fileloc_isUndefined (/*@null@*/ fileloc p_f) /*@*/ ; extern bool fileloc_isInvalid (/*@sef@*/ /*@null@*/ fileloc p_f) /*@*/ ; /*@constant null fileloc fileloc_undefined; @*/ @@ -120,7 +120,7 @@ extern void fileloc_setColumnUndefined (/*@sef@*/ fileloc p_f) /*@modifies p_f@* (fileloc_isDefined(f) ? (f)->column = UNKNOWN_COLUMN : UNKNOWN_COLUMN) # endif -extern /*@falsenull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f); +extern /*@falsewhennull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f); # define fileloc_isValid(f) \ (fileloc_isDefined(f) && ((f)->lineno >= 0)) diff --git a/src/Headers/filelocList.h b/src/Headers/filelocList.h index 3a73437..c14eb65 100644 --- a/src/Headers/filelocList.h +++ b/src/Headers/filelocList.h @@ -12,9 +12,9 @@ abst_typedef /*@null@*/ struct /*@reldef@*/ /*@relnull@*/ o_fileloc *elements; } *filelocList ; -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool filelocList_isUndefined (filelocList p_f) /*@*/ ; -extern /*@falsenull@*/ bool filelocList_isDefined (filelocList p_f); +extern /*@falsewhennull@*/ bool filelocList_isDefined (filelocList p_f); /*@constant null filelocList filelocList_undefined; @*/ # define filelocList_undefined (NULL) diff --git a/src/Headers/filelocStack.h b/src/Headers/filelocStack.h index 067bce8..278b47c 100644 --- a/src/Headers/filelocStack.h +++ b/src/Headers/filelocStack.h @@ -15,7 +15,7 @@ abst_typedef /*@null@*/ struct /*@constant null filelocStack filelocStack_undefined; @*/ # define filelocStack_undefined (NULL) -extern /*@falsenull@*/ bool filelocStack_isDefined (filelocStack p_f) /*@*/ ; +extern /*@falsewhennull@*/ bool filelocStack_isDefined (filelocStack p_f) /*@*/ ; # define filelocStack_isDefined(f) ((f) != filelocStack_undefined) extern int filelocStack_size (/*@sef@*/ filelocStack p_s) /*@*/ ; diff --git a/src/Headers/flagSpec.h b/src/Headers/flagSpec.h index fc35025..493f1df 100644 --- a/src/Headers/flagSpec.h +++ b/src/Headers/flagSpec.h @@ -28,7 +28,7 @@ struct s_flagSpec /*@constant null flagSpec flagSpec_undefined; @*/ # define flagSpec_undefined ((flagSpec) NULL) -extern /*@falsenull@*/ bool flagSpec_isDefined (flagSpec p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool flagSpec_isDefined (flagSpec p_e) /*@*/ ; # define flagSpec_isDefined(e) ((e) != flagSpec_undefined) extern /*@only@*/ flagSpec flagSpec_createPlain (/*@only@*/ cstring) ; diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h index cb57af8..6814914 100644 --- a/src/Headers/functionClause.h +++ b/src/Headers/functionClause.h @@ -36,7 +36,7 @@ struct s_functionClause { /*@constant null functionClause functionClause_undefined; @*/ # define functionClause_undefined NULL -extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ; +extern /*@falsewhennull@*/ bool functionClause_isDefined(functionClause) /*@*/ ; # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined) extern bool functionClause_isGlobals (functionClause) /*@*/ ; @@ -59,7 +59,7 @@ extern bool functionClause_isEnsures (functionClause) /*@*/ ; extern bool functionClause_isRequires (functionClause) /*@*/ ; # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES)) -extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ; +extern /*@nullwhentrue@*/ bool functionClause_isUndefined(functionClause) /*@*/ ; # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined) extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ; diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h index 829e96c..471949b 100644 --- a/src/Headers/functionClauseList.h +++ b/src/Headers/functionClauseList.h @@ -19,16 +19,16 @@ struct s_functionClauseList /*@constant null functionClauseList functionClauseList_undefined;@*/ # define functionClauseList_undefined ((functionClauseList) NULL) -extern /*@falsenull@*/ bool functionClauseList_isDefined (functionClauseList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool functionClauseList_isDefined (functionClauseList p_s) /*@*/ ; # define functionClauseList_isDefined(s) ((s) != functionClauseList_undefined) -extern /*@truenull@*/ bool functionClauseList_isUndefined (functionClauseList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool functionClauseList_isUndefined (functionClauseList p_s) /*@*/ ; # define functionClauseList_isUndefined(s) ((s) == functionClauseList_undefined) extern int functionClauseList_size (/*@sef@*/ functionClauseList) /*@*/ ; # define functionClauseList_size(s) (functionClauseList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool functionClauseList_empty (/*@sef@*/ functionClauseList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool functionClauseList_empty (/*@sef@*/ functionClauseList) /*@*/ ; # define functionClauseList_empty(s) (functionClauseList_size(s) == 0) extern cstring functionClauseList_unparseSep (functionClauseList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/functionConstraint.h b/src/Headers/functionConstraint.h index 0a5dcf4..83035c6 100644 --- a/src/Headers/functionConstraint.h +++ b/src/Headers/functionConstraint.h @@ -26,10 +26,10 @@ struct s_functionConstraint { /*@constant null functionConstraint functionConstraint_undefined; @*/ # define functionConstraint_undefined ((functionConstraint) NULL) -extern /*@falsenull@*/ bool functionConstraint_isDefined (functionConstraint) /*@*/ ; +extern /*@falsewhennull@*/ bool functionConstraint_isDefined (functionConstraint) /*@*/ ; # define functionConstraint_isDefined(p_info) ((p_info) != NULL) -extern /*@truenull@*/ bool functionConstraint_isUndefined (functionConstraint) /*@*/ ; +extern /*@nullwhentrue@*/ bool functionConstraint_isUndefined (functionConstraint) /*@*/ ; # define functionConstraint_isUndefined(p_info) ((p_info) == NULL) extern functionConstraint functionConstraint_copy (functionConstraint) /*@*/ ; diff --git a/src/Headers/genericTable.h b/src/Headers/genericTable.h index 042c1cd..a405041 100644 --- a/src/Headers/genericTable.h +++ b/src/Headers/genericTable.h @@ -44,10 +44,10 @@ struct s_genericTable /*@constant null genericTable genericTable_undefined; @*/ # define genericTable_undefined ((genericTable) NULL) -extern /*@falsenull@*/ bool genericTable_isDefined(genericTable) /*@*/ ; +extern /*@falsewhennull@*/ bool genericTable_isDefined(genericTable) /*@*/ ; # define genericTable_isDefined(p_h) ((p_h) != genericTable_undefined) -extern /*@truenull@*/ /*@unused@*/ bool genericTable_isUndefined(genericTable) /*@*/ ; +extern /*@nullwhentrue@*/ /*@unused@*/ bool genericTable_isUndefined(genericTable) /*@*/ ; # define genericTable_isUndefined(p_h) ((p_h) == genericTable_undefined) extern /*@only@*/ genericTable genericTable_create (int p_size); diff --git a/src/Headers/globSet.h b/src/Headers/globSet.h index c0f2588..21d2d33 100644 --- a/src/Headers/globSet.h +++ b/src/Headers/globSet.h @@ -50,8 +50,8 @@ extern void globSet_clear (globSet p_g); /*@constant null globSet globSet_undefined;@*/ # define globSet_undefined sRefSet_undefined -extern /*@falsenull@*/ bool globSet_isDefined (/*@null@*/ globSet p_s) /*@*/ ; -extern /*@truenull@*/ bool globSet_isUndefined (/*@null@*/ globSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool globSet_isDefined (/*@null@*/ globSet p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool globSet_isUndefined (/*@null@*/ globSet p_s) /*@*/ ; # define globSet_isDefined(s) (sRefSet_isDefined (s)) # define globSet_isUndefined(s) (sRefSet_isUndefined (s)) diff --git a/src/Headers/guardSet.h b/src/Headers/guardSet.h index 6952cd4..302dd64 100644 --- a/src/Headers/guardSet.h +++ b/src/Headers/guardSet.h @@ -20,11 +20,11 @@ /*@constant null guardSet guardSet_undefined;@*/ # define guardSet_undefined ((guardSet)NULL) -extern /*@falsenull@*/ /*@unused@*/ bool +extern /*@falsewhennull@*/ /*@unused@*/ bool guardSet_isDefined (guardSet p_g) /*@*/ ; # define guardSet_isDefined(g) ((g) != guardSet_undefined) -extern /*@falsenull@*/ bool guardSet_isEmpty (guardSet p_g); +extern /*@falsewhennull@*/ bool guardSet_isEmpty (guardSet p_g); extern /*@only@*/ guardSet guardSet_new (void); extern guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet p_g, /*@exposed@*/ sRef p_s); diff --git a/src/Headers/idDecl.h b/src/Headers/idDecl.h index 9f39203..98749b5 100644 --- a/src/Headers/idDecl.h +++ b/src/Headers/idDecl.h @@ -20,7 +20,7 @@ struct s_idDecl /*@constant null idDecl idDecl_undefined; @*/ # define idDecl_undefined ((idDecl) NULL) -extern /*@falsenull@*/ bool idDecl_isDefined (idDecl p_t) /*@*/ ; +extern /*@falsewhennull@*/ bool idDecl_isDefined (idDecl p_t) /*@*/ ; # define idDecl_isDefined(t) ((t) != idDecl_undefined) extern void idDecl_free (/*@only@*/ idDecl p_t); diff --git a/src/Headers/inputStream.h b/src/Headers/inputStream.h index fa8c5c4..d50c826 100644 --- a/src/Headers/inputStream.h +++ b/src/Headers/inputStream.h @@ -26,8 +26,8 @@ struct s_inputStream { /* in forwardTypes.h: abst_typedef null struct _inputStream *inputStream; */ -extern /*@falsenull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ; -extern /*@truenull@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ; +extern /*@falsewhennull@*/ bool inputStream_isDefined (/*@null@*/ inputStream p_f) /*@*/ ; +extern /*@nullwhentrue@*/ bool inputStream_isUndefined (/*@null@*/ inputStream p_f) /*@*/ ; /*@constant null inputStream inputStream_undefined; @*/ # define inputStream_undefined ((inputStream) NULL) diff --git a/src/Headers/lclTypeSpecNode.h b/src/Headers/lclTypeSpecNode.h index d3ba22b..b3e8841 100644 --- a/src/Headers/lclTypeSpecNode.h +++ b/src/Headers/lclTypeSpecNode.h @@ -33,7 +33,7 @@ struct s_lclTypeSpecNode { /*@constant null lclTypeSpecNode lclTypeSpecNode_undefined; @*/ # define lclTypeSpecNode_undefined ((lclTypeSpecNode) 0) -extern /*@falsenull@*/ bool lclTypeSpecNode_isDefined (lclTypeSpecNode p_x) /*@*/ ; +extern /*@falsewhennull@*/ bool lclTypeSpecNode_isDefined (lclTypeSpecNode p_x) /*@*/ ; # define lclTypeSpecNode_isDefined(x) ((x) != lclTypeSpecNode_undefined) extern /*@null@*/ /*@only@*/ lclTypeSpecNode diff --git a/src/Headers/lslOpSet.h b/src/Headers/lslOpSet.h index 5e92ead..ccc2b0c 100644 --- a/src/Headers/lslOpSet.h +++ b/src/Headers/lslOpSet.h @@ -30,7 +30,7 @@ abst_typedef /*@null@*/ struct /*@constant null lslOpSet lslOpSet_undefined;@*/ # define lslOpSet_undefined ((lslOpSet) NULL) -extern /*@falsenull@*/ bool lslOpSet_isDefined (lslOpSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool lslOpSet_isDefined (lslOpSet p_s) /*@*/ ; # define lslOpSet_isDefined(s) ((s) != lslOpSet_undefined) extern /*@unused@*/ int diff --git a/src/Headers/lsymbolSet.h b/src/Headers/lsymbolSet.h index a380c34..2b657e0 100644 --- a/src/Headers/lsymbolSet.h +++ b/src/Headers/lsymbolSet.h @@ -22,7 +22,7 @@ abst_typedef /*@null@*/ struct /*@constant null lsymbolSet lsymbolSet_undefined; @*/ # define lsymbolSet_undefined (NULL) -extern /*@falsenull@*/ bool lsymbolSet_isDefined (lsymbolSet p_l) /*@*/ ; +extern /*@falsewhennull@*/ bool lsymbolSet_isDefined (lsymbolSet p_l) /*@*/ ; # define lsymbolSet_isDefined(l) ((l) != lsymbolSet_undefined) /*@iter lsymbolSet_elements (sef lsymbolSet s, yield lsymbol el); @*/ diff --git a/src/Headers/ltoken.h b/src/Headers/ltoken.h index 685a1bd..ef9f3f3 100644 --- a/src/Headers/ltoken.h +++ b/src/Headers/ltoken.h @@ -46,10 +46,10 @@ typedef /*@only@*/ ltoken o_ltoken; /*@constant null ltoken ltoken_undefined; @*/ # define ltoken_undefined ((ltoken)NULL) -extern /*@falsenull@*/ bool ltoken_isValid (ltoken p_tok); +extern /*@falsewhennull@*/ bool ltoken_isValid (ltoken p_tok); # define ltoken_isValid(t) ((t) != ltoken_undefined) -extern /*@truenull@*/ bool ltoken_isUndefined (ltoken p_tok); +extern /*@nullwhentrue@*/ bool ltoken_isUndefined (ltoken p_tok); # define ltoken_isUndefined(t) ((t) == ltoken_undefined) extern bool ltoken_isStateDefined (/*@sef@*/ ltoken p_tok) /*@*/ ; diff --git a/src/Headers/ltokenList.h b/src/Headers/ltokenList.h index 3bcf1ef..72b4957 100644 --- a/src/Headers/ltokenList.h +++ b/src/Headers/ltokenList.h @@ -32,10 +32,10 @@ abst_typedef /*@null@*/ struct /*@constant null ltokenList ltokenList_undefined;@*/ # define ltokenList_undefined NULL -extern /*@falsenull@*/ bool ltokenList_isDefined (ltokenList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool ltokenList_isDefined (ltokenList p_s) /*@*/ ; # define ltokenList_isDefined(s) ((s) != ltokenList_undefined) -extern /*@truenull@*/ bool ltokenList_isUndefined (ltokenList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool ltokenList_isUndefined (ltokenList p_s) /*@*/ ; # define ltokenList_isUndefined(s) ((s) == ltokenList_undefined) extern int ltokenList_size (/*@sef@*/ ltokenList p_s) /*@*/ ; diff --git a/src/Headers/messageLog.h b/src/Headers/messageLog.h index 5221959..beaf205 100644 --- a/src/Headers/messageLog.h +++ b/src/Headers/messageLog.h @@ -28,7 +28,7 @@ abst_typedef /*@null@*/ struct /*@constant null messageLog messageLog_undefined; @*/ # define messageLog_undefined ((messageLog)0) -extern /*@unused@*/ /*@falsenull@*/ bool +extern /*@unused@*/ /*@falsewhennull@*/ bool messageLog_isDefined (messageLog p_s) /*@*/ ; # define messageLog_isDefined(c) ((c) != messageLog_undefined) diff --git a/src/Headers/metaStateConstraintList.h b/src/Headers/metaStateConstraintList.h index e62047b..c50201e 100644 --- a/src/Headers/metaStateConstraintList.h +++ b/src/Headers/metaStateConstraintList.h @@ -14,9 +14,9 @@ struct s_metaStateConstraintList /*@reldef@*/ /*@relnull@*/ b_metaStateConstraint *elements; } ; -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ; -extern /*@falsenull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ; +extern /*@falsewhennull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ; /*@constant null metaStateConstraintList metaStateConstraintList_undefined; @*/ # define metaStateConstraintList_undefined (NULL) diff --git a/src/Headers/metaStateExpression.h b/src/Headers/metaStateExpression.h index 805d68c..7980c45 100644 --- a/src/Headers/metaStateExpression.h +++ b/src/Headers/metaStateExpression.h @@ -17,10 +17,10 @@ struct s_metaStateExpression { /*@constant null metaStateExpression metaStateExpression_undefined; @*/ # define metaStateExpression_undefined ((metaStateExpression) NULL) -extern /*@falsenull@*/ bool metaStateExpression_isDefined (metaStateExpression) /*@*/ ; +extern /*@falsewhennull@*/ bool metaStateExpression_isDefined (metaStateExpression) /*@*/ ; # define metaStateExpression_isDefined(p_info) ((p_info) != NULL) -extern /*@truenull@*/ bool metaStateExpression_isUndefined (metaStateExpression) /*@*/ ; +extern /*@nullwhentrue@*/ bool metaStateExpression_isUndefined (metaStateExpression) /*@*/ ; # define metaStateExpression_isUndefined(p_info) ((p_info) == NULL) extern /*@notnull@*/ metaStateExpression diff --git a/src/Headers/metaStateInfo.h b/src/Headers/metaStateInfo.h index 1919764..0aa4121 100644 --- a/src/Headers/metaStateInfo.h +++ b/src/Headers/metaStateInfo.h @@ -41,10 +41,10 @@ struct s_metaStateInfo { /*@constant null metaStateInfo metaStateInfo_undefined; @*/ # define metaStateInfo_undefined ((metaStateInfo) NULL) -extern /*@falsenull@*/ bool metaStateInfo_isDefined (metaStateInfo) /*@*/ ; +extern /*@falsewhennull@*/ bool metaStateInfo_isDefined (metaStateInfo) /*@*/ ; # define metaStateInfo_isDefined(p_info) ((p_info) != NULL) -extern /*@truenull@*/ bool metaStateInfo_isUndefined (metaStateInfo) /*@*/ ; +extern /*@nullwhentrue@*/ bool metaStateInfo_isUndefined (metaStateInfo) /*@*/ ; # define metaStateInfo_isUndefined(p_info) ((p_info) == NULL) extern /*@notnull@*/ metaStateInfo diff --git a/src/Headers/metaStateTable.h b/src/Headers/metaStateTable.h index 9420cd9..b1a5041 100644 --- a/src/Headers/metaStateTable.h +++ b/src/Headers/metaStateTable.h @@ -23,10 +23,10 @@ /*@constant null metaStateTable metaStateTable_undefined; @*/ # define metaStateTable_undefined genericTable_undefined -extern /*@falsenull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ; +extern /*@falsewhennull@*/ bool metaStateTable_isDefined(metaStateTable) /*@*/ ; # define metaStateTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) -extern /*@truenull@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ; +extern /*@nullwhentrue@*/ bool metaStateTable_isUndefined(metaStateTable) /*@*/ ; # define metaStateTable_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) /*@constant int DEFAULT_MSTABLE_SIZE@*/ diff --git a/src/Headers/misc.h b/src/Headers/misc.h index 8db1da7..726263d 100644 --- a/src/Headers/misc.h +++ b/src/Headers/misc.h @@ -57,10 +57,10 @@ extern int mstring_length (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_length(s) \ (((s) != NULL) ? size_toInt (strlen (s)) : 0) -extern /*@falsenull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mstring_isDefined (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_isDefined(s) ((s) != NULL) -extern /*@truenull@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool mstring_isEmpty (/*@sef@*/ /*@null@*/ char *p_s) /*@*/ ; # define mstring_isEmpty(s) (mstring_length(s) == 0) extern void mstring_markFree (/*@owned@*/ char *p_s) /*@modifies *p_s;@*/ ; diff --git a/src/Headers/mtAnnotationList.h b/src/Headers/mtAnnotationList.h index 43632e4..c99a8f9 100644 --- a/src/Headers/mtAnnotationList.h +++ b/src/Headers/mtAnnotationList.h @@ -16,13 +16,13 @@ struct s_mtAnnotationList /*@constant null mtAnnotationList mtAnnotationList_undefined;@*/ # define mtAnnotationList_undefined ((mtAnnotationList) NULL) -extern /*@falsenull@*/ bool mtAnnotationList_isDefined (mtAnnotationList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtAnnotationList_isDefined (mtAnnotationList p_s) /*@*/ ; # define mtAnnotationList_isDefined(s) ((s) != mtAnnotationList_undefined) extern int mtAnnotationList_size (/*@sef@*/ mtAnnotationList) /*@*/ ; # define mtAnnotationList_size(s) (mtAnnotationList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool mtAnnotationList_empty (/*@sef@*/ mtAnnotationList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool mtAnnotationList_empty (/*@sef@*/ mtAnnotationList) /*@*/ ; # define mtAnnotationList_empty(s) (mtAnnotationList_size(s) == 0) extern cstring mtAnnotationList_unparseSep (mtAnnotationList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/mtContextNode.h b/src/Headers/mtContextNode.h index 567d2a9..6797aad 100644 --- a/src/Headers/mtContextNode.h +++ b/src/Headers/mtContextNode.h @@ -28,7 +28,7 @@ struct s_mtContextNode { /*@constant null mtContextNode mtContextNode_undefined@*/ # define mtContextNode_undefined ((mtContextNode) 0) -extern /*@falsenull@*/ bool mtContextNode_isDefined (mtContextNode p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtContextNode_isDefined (mtContextNode p_s) /*@*/ ; # define mtContextNode_isDefined(s) ((s) != mtContextNode_undefined) extern cstring mtContextNode_unparse (mtContextNode) /*@*/ ; diff --git a/src/Headers/mtDeclarationPiece.h b/src/Headers/mtDeclarationPiece.h index 9cfb196..d9ae03f 100644 --- a/src/Headers/mtDeclarationPiece.h +++ b/src/Headers/mtDeclarationPiece.h @@ -28,10 +28,10 @@ struct s_mtDeclarationPiece { /*@constant null mtDeclarationPiece mtDeclarationPiece_undefined; @*/ # define mtDeclarationPiece_undefined NULL -extern /*@falsenull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ; +extern /*@falsewhennull@*/ bool mtDeclarationPiece_isDefined(mtDeclarationPiece) /*@*/ ; # define mtDeclarationPiece_isDefined(p_h) ((p_h) != mtDeclarationPiece_undefined) -extern /*@truenull@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ; +extern /*@nullwhentrue@*/ bool mtDeclarationPiece_isUndefined(mtDeclarationPiece) /*@*/ ; # define mtDeclarationPiece_isUndefined(p_h) ((p_h) == mtDeclarationPiece_undefined) extern mtDeclarationPiece mtDeclarationPiece_createContext (/*@only@*/ mtContextNode) /*@*/ ; diff --git a/src/Headers/mtDeclarationPieces.h b/src/Headers/mtDeclarationPieces.h index 26be9cd..a6b5131 100644 --- a/src/Headers/mtDeclarationPieces.h +++ b/src/Headers/mtDeclarationPieces.h @@ -20,10 +20,10 @@ struct s_mtDeclarationPieces { /*@constant null mtDeclarationPieces mtDeclarationPieces_undefined; @*/ # define mtDeclarationPieces_undefined NULL -extern /*@falsenull@*/ bool mtDeclarationPieces_isDefined(mtDeclarationPieces) /*@*/ ; +extern /*@falsewhennull@*/ bool mtDeclarationPieces_isDefined(mtDeclarationPieces) /*@*/ ; # define mtDeclarationPieces_isDefined(p_h) ((p_h) != mtDeclarationPieces_undefined) -extern /*@truenull@*/ bool mtDeclarationPieces_isUndefined(mtDeclarationPieces) /*@*/ ; +extern /*@nullwhentrue@*/ bool mtDeclarationPieces_isUndefined(mtDeclarationPieces) /*@*/ ; # define mtDeclarationPieces_isUndefined(p_h) ((p_h) == mtDeclarationPieces_undefined) extern mtDeclarationPieces mtDeclarationPieces_create (void) /*@*/ ; diff --git a/src/Headers/mtDefaultsDeclList.h b/src/Headers/mtDefaultsDeclList.h index 3fb005b..fcff276 100644 --- a/src/Headers/mtDefaultsDeclList.h +++ b/src/Headers/mtDefaultsDeclList.h @@ -19,13 +19,13 @@ struct s_mtDefaultsDeclList /*@constant null mtDefaultsDeclList mtDefaultsDeclList_undefined;@*/ # define mtDefaultsDeclList_undefined ((mtDefaultsDeclList) NULL) -extern /*@falsenull@*/ bool mtDefaultsDeclList_isDefined (mtDefaultsDeclList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtDefaultsDeclList_isDefined (mtDefaultsDeclList p_s) /*@*/ ; # define mtDefaultsDeclList_isDefined(s) ((s) != mtDefaultsDeclList_undefined) extern int mtDefaultsDeclList_size (/*@sef@*/ mtDefaultsDeclList) /*@*/ ; # define mtDefaultsDeclList_size(s) (mtDefaultsDeclList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool mtDefaultsDeclList_empty (/*@sef@*/ mtDefaultsDeclList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool mtDefaultsDeclList_empty (/*@sef@*/ mtDefaultsDeclList) /*@*/ ; # define mtDefaultsDeclList_empty(s) (mtDefaultsDeclList_size(s) == 0) extern cstring mtDefaultsDeclList_unparseSep (mtDefaultsDeclList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/mtLoseReferenceList.h b/src/Headers/mtLoseReferenceList.h index c58b9c2..a0ef72b 100644 --- a/src/Headers/mtLoseReferenceList.h +++ b/src/Headers/mtLoseReferenceList.h @@ -19,13 +19,13 @@ struct s_mtLoseReferenceList /*@constant null mtLoseReferenceList mtLoseReferenceList_undefined;@*/ # define mtLoseReferenceList_undefined ((mtLoseReferenceList) NULL) -extern /*@falsenull@*/ bool mtLoseReferenceList_isDefined (mtLoseReferenceList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtLoseReferenceList_isDefined (mtLoseReferenceList p_s) /*@*/ ; # define mtLoseReferenceList_isDefined(s) ((s) != mtLoseReferenceList_undefined) extern int mtLoseReferenceList_size (/*@sef@*/ mtLoseReferenceList) /*@*/ ; # define mtLoseReferenceList_size(s) (mtLoseReferenceList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool mtLoseReferenceList_empty (/*@sef@*/ mtLoseReferenceList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool mtLoseReferenceList_empty (/*@sef@*/ mtLoseReferenceList) /*@*/ ; # define mtLoseReferenceList_empty(s) (mtLoseReferenceList_size(s) == 0) extern cstring mtLoseReferenceList_unparseSep (mtLoseReferenceList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/mtMergeClauseList.h b/src/Headers/mtMergeClauseList.h index 30c7c1b..12f5d5b 100644 --- a/src/Headers/mtMergeClauseList.h +++ b/src/Headers/mtMergeClauseList.h @@ -19,13 +19,13 @@ struct s_mtMergeClauseList /*@constant null mtMergeClauseList mtMergeClauseList_undefined;@*/ # define mtMergeClauseList_undefined ((mtMergeClauseList) NULL) -extern /*@falsenull@*/ bool mtMergeClauseList_isDefined (mtMergeClauseList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtMergeClauseList_isDefined (mtMergeClauseList p_s) /*@*/ ; # define mtMergeClauseList_isDefined(s) ((s) != mtMergeClauseList_undefined) extern int mtMergeClauseList_size (/*@sef@*/ mtMergeClauseList) /*@*/ ; # define mtMergeClauseList_size(s) (mtMergeClauseList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool mtMergeClauseList_empty (/*@sef@*/ mtMergeClauseList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool mtMergeClauseList_empty (/*@sef@*/ mtMergeClauseList) /*@*/ ; # define mtMergeClauseList_empty(s) (mtMergeClauseList_size(s) == 0) extern cstring mtMergeClauseList_unparseSep (mtMergeClauseList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/mtTransferClauseList.h b/src/Headers/mtTransferClauseList.h index 12bd70d..15b327c 100644 --- a/src/Headers/mtTransferClauseList.h +++ b/src/Headers/mtTransferClauseList.h @@ -19,13 +19,13 @@ struct s_mtTransferClauseList /*@constant null mtTransferClauseList mtTransferClauseList_undefined;@*/ # define mtTransferClauseList_undefined ((mtTransferClauseList) NULL) -extern /*@falsenull@*/ bool mtTransferClauseList_isDefined (mtTransferClauseList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool mtTransferClauseList_isDefined (mtTransferClauseList p_s) /*@*/ ; # define mtTransferClauseList_isDefined(s) ((s) != mtTransferClauseList_undefined) extern int mtTransferClauseList_size (/*@sef@*/ mtTransferClauseList) /*@*/ ; # define mtTransferClauseList_size(s) (mtTransferClauseList_isDefined (s) ? (s)->nelements : 0) -extern /*@unused@*/ /*@falsenull@*/ bool mtTransferClauseList_empty (/*@sef@*/ mtTransferClauseList) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool mtTransferClauseList_empty (/*@sef@*/ mtTransferClauseList) /*@*/ ; # define mtTransferClauseList_empty(s) (mtTransferClauseList_size(s) == 0) extern cstring mtTransferClauseList_unparseSep (mtTransferClauseList p_s, cstring p_sep) /*@*/ ; diff --git a/src/Headers/multiVal.h b/src/Headers/multiVal.h index ff80e0c..71b88c2 100644 --- a/src/Headers/multiVal.h +++ b/src/Headers/multiVal.h @@ -19,9 +19,9 @@ typedef /*@null@*/ struct } value; } *multiVal; -extern /*@falsenull@*/ bool multiVal_isDefined (multiVal p_m) /*@*/ ; -extern /*@truenull@*/ bool multiVal_isUndefined (multiVal p_m) /*@*/ ; -extern /*@truenull@*/ bool multiVal_isUnknown (multiVal p_m) /*@*/ ; +extern /*@falsewhennull@*/ bool multiVal_isDefined (multiVal p_m) /*@*/ ; +extern /*@nullwhentrue@*/ bool multiVal_isUndefined (multiVal p_m) /*@*/ ; +extern /*@nullwhentrue@*/ bool multiVal_isUnknown (multiVal p_m) /*@*/ ; extern multiVal multiVal_add (multiVal p_m1, multiVal p_m2) /*@*/ ; extern multiVal multiVal_subtract (multiVal p_m1, multiVal p_m2) /*@*/ ; @@ -50,10 +50,10 @@ extern void multiVal_free (/*@only@*/ multiVal p_m); extern multiVal multiVal_invert (multiVal p_m) /*@*/ ; -extern /*@falsenull@*/ bool multiVal_isInt (multiVal p_m) /*@*/ ; -extern /*@falsenull@*/ bool multiVal_isChar (multiVal p_m) /*@*/ ; -extern /*@falsenull@*/ bool multiVal_isDouble (multiVal p_m) /*@*/ ; -extern /*@falsenull@*/ bool multiVal_isString (multiVal p_m) /*@*/ ; +extern /*@falsewhennull@*/ bool multiVal_isInt (multiVal p_m) /*@*/ ; +extern /*@falsewhennull@*/ bool multiVal_isChar (multiVal p_m) /*@*/ ; +extern /*@falsewhennull@*/ bool multiVal_isDouble (multiVal p_m) /*@*/ ; +extern /*@falsewhennull@*/ bool multiVal_isString (multiVal p_m) /*@*/ ; extern /*@only@*/ multiVal multiVal_undump (char **p_s) /*@modifies *p_s;@*/ ; extern /*@only@*/ cstring multiVal_dump (multiVal p_m) /*@*/ ; diff --git a/src/Headers/pairNodeList.h b/src/Headers/pairNodeList.h index a904d9b..c660092 100644 --- a/src/Headers/pairNodeList.h +++ b/src/Headers/pairNodeList.h @@ -24,7 +24,7 @@ abst_typedef /*@null@*/ struct # define end_pairNodeList_elements }} -extern /*@falsenull@*/ bool pairNodeList_isDefined (pairNodeList p_p) /*@*/ ; +extern /*@falsewhennull@*/ bool pairNodeList_isDefined (pairNodeList p_p) /*@*/ ; /*@constant null pairNodeList pairNodeList_undefined; @*/ # define pairNodeList_undefined ((pairNodeList)0) diff --git a/src/Headers/paramNodeList.h b/src/Headers/paramNodeList.h index 97ba6e0..1fe049a 100644 --- a/src/Headers/paramNodeList.h +++ b/src/Headers/paramNodeList.h @@ -33,7 +33,7 @@ extern bool paramNodeList_empty (/*@sef@*/ paramNodeList p_s); extern /*@only@*/ paramNodeList paramNodeList_single (/*@keep@*/ paramNode p_p); -extern /*@falsenull@*/ bool paramNodeList_isDefined (paramNodeList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool paramNodeList_isDefined (paramNodeList p_s) /*@*/ ; # define paramNodeList_isDefined(s) ((s) != (paramNodeList)0) extern /*@only@*/ paramNodeList paramNodeList_new (void); @@ -52,7 +52,7 @@ extern /*@only@*/ cstring paramNodeList_unparseComments (paramNodeList p_s); /*@constant null paramNodeList paramNodeList_undefined; @*/ # define paramNodeList_undefined ((paramNodeList) 0) -extern /*@truenull@*/ bool paramNodeList_isNull (/*@null@*/ paramNodeList p_p); +extern /*@nullwhentrue@*/ bool paramNodeList_isNull (/*@null@*/ paramNodeList p_p); # define paramNodeList_isNull(p) ((p) == paramNodeList_undefined) diff --git a/src/Headers/qtype.h b/src/Headers/qtype.h index 88275f6..d4682db 100644 --- a/src/Headers/qtype.h +++ b/src/Headers/qtype.h @@ -21,10 +21,10 @@ abst_typedef /*@null@*/ struct /*@constant null qtype qtype_undefined;@*/ # define qtype_undefined ((qtype) NULL) -extern /*@truenull@*/ bool qtype_isUndefined (qtype p_q); +extern /*@nullwhentrue@*/ bool qtype_isUndefined (qtype p_q); # define qtype_isUndefined(q) ((q) == qtype_undefined) -extern /*@falsenull@*/ bool qtype_isDefined (qtype p_q); +extern /*@falsewhennull@*/ bool qtype_isDefined (qtype p_q); # define qtype_isDefined(q) ((q) != qtype_undefined) extern ctype qtype_getType (/*@sef@*/ qtype p_q); diff --git a/src/Headers/qualList.h b/src/Headers/qualList.h index 8e80eb7..38bab62 100644 --- a/src/Headers/qualList.h +++ b/src/Headers/qualList.h @@ -12,8 +12,8 @@ abst_typedef /*@null@*/ struct /*@reldef@*/ /*@relnull@*/ qual *elements; } *qualList ; -extern /*@falsenull@*/ bool qualList_isDefined (qualList p_s); -extern /*@unused@*/ /*@truenull@*/ bool qualList_isUndefined (qualList p_s); +extern /*@falsewhennull@*/ bool qualList_isDefined (qualList p_s); +extern /*@unused@*/ /*@nullwhentrue@*/ bool qualList_isUndefined (qualList p_s); /*@constant null qualList qualList_undefined; @*/ # define qualList_undefined ((qualList) NULL) diff --git a/src/Headers/rangeTable.h b/src/Headers/rangeTable.h index 829df88..c46e307 100644 --- a/src/Headers/rangeTable.h +++ b/src/Headers/rangeTable.h @@ -43,10 +43,10 @@ struct _rangeTable } ; -extern /*@unused@*/ /*@truenull@*/ bool rangeTable_isUndefined (rangeTable p_s); -extern /*@unused@*/ /*@truenull@*/ bool +extern /*@unused@*/ /*@nullwhentrue@*/ bool rangeTable_isUndefined (rangeTable p_s); +extern /*@unused@*/ /*@nullwhentrue@*/ bool rangeTable_isEmpty (/*@sef@*/ rangeTable p_s); -extern /*@falsenull@*/ bool rangeTable_isDefined (rangeTable p_s); +extern /*@falsewhennull@*/ bool rangeTable_isDefined (rangeTable p_s); /*@constant null rangeTable rangeTable_undefined; @*/ # define rangeTable_undefined ((rangeTable) NULL) diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h index 2381642..77033ac 100644 --- a/src/Headers/sRef.h +++ b/src/Headers/sRef.h @@ -150,8 +150,8 @@ extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc) extern void sRef_setPosNull (sRef p_s, fileloc p_loc); extern void sRef_setDefNull (sRef p_s, fileloc p_loc); -extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ; /*@constant null sRef sRef_undefined; @*/ # define sRef_undefined ((sRef) NULL) @@ -165,11 +165,11 @@ extern bool sRef_isNotNull (sRef p_s) /*@*/ ; extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ; extern bool sRef_hasLastReference (sRef p_s) /*@*/ ; # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s)) @@ -202,7 +202,7 @@ extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR) -extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isConj(s) (sRef_isValid(s) && (s)->kind == SK_CONJ) extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f); @@ -234,7 +234,7 @@ extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s); extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc); -extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL) extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ; @@ -255,13 +255,13 @@ extern ctype sRef_getType (sRef p_s) /*@*/ ; extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ; -extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ; extern void sRef_setType (sRef p_s, ctype p_t); extern void sRef_setTypeFull (sRef p_s, ctype p_t); @@ -323,7 +323,7 @@ extern /*@exposed@*/ sRef sRef_buildPointer (/*@exposed@*/ sRef p_t) extern /*@exposed@*/ sRef sRef_makeAddress (/*@exposed@*/ sRef p_t); extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeUnconstrained (/*@exposed@*/ cstring) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isUnconstrained (sRef p_s) /*@*/ ; extern /*@observer@*/ cstring sRef_unconstrainedName (sRef p_s) /*@*/ ; @@ -428,18 +428,18 @@ extern void sRef_setAllocated (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setAllocatedShallowComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern void sRef_setAllocatedComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ; extern /*@only@*/ cstring sRef_unparseKindNamePlain (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRealGlobal(sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isFileStatic (sRef p_s) /*@*/ ; extern int sRef_getScope (sRef p_s) /*@*/ ; extern /*@observer@*/ cstring sRef_getScopeName (sRef p_s) /*@*/ ; /* must be real function (passed as function param) */ -extern /*@falsenull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isDead (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isDeadStorage (sRef p_s) /*@*/ ; extern bool sRef_isStateLive (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; -extern /*@truenull@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPossiblyDead (sRef p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRef_isStateUndefined (sRef p_s) /*@*/ ; extern bool sRef_isUnuseable (sRef p_s) /*@*/ ; extern /*@exposed@*/ sRef sRef_constructDeref (sRef p_t) @@ -450,7 +450,7 @@ extern /*@exposed@*/ sRef sRef_constructDeadDeref (sRef p_t) extern bool sRef_isJustAllocated (sRef p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isAllocated (sRef p_s) /*@*/ ; extern bool sRef_isUndefGlob (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isUndefGlob(s) \ @@ -489,7 +489,7 @@ extern bool sRef_isAnyDefined (/*@sef@*/ sRef p_s) /*@*/ ; || ((s)->defstate == SS_RELDEF) \ || ((s)->defstate == SS_PARTIAL))) -extern /*@falsenull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isPdefined (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isPdefined(s) \ ((sRef_isValid(s)) && ((s)->defstate == SS_PDEFINED)) @@ -499,15 +499,15 @@ extern bool sRef_isStateUnknown (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isStateUnknown(s) \ ((sRef_isValid(s)) && ((s)->defstate == SS_UNKNOWN)) -extern /*@falsenull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isRefCounted (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isRefCounted(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_REFCOUNTED)) -extern /*@falsenull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isNewRef (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isNewRef(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_NEWREF)) -extern /*@falsenull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRef_isKillRef (/*@sef@*/ sRef p_s) /*@*/ ; # define sRef_isKillRef(s) \ ((sRef_isValid(s)) && ((s)->aliaskind == AK_KILLREF)) diff --git a/src/Headers/sRefList.h b/src/Headers/sRefList.h index 4bb32c3..cf77623 100644 --- a/src/Headers/sRefList.h +++ b/src/Headers/sRefList.h @@ -29,9 +29,9 @@ struct s_sRefList extern int sRefList_size (sRefList p_s) /*@*/ ; -extern /*@truenull@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ; -extern /*@unused@*/ /*@falsenull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ; # define sRefList_isEmpty(s) (sRefList_size(s) == 0) diff --git a/src/Headers/sRefSet.h b/src/Headers/sRefSet.h index d70d5aa..969fa0d 100644 --- a/src/Headers/sRefSet.h +++ b/src/Headers/sRefSet.h @@ -52,9 +52,9 @@ struct s_sRefSet /*@constant null sRefSet sRefSet_undefined;@*/ # define sRefSet_undefined ((sRefSet) 0) -extern /*@truenull@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ; -extern /*@truenull@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ; -extern /*@falsenull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ; # define sRefSet_isUndefined(s) ((s) == sRefSet_undefined) # define sRefSet_isDefined(s) ((s) != sRefSet_undefined) diff --git a/src/Headers/sRefSetList.h b/src/Headers/sRefSetList.h index e90e9cf..4b2dd04 100644 --- a/src/Headers/sRefSetList.h +++ b/src/Headers/sRefSetList.h @@ -27,10 +27,10 @@ abst_typedef /*@null@*/ struct /*@constant null sRefSetList sRefSetList_undefined; @*/ # define sRefSetList_undefined ((sRefSetList) NULL) -extern /*@falsenull@*/ bool sRefSetList_isDefined (sRefSetList p_s); +extern /*@falsewhennull@*/ bool sRefSetList_isDefined (sRefSetList p_s); # define sRefSetList_isDefined(s) ((s) != sRefSetList_undefined) -extern /*@unused@*/ /*@truenull@*/ bool sRefSetList_isUndefined (sRefSetList p_s); +extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefSetList_isUndefined (sRefSetList p_s); # define sRefSetList_isUndefined(s) ((s) == sRefSetList_undefined) extern sRefSetList diff --git a/src/Headers/sRefTable.h b/src/Headers/sRefTable.h index 6ed695f..24853e1 100644 --- a/src/Headers/sRefTable.h +++ b/src/Headers/sRefTable.h @@ -27,9 +27,9 @@ abst_typedef /*@null@*/ struct /*@constant null sRefTable sRefTable_undefined; @*/ # define sRefTable_undefined ((sRefTable) NULL) -extern /*@truenull@*/ bool sRefTable_isNull (sRefTable p_s) /*@*/ ; -extern /*@truenull@*/ bool sRefTable_isEmpty (/*@sef@*/ sRefTable p_s) /*@*/ ; -extern /*@unused@*/ /*@falsenull@*/ bool +extern /*@nullwhentrue@*/ bool sRefTable_isNull (sRefTable p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sRefTable_isEmpty (/*@sef@*/ sRefTable p_s) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool sRefTable_isDefined (sRefTable p_s) /*@*/ ; # define sRefTable_isNull(s) ((s) == sRefTable_undefined) diff --git a/src/Headers/sigNodeSet.h b/src/Headers/sigNodeSet.h index e576d71..ac1bec6 100644 --- a/src/Headers/sigNodeSet.h +++ b/src/Headers/sigNodeSet.h @@ -33,11 +33,11 @@ abst_typedef /*@null@*/ struct /*@constant null sigNodeSet sigNodeSet_undefined; @*/ # define sigNodeSet_undefined ((sigNodeSet) 0) -extern /*@falsenull@*/ bool sigNodeSet_isDefined (sigNodeSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sigNodeSet_isDefined (sigNodeSet p_s) /*@*/ ; # define sigNodeSet_isDefined(s) \ ((s) != sigNodeSet_undefined) -extern /*@truenull@*/ bool sigNodeSet_isUndefined (sigNodeSet p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool sigNodeSet_isUndefined (sigNodeSet p_s) /*@*/ ; # define sigNodeSet_isUndefined(s) \ ((s) == sigNodeSet_undefined) diff --git a/src/Headers/sortSet.h b/src/Headers/sortSet.h index 7639dbc..a1f5d30 100644 --- a/src/Headers/sortSet.h +++ b/src/Headers/sortSet.h @@ -29,7 +29,7 @@ abst_typedef /*@null@*/ struct /*@constant null sortSet sortSet_undefined; @*/ # define sortSet_undefined ((sortSet) NULL) -extern /*@falsenull@*/ bool sortSet_isDefined (sortSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool sortSet_isDefined (sortSet p_s) /*@*/ ; # define sortSet_isDefined(s) ((s) != sortSet_undefined) extern int sortSet_size (/*@sef@*/ sortSet p_s); diff --git a/src/Headers/stateClauseList.h b/src/Headers/stateClauseList.h index 79b3348..5049d11 100644 --- a/src/Headers/stateClauseList.h +++ b/src/Headers/stateClauseList.h @@ -22,10 +22,10 @@ extern void stateClauseList_checkAll (uentry p_ue) /*@constant null stateClauseList stateClauseList_undefined@*/ # define stateClauseList_undefined ((stateClauseList) 0) -extern /*@falsenull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ; # define stateClauseList_isDefined(s) ((s) != stateClauseList_undefined) -extern /*@truenull@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ; # define stateClauseList_isUndefined(s) ((s) == stateClauseList_undefined) extern /*@unused@*/ int diff --git a/src/Headers/stateInfo.h b/src/Headers/stateInfo.h index a5d0fcb..2e2d223 100644 --- a/src/Headers/stateInfo.h +++ b/src/Headers/stateInfo.h @@ -19,7 +19,7 @@ typedef /*@null@*/ struct /*@constant null stateInfo stateInfo_undefined@*/ # define stateInfo_undefined (NULL) -extern /*@falsenull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool stateInfo_isDefined (stateInfo p_s) /*@*/ ; # define stateInfo_isDefined(p_s) ((p_s) != stateInfo_undefined) extern void stateInfo_free (/*@only@*/ stateInfo p_a); diff --git a/src/Headers/stateValue.h b/src/Headers/stateValue.h index d535074..5f8700d 100644 --- a/src/Headers/stateValue.h +++ b/src/Headers/stateValue.h @@ -27,10 +27,10 @@ extern /*@notnull@*/ stateValue stateValue_createImplicit (int p_value, /*@only@ /*@constant null stateValue stateValue_undefined@*/ # define stateValue_undefined (NULL) -extern /*@truenull@*/ bool stateValue_isUndefined (stateValue) /*@*/ ; +extern /*@nullwhentrue@*/ bool stateValue_isUndefined (stateValue) /*@*/ ; # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined) -extern /*@falsenull@*/ bool stateValue_isDefined (stateValue) /*@*/ ; +extern /*@falsewhennull@*/ bool stateValue_isDefined (stateValue) /*@*/ ; # define stateValue_isDefined(p_s) ((p_s) != NULL) extern bool stateValue_isImplicit (stateValue) /*@*/ ; diff --git a/src/Headers/symtable.h b/src/Headers/symtable.h index aed7481..e9a72a9 100644 --- a/src/Headers/symtable.h +++ b/src/Headers/symtable.h @@ -133,16 +133,16 @@ typedef struct { typedef struct s_symtableStruct *symtable; -extern /*@falsenull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti); +extern /*@falsewhennull@*/ bool typeInfo_exists(/*@null@*/ typeInfo p_ti); # define typeInfo_exists(ti) ((ti) != NULL) -extern /*@falsenull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi); +extern /*@falsewhennull@*/ bool varInfo_exists(/*@null@*/ varInfo p_vi); # define varInfo_exists(vi) ((vi) != NULL) -extern /*@falsenull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi); +extern /*@falsewhennull@*/ bool tagInfo_exists(/*@null@*/ tagInfo p_oi); # define tagInfo_exists(ti) ((ti) != NULL) -extern /*@falsenull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi); +extern /*@falsewhennull@*/ bool opInfo_exists(/*@null@*/ opInfo p_oi); # define opInfo_exists(oi) ((oi) != NULL) extern /*@only@*/ symtable symtable_new (void) /*@*/ ; diff --git a/src/Headers/termNode.h b/src/Headers/termNode.h index 35b4541..219a4fc 100644 --- a/src/Headers/termNode.h +++ b/src/Headers/termNode.h @@ -23,7 +23,7 @@ struct s_termNode /*@reldef@*/ lclTypeSpecNode sizeofField; /* only for TRM_SIZEOF */ } ; -extern /*@falsenull@*/ bool termNode_isDefined (/*@null@*/ termNode p_t) /*@*/ ; +extern /*@falsewhennull@*/ bool termNode_isDefined (/*@null@*/ termNode p_t) /*@*/ ; # define termNode_isDefined(t) ((t) != NULL) extern termNode termNode_copySafe (termNode p_t) /*@*/ ; diff --git a/src/Headers/termNodeList.h b/src/Headers/termNodeList.h index 0adeec9..6efc415 100644 --- a/src/Headers/termNodeList.h +++ b/src/Headers/termNodeList.h @@ -32,7 +32,7 @@ extern int termNodeList_size (/*@sef@*/ termNodeList); extern bool termNodeList_empty (/*@sef@*/ termNodeList); # define termNodeList_empty(s) (termNodeList_size(s) == 0) -extern /*@falsenull@*/ bool termNodeList_isDefined (termNodeList p_t); +extern /*@falsewhennull@*/ bool termNodeList_isDefined (termNodeList p_t); # define termNodeList_isDefined(s) ((s) != (termNodeList) 0) extern /*@only@*/ termNodeList termNodeList_new(void); diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h index 1d1f4fc..00eef1f 100644 --- a/src/Headers/uentry.h +++ b/src/Headers/uentry.h @@ -169,11 +169,11 @@ struct s_uentry ** uentry_isDefined). */ -extern /*@truenull@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) +extern /*@nullwhentrue@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) /*@*/ ; -extern /*@truenull@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) +extern /*@nullwhentrue@*/ bool uentry_isInvalid (/*@special@*/ uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isValid (/*@special@*/ uentry p_e) /*@*/ ; /*@constant null uentry uentry_undefined; @*/ @@ -193,51 +193,51 @@ extern void uentry_setAbstract (uentry p_e) /*@modifies p_e@*/ ; extern void uentry_setConcrete (uentry p_e) /*@modifies p_e@*/ ; extern void uentry_setHasNameError (uentry p_ue) /*@modifies p_ue@*/ ; -extern /*@falsenull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e); +extern /*@falsewhennull@*/ bool uentry_isLset (/*@sef@*/ uentry p_e); # define uentry_isLset(e) \ (uentry_isValid(e) && (e)->lset) -extern /*@falsenull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e); +extern /*@falsewhennull@*/ bool uentry_isUsed (/*@sef@*/ uentry p_e); # define uentry_isUsed(e) (uentry_isValid(e) && (e)->used) -extern /*@unused@*/ /*@falsenull@*/ bool +extern /*@unused@*/ /*@falsewhennull@*/ bool uentry_isAbstractType (uentry p_e) /*@*/ ; # define uentry_isAbstractType(e) (uentry_isAbstractDatatype(e)) -extern /*@falsenull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isConstant(e) \ (uentry_isValid(e) && ekind_isConst ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEitherConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isEitherConstant(e) \ (uentry_isValid(e) && (ekind_isConst ((e)->ukind) || ekind_isEnumConst ((e)->ukind))) -extern /*@falsenull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEnumConstant (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isEnumConstant(e) \ (uentry_isValid(e) && ekind_isEnumConst ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExternal (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isExternal(c) \ (uentry_isValid(c) && fileloc_isExternal (uentry_whereDefined (c))) -extern /*@falsenull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExtern (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isExtern(c) \ (uentry_isValid(c) && (c)->storageclass == SCEXTERN) extern bool uentry_isForward (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isFunction (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isFunction(e) \ (uentry_isValid(e) && ekind_isFunction ((e)->ukind)) -extern /*@falsenull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isPriv (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isPriv(e) \ (uentry_isValid(e) && (e)->isPrivate) -extern /*@falsenull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isFileStatic (uentry p_ue) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExported (uentry p_ue) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isStatic (/*@sef@*/ uentry p_e) /*@*/ ; # define uentry_isStatic(c) \ (uentry_isValid(c) && (c)->storageclass == SCSTATIC) @@ -284,49 +284,49 @@ extern /*@observer@*/ fileloc uentry_whereEarliest (uentry p_e) /*@*/ ; extern /*@observer@*/ cstring uentry_rawName (uentry p_e) /*@*/ ; extern /*@observer@*/ fileloc uentry_whereDeclared (uentry p_e) /*@*/ ; extern bool uentry_equiv (uentry p_p1, uentry p_p2) /*@*/ ; -extern /*@falsenull@*/ bool uentry_hasName (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_hasName (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_hasRealName (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAbstractDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAnyTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isCodeDefined (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isDeclared (/*@special@*/ uentry p_e) /*@uses p_e->whereDeclared@*/ /*@*/ ; extern /*@observer@*/ cstring uentry_ekindName (uentry p_ue) /*@*/ ; extern /*@observer@*/ cstring uentry_ekindNameLC (uentry p_ue) /*@*/ ; extern void uentry_showWhereDefined (uentry p_spec); -extern /*@falsenull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isEndIter (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isEnumTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isIter (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isParam (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) +extern /*@falsewhennull@*/ bool uentry_isFakeTag (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isIter (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isMutableDatatype (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isParam (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isExpandedMacro (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isSefParam (uentry p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isAnyParam (/*@special@*/ uentry p_u) /*@uses p_u->ukind, p_u->info@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isRealFunction (uentry p_e) /*@*/ ; +extern /*@falsewhennull@*/ bool uentry_isSpecified (uentry p_e) /*@*/ ; -extern /*@falsenull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isStructTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue) +extern /*@falsewhennull@*/ bool uentry_isUnionTag (/*@special@*/ uentry p_ue) /*@uses p_ue->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isVar (/*@special@*/ uentry p_e) /*@uses p_e->ukind@*/ /*@*/ ; -extern /*@falsenull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) +extern /*@falsewhennull@*/ bool uentry_isVariable (/*@special@*/ uentry p_e) /*@uses p_e->ukind@*/ /*@*/ ; diff --git a/src/Headers/uentryList.h b/src/Headers/uentryList.h index 7aae25b..c736e16 100644 --- a/src/Headers/uentryList.h +++ b/src/Headers/uentryList.h @@ -34,10 +34,10 @@ extern /*@only@*/ uentryList uentryList_makeMissingParams (void); # define uentryList_makeMissingParams() uentryList_missingParams -extern /*@truenull@*/ bool uentryList_isMissingParams (uentryList p_s) /*@*/ ; -extern /*@truenull@*/ bool uentryList_isUndefined (uentryList p_s) /*@*/ ; -extern /*@unused@*/ /*@truenull@*/ bool uentryList_isEmpty (uentryList p_s) /*@*/ ; -extern /*@unused@*/ /*@falsenull@*/ bool uentryList_isDefined (uentryList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool uentryList_isMissingParams (uentryList p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool uentryList_isUndefined (uentryList p_s) /*@*/ ; +extern /*@unused@*/ /*@nullwhentrue@*/ bool uentryList_isEmpty (uentryList p_s) /*@*/ ; +extern /*@unused@*/ /*@falsewhennull@*/ bool uentryList_isDefined (uentryList p_s) /*@*/ ; # define uentryList_isEmpty(s) (uentryList_size(s) == 0) diff --git a/src/Headers/usymIdSet.h b/src/Headers/usymIdSet.h index 4ec5cdf..2e2b115 100644 --- a/src/Headers/usymIdSet.h +++ b/src/Headers/usymIdSet.h @@ -43,10 +43,10 @@ extern /*@only@*/ usymIdSet /*@constant null usymIdSet usymIdSet_undefined; @*/ # define usymIdSet_undefined ((usymIdSet) NULL) -extern /*@falsenull@*/ bool usymIdSet_isDefined (usymIdSet p_s) /*@*/ ; +extern /*@falsewhennull@*/ bool usymIdSet_isDefined (usymIdSet p_s) /*@*/ ; # define usymIdSet_isDefined(s) ((s) != usymIdSet_undefined) -extern /*@truenull@*/ bool usymIdSet_isUndefined (usymIdSet p_s) /*@*/ ; +extern /*@nullwhentrue@*/ bool usymIdSet_isUndefined (usymIdSet p_s) /*@*/ ; # define usymIdSet_isUndefined(s) ((s) == usymIdSet_undefined) /*@iter usymIdSet_elements (sef usymIdSet u, yield usymId el); @*/ diff --git a/src/Headers/usymtab-branch.h b/src/Headers/usymtab-branch.h index 2eae7a3..9401643 100644 --- a/src/Headers/usymtab-branch.h +++ b/src/Headers/usymtab-branch.h @@ -414,7 +414,7 @@ extern void usymtab_popCaseBranch (void) /*@constant int functionScope;@*/ # define functionScope 3 -extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ; /*@constant null usymtab usymtab_undefined; @*/ # define usymtab_undefined ((usymtab)NULL) diff --git a/src/Headers/usymtab.h b/src/Headers/usymtab.h index 09840ae..e6a5ada 100644 --- a/src/Headers/usymtab.h +++ b/src/Headers/usymtab.h @@ -394,7 +394,7 @@ extern void usymtab_popCaseBranch (void) /*@constant int functionScope;@*/ # define functionScope 3 -extern /*@falsenull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ; +extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ; /*@constant null usymtab usymtab_undefined; @*/ # define usymtab_undefined ((usymtab)NULL) diff --git a/src/Headers/valueMatrix.h b/src/Headers/valueMatrix.h index d7efcbe..aff4e61 100644 --- a/src/Headers/valueMatrix.h +++ b/src/Headers/valueMatrix.h @@ -21,10 +21,10 @@ abst_typedef genericTable valueMatrix; /*@constant null valueMatrix valueMatrix_undefined; @*/ # define valueMatrix_undefined genericTable_undefined -extern /*@falsenull@*/ bool valueMatrix_isDefined(valueMatrix) /*@*/ ; +extern /*@falsewhennull@*/ bool valueMatrix_isDefined(valueMatrix) /*@*/ ; # define valueMatrix_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) -extern /*@truenull@*/ bool valueMatrix_isUndefined(valueMatrix) /*@*/ ; +extern /*@nullwhentrue@*/ bool valueMatrix_isUndefined(valueMatrix) /*@*/ ; # define valueMatrix_isUndefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) extern /*@only@*/ valueMatrix valueMatrix_create(int p_size); diff --git a/src/Headers/valueTable.h b/src/Headers/valueTable.h index 6860e3c..f188920 100644 --- a/src/Headers/valueTable.h +++ b/src/Headers/valueTable.h @@ -17,10 +17,10 @@ /*@constant null valueTable valueTable_undefined; @*/ # define valueTable_undefined genericTable_undefined -extern /*@falsenull@*/ bool valueTable_isDefined(valueTable) /*@*/ ; +extern /*@falsewhennull@*/ bool valueTable_isDefined(valueTable) /*@*/ ; # define valueTable_isDefined(p_h) (genericTable_isDefined ((genericTable) (p_h))) -extern /*@truenull@*/ bool valueTable_isUndefined(valueTable) /*@*/ ; +extern /*@nullwhentrue@*/ bool valueTable_isUndefined(valueTable) /*@*/ ; # define valueTable_isUndefined(p_h) (genericTable_isUndefined ((genericTable) (p_h))) extern /*@only@*/ valueTable valueTable_create(int p_size); diff --git a/src/Headers/warnClause.h b/src/Headers/warnClause.h index 4f41bb0..bb3d1d9 100644 --- a/src/Headers/warnClause.h +++ b/src/Headers/warnClause.h @@ -20,8 +20,8 @@ struct s_warnClause /*@constant null warnClause warnClause_undefined; @*/ # define warnClause_undefined ((warnClause) NULL) -extern /*@falsenull@*/ bool warnClause_isDefined (/*@null@*/ warnClause p_f) /*@*/ ; -extern /*@truenull@*/ bool warnClause_isUndefined (/*@null@*/ warnClause p_f) /*@*/ ; +extern /*@falsewhennull@*/ bool warnClause_isDefined (/*@null@*/ warnClause p_f) /*@*/ ; +extern /*@nullwhentrue@*/ bool warnClause_isUndefined (/*@null@*/ warnClause p_f) /*@*/ ; # define warnClause_isDefined(f) ((f) != warnClause_undefined) # define warnClause_isUndefined(f) ((f) == warnClause_undefined) @@ -37,7 +37,7 @@ extern /*@observer@*/ flagSpec warnClause_getFlag (warnClause p_w) /*@*/ ; extern /*@only@*/ cstring warnClause_dump (warnClause p_wc) /*@*/ ; extern /*@only@*/ warnClause warnClause_undump (char **p_s) /*@modifies p_s@*/ ; -extern /*@falsenull@*/ bool warnClause_hasMessage (warnClause p_w) /*@*/ ; +extern /*@falsewhennull@*/ bool warnClause_hasMessage (warnClause p_w) /*@*/ ; extern /*@observer@*/ cstring warnClause_getMessage (warnClause p_w) /*@*/ ; extern /*@only@*/ cstring warnClause_unparse (warnClause p_w) /*@*/ ; diff --git a/src/cscanner.l b/src/cscanner.l index aac8219..d20f4f3 100644 --- a/src/cscanner.l +++ b/src/cscanner.l @@ -288,6 +288,8 @@ L\"(\\.|[^\\"])*\"([ \t\n]*\"(\\.|[^\\"])*\")* { RETURN_EXPR (processWideString "isnull" { return (processSpec (QISNULL)); } "truenull" { return (processSpec (QTRUENULL)); } "falsenull" { return (processSpec (QFALSENULL)); } +"nullwhentrue" { return (processSpec (QTRUENULL)); } +"nullwhenfalse" { return (processSpec (QFALSENULL)); } "relnull" { return (processSpec (QRELNULL)); } "reldef" { return (processSpec (QRELDEF)); } "exposed" { return (processSpec (QEXPOSED)); } @@ -632,6 +634,8 @@ struct skeyword s_keytable[] = { { "special", QSPECIAL } , { "truenull", QTRUENULL } , { "falsenull", QFALSENULL } , + { "nullwhentrue", QTRUENULL } , + { "falsewhennull", QFALSENULL } , { "keep", QKEEP } , { "kept", QKEPT } , { "notnull", QNOTNULL } , diff --git a/src/cstringTable.c b/src/cstringTable.c index 1fb90c1..0f5f970 100644 --- a/src/cstringTable.c +++ b/src/cstringTable.c @@ -44,7 +44,7 @@ static void cstringTable_addEntry (/*@notnull@*/ cstringTable p_h, /*@only@*/ hentry p_e) /*@modifies p_h@*/ ; -static /*@truenull@*/ bool hbucket_isNull (/*@null@*/ hbucket h) +static /*@nullwhentrue@*/ bool hbucket_isNull (/*@null@*/ hbucket h) { return (h == hbucket_undefined); } diff --git a/src/genericTable.c b/src/genericTable.c index 35274e9..e2c00d7 100644 --- a/src/genericTable.c +++ b/src/genericTable.c @@ -35,7 +35,7 @@ /*@constant null ghbucket ghbucket_undefined; @*/ # define ghbucket_undefined 0 -static /*@truenull@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h) +static /*@nullwhentrue@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h) { return (h == ghbucket_undefined); } diff --git a/src/llmain.c b/src/llmain.c index 1d9c6b5..66d9115 100644 --- a/src/llmain.c +++ b/src/llmain.c @@ -1928,12 +1928,12 @@ printAnnotations (void) llmsglit (""); llmsglit ("Null State:"); llmsglit (" /*@null@*/ - possibly null pointer"); - llmsglit (" /*@notnull@*/ - non-null pointer"); + llmsglit (" /*@notnull@*/ - definitely non-null pointer"); llmsglit (" /*@relnull@*/ - relax null checking"); llmsglit (""); llmsglit ("Null Predicates:"); - llmsglit (" /*@truenull@*/ - if result is TRUE, first parameter is NULL"); - llmsglit (" /*@falsenull@*/ - if result is TRUE, first parameter is not NULL"); + llmsglit (" /*@nullwhentrue@*/ - if result is TRUE, first parameter is NULL"); + llmsglit (" /*@falsewhennull@*/ - if result is TRUE, first parameter is not NULL"); llmsglit (""); llmsglit ("Execution:"); llmsglit (" /*@noreturn@*/ - function never returns"); diff --git a/src/sRef.c b/src/sRef.c index 060c91b..9a18b79 100644 --- a/src/sRef.c +++ b/src/sRef.c @@ -588,14 +588,14 @@ static bool && (fileloc_isDefined (s->aliasinfo->loc))); } -static /*@falsenull@*/ bool +static /*@falsewhennull@*/ bool sRef_hasStateInfoLoc (sRef s) { return (sRef_isValid (s) && (s->definfo != NULL) && (fileloc_isDefined (s->definfo->loc))); } -static /*@falsenull@*/ bool +static /*@falsewhennull@*/ bool sRef_hasExpInfoLoc (sRef s) { return (sRef_isValid (s) diff --git a/src/usymtab.c b/src/usymtab.c index 43ab21e..d9073d5 100644 --- a/src/usymtab.c +++ b/src/usymtab.c @@ -193,7 +193,7 @@ static void clearFunctionTypes (void) uentryList_clear (functypes); } -static /*@falsenull@*/ bool usymtab_isBranch (usymtab u) +static /*@falsewhennull@*/ bool usymtab_isBranch (usymtab u) { return (usymtab_isDefined (u) && (u->kind == US_TBRANCH || u->kind == US_FBRANCH -- 2.45.2