src/Headers/stateValue.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** stateValue.h
   7 */
   8
   9 # ifndef STATEVALUE_H
  10 # define STATEVALUE_H
  11
  12 /*
  13 ** Keeps track of the value of a state variable, as well as tracking
  14 ** information about its history.
  15 */
  16
  17 struct s_stateValue
  18 {
  19   int value;
  20   /*@only@*/ stateInfo info;
  21 };
  22
  23 extern stateValue stateValue_create (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
  24
  25 /*@constant null stateValue stateValue_undefined@*/
  26 # define stateValue_undefined (NULL)
  27
  28 extern /*@truenull@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
  29 # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined)
  30
  31 extern /*@falsenull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
  32 # define stateValue_isDefined(p_s) ((p_s) != NULL)
  33
  34 extern int stateValue_getValue (stateValue p_s) /*@*/ ;
  35
  36 extern void stateValue_update (stateValue p_res, stateValue p_val) /*@modifies p_res@*/ ;
  37
  38 extern /*@observer@*/ fileloc stateValue_getLoc (stateValue p_s) /*@*/ ;
  39 # define stateValue_getLoc(p_s) (stateInfo_getLoc (stateValue_getInfo (p_s)))
  40
  41 extern bool stateValue_hasLoc (stateValue p_s) /*@*/ ;
  42
  43 extern /*@observer@*/ stateInfo stateValue_getInfo (stateValue p_s) /*@*/ ;
  44
  45 extern void stateValue_updateValue (/*@sef@*/ stateValue p_s, int p_value, /*@only@*/ stateInfo p_info) /*@modifies p_s@*/ ;
  46
  47 extern void stateValue_updateValueLoc (stateValue p_s, int p_value, fileloc p_loc) /*@modifies p_s@*/ ;
  48
  49 extern void stateValue_show (stateValue p_s, metaStateInfo p_msinfo) ;
  50
  51 extern stateValue stateValue_copy (stateValue p_s) /*@*/ ;
  52
  53 extern /*@observer@*/ cstring
  54    stateValue_unparseValue (stateValue p_s, metaStateInfo p_msinfo) /*@*/ ;
  55
  56 extern cstring stateValue_unparse (stateValue p_s) /*@*/ ;
  57
  58 extern bool stateValue_sameValue (stateValue p_s1, stateValue p_s2) /*@*/ ;
  59
  60 extern bool stateValue_isError (stateValue p_s) /*@*/ ;
  61 # define stateValue_isError(p_s) (stateValue_getValue (p_s) == stateValue_error)
  62
  63 /*@constant int stateValue_error@*/
  64 # define stateValue_error -1
  65
  66 # else
  67 # error "Multiple include"
  68 # endif