X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/28bf4b0bfd405a2057d865910f8589c54a40f17b..c59f5181c83cf156efc93a26de8f921c927b70ff:/src/Headers/stateValue.h

diff --git a/src/Headers/stateValue.h b/src/Headers/stateValue.h
index 587c060..5f8700d 100644
--- a/src/Headers/stateValue.h
+++ b/src/Headers/stateValue.h
@@ -17,20 +17,24 @@
 struct s_stateValue
 {
   int value;
+  bool implicit;
   /*@only@*/ stateInfo info;
 };
 
-extern stateValue stateValue_create (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
+extern /*@notnull@*/ stateValue stateValue_create (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
+extern /*@notnull@*/ stateValue stateValue_createImplicit (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
 
 /*@constant null stateValue stateValue_undefined@*/
 # define stateValue_undefined (NULL)
 
-extern /*@truenull@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
+extern /*@nullwhentrue@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
 # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined)
 
-extern /*@falsenull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
+extern /*@falsewhennull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
 # define stateValue_isDefined(p_s) ((p_s) != NULL)
 
+extern bool stateValue_isImplicit (stateValue) /*@*/ ;
+
 extern int stateValue_getValue (stateValue p_s) /*@*/ ;
 
 extern void stateValue_update (stateValue p_res, stateValue p_val) /*@modifies p_res@*/ ;
@@ -50,15 +54,15 @@ extern void stateValue_show (stateValue p_s, metaStateInfo p_msinfo) ;
 
 extern stateValue stateValue_copy (stateValue p_s) /*@*/ ;
 
-extern /*@observer@*/ cstring 
+extern /*@only@*/ cstring 
    stateValue_unparseValue (stateValue p_s, metaStateInfo p_msinfo) /*@*/ ;
 
 extern cstring stateValue_unparse (stateValue p_s) /*@*/ ;
 
 extern bool stateValue_sameValue (stateValue p_s1, stateValue p_s2) /*@*/ ;
 
-extern bool stateValue_isError (stateValue p_s) /*@*/ ;
-# define stateValue_isError(p_s) (stateValue_getValue (p_s) == stateValue_error)
+extern bool stateValue_isError (/*@sef@*/ stateValue p_s) /*@*/ ;
+# define stateValue_isError(p_s) (stateValue_isDefined (p_s) && (stateValue_getValue (p_s) == stateValue_error))
 
 /*@constant int stateValue_error@*/ 
 # define stateValue_error -1