*** empty log message ***

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

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index fc0c2ac1e116c4976569cefdf199c721065b0b80..db199e3609663e1126aec4a2c1751c8f177830a2 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 
@@ -418,6 +417,7 @@ extern /*@notnull@*/ /*@only@*/ uentry
 extern /*@notnull@*/ uentry uentry_makeElipsisMarker (void) /*@*/ ;
 
 extern void uentry_makeVarFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
+extern void uentry_makeConstantFunction (/*@temp@*/ uentry p_ue) /*@modifies p_ue@*/ ;
 
 extern bool uentry_isElipsisMarker (/*@sef@*/ uentry p_u) /*@*/ ;
 # define uentry_isElipsisMarker(u) \
@@ -457,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@*/ 
@@ -545,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);
@@ -651,7 +653,7 @@ 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);