]> andersk Git - splint.git/blobdiff - src/Headers/uentry.h
andersk / splint.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Fixed all /*@i...@*/ tags (except 1).
[splint.git] / src / Headers / uentry.h
diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index 1b030a1d541ade5290cbcef2cec43759afde25b6..d60d77f388999ed32e86069a5366b0992bd2a596 100644 (file)
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
 ** See ../LICENSE for license information.
 */
 # ifndef UENTRY_H
@@ -53,7 +53,7 @@ typedef enum  {
   BB_NOTNULLTERMINATED /* buffer is known to be not nullterm */
 } bbufstate;
 
-typedef  struct s_bbufinfo {
+typedef /*@null@*/ struct s_bbufinfo {
   bbufstate bufstate; /* state of the buffer */
   int size;          /* size of the buffer allocated */
   int len;           /* len of the buffer VALID ONLY IF state is NULLTERM */
@@ -72,7 +72,7 @@ typedef struct
 
 typedef struct 
 {
-  ynm   abs;
+  qual abs; /* oneof QU_UNKNOWN, QU_ABSTRACT, QU_NUMABSTRACT, QU_CONCRETE */
   ynm   mut;
   ctype type;
 } *udinfo ;
@@ -118,7 +118,7 @@ typedef struct
 
 typedef struct 
 {
-  typeIdSet   access;
+  typeIdSet access;
 } *ueinfo ;
 
 typedef union
@@ -254,7 +254,7 @@ extern void uentry_setMessageLike (uentry p_ue) /*@modifies p_ue@*/ ;
 extern void uentry_setScanfLike (uentry p_ue) /*@modifies p_ue@*/ ;
 extern void uentry_setPrintfLike (uentry p_ue) /*@modifies p_ue@*/ ;
 
-extern void uentry_checkName (uentry p_ue) /*@modifies g_msgstream, p_ue@*/ ;
+extern void uentry_checkName (uentry p_ue) /*@modifies g_warningstream, p_ue@*/ ;
 
 extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
 # define uentry_sameObject(e1,e2) ((e1) == (e2))
@@ -262,7 +262,7 @@ extern bool uentry_sameObject (uentry p_e1, uentry p_e2);
 extern void uentry_addAccessType (uentry p_ue, typeId p_tid) /*@modifies p_ue@*/ ;
 
 extern void uentry_showWhereAny (uentry p_spec)
-     /*@modifies g_msgstream@*/ ;
+     /*@modifies g_warningstream@*/ ;
 
 extern void uentry_checkParams (uentry p_ue);
 extern void uentry_mergeUses (uentry p_res, uentry p_other);
@@ -354,21 +354,23 @@ extern /*@exposed@*/ sRef uentry_getSref (/*@temp@*/ uentry p_e) /*@*/ ;
 extern /*@observer@*/ sRefSet uentry_getMods (uentry p_l) /*@*/ ;
 extern typeIdSet uentry_accessType (uentry p_e) /*@*/ ;
 extern /*@observer@*/ fileloc uentry_whereEither (uentry p_e) /*@*/ ;
+
+extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
 extern /*@notnull@*/ uentry uentry_makeExpandedMacro (cstring p_s, 
                                                      /*@temp@*/ fileloc p_f)
   /*@*/ ;
 
-extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_msgstream@*/ ;
+extern void uentry_checkMatchParam (uentry p_u1, uentry p_u2, int p_paramno, exprNode p_e) /*@modifies g_warningstream@*/ ;
 
 extern /*@observer@*/ stateClauseList uentry_getStateClauseList (uentry p_ue) /*@*/ ;
 
 extern void uentry_showWhereLastExtra (uentry p_spec, /*@only@*/ cstring p_extra) 
-   /*@modifies g_msgstream@*/ ;
+   /*@modifies g_warningstream@*/ ;
 
-# ifndef NOLCL
 extern void uentry_setRefCounted (uentry p_e);
 
 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype p_t);
+extern /*@falsewhennull@*/ bool uentry_isUnnamedVariable (uentry) /*@*/;
 
 extern /*@notnull@*/ uentry 
   uentry_makeUnspecFunction (cstring p_n, ctype p_t, typeIdSet p_access, 
@@ -394,7 +396,6 @@ extern /*@notnull@*/ uentry
   uentry_makeSpecFunction (cstring p_n, ctype p_t,
                           typeIdSet p_access, /*@only@*/ globSet p_globs, 
                           /*@only@*/ sRefSet p_mods, /*@keep@*/ fileloc p_f);
-# endif
 
 extern /*@notnull@*/ uentry
   uentry_makeEnumConstant (cstring p_n, ctype p_t) /*@*/ ;
@@ -416,11 +417,11 @@ extern /*@notnull@*/ /*@only@*/ uentry
   /*@*/ ;
 
 extern /*@notnull@*/ /*@only@*/ uentry 
-  uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, ynm p_abstract, 
+  uentry_makeDatatype (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, qual p_abstract, 
                       /*@only@*/ fileloc p_f) /*@*/ ;
 extern /*@notnull@*/ /*@only@*/ uentry 
   uentry_makeDatatypeAux (/*@temp@*/ cstring p_n, ctype p_t, ynm p_mut, 
-                         ynm p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
+                         qual p_abstract, /*@keep@*/ fileloc p_f, bool p_priv) /*@*/ ;
 extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
 
 extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
@@ -462,10 +463,8 @@ extern /*@notnull@*/ uentry
 extern /*@notnull@*/ /*@only@*/ uentry 
   uentry_makeVariableLoc (cstring p_n, ctype p_t);
 
-# ifndef NOLCL
 extern /*@notnull@*/ /*@only@*/ 
   uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
-# endif
 
 extern /*@notnull@*/ /*@only@*/ 
 uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
@@ -475,7 +474,7 @@ extern /*@notnull@*/ /*@only@*/
 extern /*@notnull@*/ /*@only@*/ 
   uentry uentry_makeIdDatatype (idDecl p_id);
 extern /*@notnull@*/ /*@only@*/ 
-  uentry uentry_makeBoolDatatype (ynm p_abstract);
+  uentry uentry_makeBoolDatatype (qual p_abstract);
 extern void uentry_mergeDefinition (uentry p_old, /*@only@*/ uentry p_unew);
 extern void uentry_mergeEntries (uentry p_spec, /*@only@*/ uentry p_def);
 extern uentry uentry_nameCopy (/*@only@*/ cstring p_name, uentry p_e);
@@ -486,7 +485,7 @@ extern void uentry_resetParams (uentry p_ue, /*@only@*/ uentryList p_pn)
 extern /*@observer@*/ globSet uentry_getGlobs (uentry p_l) /*@*/ ;
 extern qual uentry_nullPred (uentry p_u);
 extern void uentry_free (/*@only@*/ /*@only@*/ uentry p_e);
-extern void uentry_setDatatype (uentry p_e, usymId p_uid);
+extern void uentry_setDatatype (uentry p_e, typeId p_uid);
 
 extern void uentry_setDefined (/*@special@*/ uentry p_e, fileloc p_f)
    /*@uses p_e->whereDefined, p_e->ukind, p_e->uname, p_e->info@*/
@@ -517,18 +516,19 @@ extern void uentry_setStateClauseList (uentry p_ue, /*@only@*/ stateClauseList p
 extern void uentry_setType (uentry p_e, ctype p_t);
 
 extern /*@unused@*/ /*@observer@*/ cstring uentry_checkedName (uentry p_ue);
-extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_msgstream@*/ ;
+extern void uentry_showWhereLastPlain (uentry p_spec) /*@modifies g_warningstream@*/ ;
 
 extern void 
   uentry_showWhereSpecifiedExtra (uentry p_spec, /*@only@*/ cstring p_s)
-  /*@modifies g_msgstream@*/ ;
+  /*@modifies g_warningstream@*/ ;
 
-extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_msgstream@*/ ; 
-extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_msgstream@*/ ;
-extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_msgstream@*/ ;
+extern void uentry_showWhereSpecified (uentry p_spec) /*@modifies g_warningstream@*/ ; 
+extern void uentry_showWhereLast (uentry p_spec) /*@modifies g_warningstream@*/ ;
+extern void uentry_showWhereDeclared (uentry p_spec) /*@modifies g_warningstream@*/ ;
 
 extern /*@notnull@*/ /*@only@*/ uentry uentry_makeIdVariable (idDecl p_t) /*@*/ ;
 extern uentry uentry_copy (uentry p_e) /*@*/ ;
+extern uentry uentry_copyNoSave (uentry p_e) /*@*/ ; /* for use for uentries that do not live beyond function exits */
 extern void uentry_freeComplete (/*@only@*/ uentry p_e) ;
 extern void uentry_clearDefined (uentry p_e) /*@modifies p_e@*/;
 extern /*@observer@*/ cstring uentry_specDeclName (uentry p_u) /*@*/ ;
@@ -569,7 +569,7 @@ extern alkind uentry_getAliasKind (uentry p_u) /*@*/ ;
 extern exkind uentry_getExpKind (uentry p_u) /*@*/ ;
 extern /*@observer@*/ multiVal uentry_getConstantValue (uentry p_e) /*@*/ ;
 extern void uentry_fixupSref (uentry p_ue) /*@modifies p_ue@*/ ;
-extern void uentry_setGlobals (uentry p_ue, /*@owned@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
+extern void uentry_setGlobals (uentry p_ue, /*@only@*/ globSet p_globs) /*@modifies p_ue, p_globs@*/ ;
 extern bool uentry_isYield (uentry p_ue) /*@*/ ;
 extern /*@notnull@*/ uentry uentry_makeIdConstant (idDecl p_t) /*@*/ ;
 extern /*@observer@*/ cstring uentry_getRealName (uentry p_e) /*@*/ ;
@@ -578,7 +578,7 @@ extern int uentry_xcompareuses (uentry *p_p1, uentry *p_p2) /*@*/ ;
 extern /*@observer@*/ cstring uentry_specOrDefName (uentry p_u) /*@*/ ;
 extern void uentry_copyState (uentry p_res, uentry p_other);
 extern bool uentry_sameKind (uentry p_u1, uentry p_u2);
-extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args);
+extern /*@exposed@*/ sRef uentry_returnedRef (uentry p_u, exprNodeList p_args, fileloc p_loc);
 extern bool uentry_isReturned (uentry p_u);
 extern bool uentry_isRefCountedDatatype (uentry p_e);
 extern sstate uentry_getDefState (uentry p_u);
@@ -610,41 +610,23 @@ extern bool uentry_hasAccessType (uentry p_e);
 /*@constant cstring GLOBAL_MARKER_NAME@*/
 # define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
 
-/* functions for making modification to null-term info */
+/* Null Termination */
+
 extern void uentry_setNullTerminatedState (uentry p_e);
 extern void uentry_setPossiblyNullTerminatedState (uentry p_e);
 extern void uentry_setSize(uentry p_e, int p_size);
 extern void uentry_setLen(uentry p_e, int p_len);
 
-/*@i66*/
-/*@-nullderef@*/
-extern bool uentry_hasBufStateInfo (uentry p_ue);
-# define uentry_hasBufStateInfo(p_ue) \
-  (((p_ue)->info->var->bufinfo != NULL) ? TRUE : FALSE)
-
-/*@unused@*/ extern bool uentry_isNullTerminated(/*@sef@*/uentry p_ue);
-# define uentry_isNullTerminated(p_ue) \
-   ( uentry_hasBufStateInfo((p_ue ) ) ? ((p_ue)->info->var->bufinfo->bufstate \
-               == BB_NULLTERMINATED) : FALSE)
+extern /*@falsewhennull@*/ bool uentry_hasBufStateInfo (uentry p_ue) /*@*/ ;
+extern bool uentry_isNullTerminated (uentry p_ue) /*@*/ ;
+extern bool uentry_isPossiblyNullTerminated (uentry p_ue) /*@*/ ;
+extern bool uentry_isNotNullTerminated (uentry p_ue) /*@*/ ;
 
-/*@unused@*/ extern bool uentry_isPossiblyNullTerminated( /*@sef@*/ uentry p_ue);
-# define uentry_isPossiblyNullTerminated(p_ue) \
-   ( uentry_hasBufStateInfo((p_ue)) ? ((p_ue)->info->var->bufinfo->bufstate \
-               == BB_POSSIBLYNULLTERMINATED) : FALSE)
-
-/*@unused@*/ extern bool uentry_isNotNullTerminated( /*@sef@*/ uentry p_ue);
-# define uentry_isNotNullTerminated(p_ue) \
-   ( uentry_hasBufStateInfo((p_ue) ) ? ((p_ue)->info->var->bufinfo->bufstate \
-               == BB_NOTNULLTERMINATED) : FALSE)
-/*@=nullderef@*/
-
-/* end modifications */
+/* Global Markers */
 
 extern uentry uentry_makeGlobalMarker (void) ;
 extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
 
-extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
-
 # ifdef DOANNOTS
 typedef enum 
 {
@@ -671,6 +653,14 @@ extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint
 extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
 /*end mods*/
 
+/*
+** For debugging only
+*/
+
+# ifdef DEBUGSPLINT
+extern void uentry_checkValid (uentry p_ue) /*@modifies g_errorstream@*/ ; 
+# endif
+
 # else
 # error "Multiple include"
 # endif
git-cvsimport mirror of splint
This page took 0.055058 seconds and 4 git commands to generate.