Fixed line numbering when multi-line macro parameters are used.

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

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index 87d5bfb14a4081413deee651d59617539244c54b..0b007f1eee9615308ea2aabd6742d79321ebc828 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -150,8 +150,8 @@ extern void sRef_setNullStateInnerComplete (sRef p_s, nstate p_n, fileloc p_loc)
 extern void sRef_setPosNull (sRef p_s, fileloc p_loc);
 extern void sRef_setDefNull (sRef p_s, fileloc p_loc);
 
-extern /*@truenull@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
+extern /*@nullwhentrue@*/ bool sRef_isInvalid (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isValid (sRef p_s) /*@*/ ;
 
 /*@constant null sRef sRef_undefined; @*/
 # define sRef_undefined    ((sRef) NULL)
@@ -165,11 +165,11 @@ extern bool sRef_isNotNull (sRef p_s) /*@*/ ;
 
 extern bool sRef_isDefinitelyNull (sRef p_s) /*@*/ ;
                                                      
-extern /*@falsenull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isNSLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isRealLocalVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isLocalParamVar (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isKnown (/*@sef@*/ sRef p_s) /*@*/ ;
 
 extern bool sRef_hasLastReference (sRef p_s) /*@*/ ;
 # define sRef_hasLastReference(s) (sRef_hasAliasInfoRef (s))
@@ -202,7 +202,7 @@ extern alkind sRef_getAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 extern alkind sRef_getOrigAliasKind (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_getOrigAliasKind(s) (sRef_isValid(s) ? (s)->oaliaskind : AK_ERROR)
 
-extern /*@falsenull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isConj (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isConj(s)           (sRef_isValid(s) && (s)->kind == SK_CONJ)
 
 extern /*@exposed@*/ sRef sRef_buildArrow (sRef p_s, /*@dependent@*/ cstring p_f);
@@ -234,7 +234,7 @@ extern bool sRef_aliasCompleteSimplePred (bool (p_predf) (sRef), sRef p_s);
 
 extern void sRef_clearExKindComplete (sRef p_s, fileloc p_loc);
 
-extern /*@falsenull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isKindSpecial (/*@sef@*/ sRef p_s) /*@*/ ;
 # define sRef_isKindSpecial(s) (sRef_isValid (s) && (s)->kind == SK_SPECIAL)
 
 extern /*@observer@*/ cstring sRef_nullMessage (sRef p_s) /*@*/ ;
@@ -255,13 +255,13 @@ extern ctype sRef_getType (sRef p_s) /*@*/ ;
 
 extern void sRef_markImmutable (sRef p_s) /*@modifies p_s@*/ ;
 
-extern /*@falsenull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; 
-extern /*@falsenull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
-extern /*@falsenull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isAddress (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isArrayFetch (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isConst (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isCvar (sRef p_s) /*@*/ ; 
+extern /*@falsewhennull@*/ bool sRef_isField (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isParam (sRef p_s) /*@*/ ;
+extern /*@falsewhennull@*/ bool sRef_isPointer (sRef p_s) /*@*/ ;
 
 extern void sRef_setType (sRef p_s, ctype p_t);
 extern void sRef_setTypeFull (sRef p_s, ctype p_t);
@@ -288,8 +288,12 @@ extern /*@only@*/ cstring sRef_unparseDebug (sRef p_s) /*@*/ ;
 extern void sRef_killComplete (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern int sRef_getIndex (sRef p_arr) /*@*/ ;
 extern /*@dependent@*/ sRef sRef_fixOuterRef (/*@returned@*/ sRef p_s);
-extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc);
-extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc);
+
+/* Use this one to clear after error */
+extern void sRef_setDefinedCompleteDirect (sRef p_s, fileloc p_loc) ;
+
+extern void sRef_setDefinedComplete (sRef p_s, fileloc p_loc) ;
+extern void sRef_setDefinedNCComplete (sRef p_s, fileloc p_loc) ;
 extern int sRef_getParam (sRef p_s) /*@*/ ;
 extern int sRef_lexLevel (sRef p_s) /*@*/ ;
 extern void sRef_setOrigAliasKind (sRef p_s, alkind p_kind);
@@ -319,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) /*@*/ ;
 
@@ -329,20 +333,20 @@ extern /*@notnull@*/ /*@exposed@*/ sRef
 extern /*@notnull@*/ /*@dependent@*/ sRef
   sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
 extern /*@notnull@*/ /*@dependent@*/ sRef
-  sRef_makeCvar (int p_level, usymId p_index, ctype p_ct);
+  sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo);
 extern /*@notnull@*/ /*@dependent@*/ sRef
   sRef_makeConst (ctype p_ct);
 extern /*@exposed@*/ sRef
   sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
 extern /*@notnull@*/ /*@dependent@*/ sRef 
-  sRef_makeGlobal (usymId p_l, ctype p_ct);
+  sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo);
 extern /*@exposed@*/ sRef
   sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
 extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef 
   sRef_makeObject (ctype p_o) /*@*/ ;
 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
-extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ;
+extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ;
 extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ;
 extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
 extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;
@@ -401,7 +405,7 @@ extern /*@dependent@*/ sRef sRef_copy (sRef p_s);
 
 extern cstring sRef_unparseState (sRef p_s) /*@*/ ;
 extern ynm sRef_isWriteable (sRef p_s) /*@*/ ;
-extern ynm sRef_isReadable (sRef p_s) /*@*/ ;
+extern ynm sRef_isValidLvalue (sRef p_s) /*@*/ ;
 extern bool sRef_isStrictReadable (sRef p_s) /*@*/ ;
 extern bool sRef_hasNoStorage (sRef p_s) /*@*/ ;
 extern void sRef_showExpInfo (sRef p_s) /*@modifies g_msgstream*/ ;
@@ -424,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) 
@@ -446,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) \
@@ -485,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))
 
@@ -495,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))
 
@@ -641,7 +645,7 @@ extern bool sRef_isNullTerminated(/*@sef@*/sRef p_s);
 
 extern bool sRef_isPossiblyNullTerminated(/*@sef@*/sRef p_s);
 # define sRef_isPossiblyNullTerminated(p_s) \
-   ( sRef_hasBufStateInfo((p_s)) ? ( (p_s)->bufinfo.bufstate \
+   ( sRef_hasBufStateInfo((p_s)) ? ((p_s)->bufinfo.bufstate \
                == BB_POSSIBLYNULLTERMINATED) : FALSE)
 
 extern bool sRef_isNotNullTerminated(/*@sef@*/sRef p_s);
@@ -677,7 +681,21 @@ extern void sRef_setValue (sRef p_s, /*@only@*/ multiVal p_val) /*@modifies p_s@
 extern bool sRef_hasValue (sRef p_s) /*@*/ ;
 extern /*@observer@*/ multiVal sRef_getValue (sRef p_s) /*@*/ ;
 
-extern /*@mayexit@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ;
+extern /*@maynotreturn@*/ void sRef_checkValid (/*@temp@*/ sRef p_s) /*@modifies stderr@*/ ;
+
+extern void
+sRef_aliasSetComplete (void (p_predf) (sRef, fileloc), sRef p_s, fileloc p_loc)
+     /*@modifies p_s@*/ ;
+
+extern void
+sRef_aliasSetCompleteParam (void (p_predf) (sRef, int, fileloc), sRef p_s, 
+                           int p_kind, fileloc p_loc)
+   /*@modifies p_s@*/ ;
+
+extern void
+sRef_aliasSetCompleteAlkParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s, 
+                              alkind p_kind, fileloc p_loc)
+     /*@modifies p_s@*/ ;
 
 # else
 # error "Multiple include"