Updated library headers to include some missing functions.

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

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index 63840c90d9fe234cfd5d19a8d0c2bc2151c204ee..67d89532e32037d65a497b88e44b01e4eba6e23e 100644 (file)
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -17,8 +17,7 @@
 
 typedef struct 
 {
-  /*@only@*/ multiVal val;
-            typeIdSet access;
+  typeIdSet access;
 } *ucinfo;
 
 typedef enum 
@@ -166,7 +165,7 @@ struct s_uentry
 /*
 ** There is no uentry_isDefined to avoid confusion with
 ** uentry_isCodeDefined (which was previously called 
-** uentry_isDefined.
+** uentry_isDefined).
 */
 
 extern /*@truenull@*/ bool uentry_isUndefined (/*@special@*/ uentry p_e) 
@@ -458,12 +457,12 @@ extern /*@notnull@*/ /*@only@*/ uentry
 
 # ifndef NOLCL
 extern /*@notnull@*/ /*@only@*/ 
-  uentry uentry_makeVariableParam (cstring p_n, ctype p_t);
+  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, 
-                                      /*@exposed@*/ sRef p_s);
+uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
+                                    /*@exposed@*/ sRef p_s);
 extern /*@notnull@*/ /*@only@*/ 
   uentry uentry_makeIdFunction (idDecl p_id);
 extern /*@notnull@*/ /*@only@*/ 
@@ -546,6 +545,8 @@ extern bool uentry_hasGlobs (uentry p_ue) /*@*/ ;
 extern bool uentry_hasMods (uentry p_ue) /*@*/ ;
 
 extern bool uentry_hasStateClauseList (uentry p_ue) /*@*/ ;
+extern bool uentry_hasConditions (uentry p_ue) /*@*/ ;
+
 extern exitkind uentry_getExitCode (uentry p_ue) /*@*/ ;
 
 extern void uentry_checkYieldParam (uentry p_old, uentry p_unew);
@@ -602,15 +603,11 @@ extern bool uentry_hasAccessType (uentry p_e);
 /*@constant cstring GLOBAL_MARKER_NAME@*/
 # define GLOBAL_MARKER_NAME cstring_makeLiteralTemp ("#GM#")
 
-/* start modifications */
-//extern void uentry_setBufferSize (uentry p_e, exprNode cconstant);
-
 /* functions for making modification to null-term info */
-  void uentry_setNullTerminatedState (uentry p_e);
- void uentry_setPossiblyNullTerminatedState (uentry p_e);
-//extern void uentry_setNotNullTerminated (uentry p_e);
-void uentry_setSize(uentry p_e, int p_size);
- void uentry_setLen(uentry p_e, int p_len);
+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@*/
@@ -639,7 +636,7 @@ extern bool uentry_hasBufStateInfo (uentry p_ue);
 extern uentry uentry_makeGlobalMarker (void) ;
 extern bool uentry_isGlobalMarker (uentry) /*@*/ ;
 
-extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@keep@*/ fileloc p_loc);
+extern /*@exposed@*/ uentry uentry_makeUnrecognized (cstring p_c, /*@only@*/ fileloc p_loc);
 
 # ifdef DOANNOTS
 typedef enum { AN_UNKNOWN, AN_FCNRETURN, AN_FCNPARAM, AN_SUFIELD, AN_TDEFN, AN_GSVAR,
@@ -652,10 +649,10 @@ extern void uentry_tallyAnnots (uentry u, ancontext kind);
 # endif /* DOANNOTS */
 
 extern bool uentry_hasMetaStateEnsures (uentry p_e) /*@*/ ;
-extern /*@observer@*/ metaStateConstraint uentry_getMetaStateEnsures (uentry p_e);
+extern /*@only@*/ metaStateConstraintList uentry_getMetaStateEnsures (uentry p_e);
 
 /* start modifications */
-//extern void uentry_setBufferSize (uentry p_e, exprNode p_cconstant);
+
 /*drl7x*/
 extern constraintList uentry_getFcnPreconditions (uentry p_ue);
 extern constraintList uentry_getFcnPostconditions (uentry p_ue);
@@ -663,8 +660,7 @@ extern constraintList uentry_getFcnPostconditions (uentry p_ue);
 extern void uentry_setPostconditions (uentry p_ue, /*@only@*/ functionConstraint p_postconditions);
 
 extern void uentry_setPreconditions (uentry p_ue, /*@only@*/ functionConstraint p_preconditions);
-
-     /*end mods*/
+/*end mods*/
 
 # else
 # error "Multiple include"