Fixed preds.expect for name change.

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

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index 5b21e32f5a28a510622907256f6d5b5a1d125d68..a5a2684fde5999c7a7056e80d752d0261b0ca22d 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -79,7 +79,7 @@ typedef union
   /*@only@*/ fldinfo  field;
              ctype    object;
   /*@observer@*/ cstring fname; /* unconstrained, new */
-  /*@exposed@*/ /*@notnull@*/ sRef     ref;
+  /*@exposed@*/ /*@notnull@*/ sRef ref;
   /*@only@*/ cjinfo   conj;
              speckind   spec;
 } *sinfo;
@@ -98,6 +98,8 @@ struct s_sRef
   skind kind;
   ctype type;
 
+  multiVal val; /* Some sRef's have known values */
+
   sstate defstate;
   nstate nullstate;
 
@@ -327,20 +329,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@*/ ;
@@ -352,7 +354,7 @@ extern /*@dependent@*/ sRef sRef_makeSpecState (void) /*@*/ ;
 extern /*@dependent@*/ sRef sRef_makeGlobalMarker (void) /*@*/ ;
 extern /*@dependent@*/ sRef sRef_makeSystemState (void) /*@*/ ;
 
-extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (void) /*@*/ ;
+extern /*@dependent@*/ /*@notnull@*/ sRef sRef_makeResult (ctype) /*@*/ ;
 extern /*@exposed@*/ sRef 
   sRef_fixResultType (/*@returned@*/ sRef p_s, ctype p_typ, uentry p_ue)
   /*@modifies p_s@*/;
@@ -671,8 +673,30 @@ extern /*@observer@*/ stateValue sRef_getMetaStateValue (sRef p_s, cstring p_key
 extern bool sRef_checkMetaStateValue (sRef p_s, cstring p_key, int p_value) 
    /*@modifies p_s@*/ ;
 
+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 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"
 # endif