Updated the copyright on source code files.

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

diff --git a/src/Headers/stateValue.h b/src/Headers/stateValue.h
index 587c060fba3c17b6897cc715ab1c6e8a92106a9d..5f8700dbb39d7cad23c69343babffdf2b9761605 100644 (file)
--- 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