src/Headers/stateValue.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   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   bool implicit;
  21   /*@only@*/ stateInfo info;
  22 };
  23
  24 extern /*@notnull@*/ stateValue stateValue_create (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
  25 extern /*@notnull@*/ stateValue stateValue_createImplicit (int p_value, /*@only@*/ stateInfo p_info) /*@*/ ;
  26
  27 /*@constant null stateValue stateValue_undefined@*/
  28 # define stateValue_undefined (NULL)
  29
  30 extern /*@nullwhentrue@*/ bool stateValue_isUndefined (stateValue) /*@*/ ;
  31 # define stateValue_isUndefined(p_s) ((p_s) == stateValue_undefined)
  32
  33 extern /*@falsewhennull@*/ bool stateValue_isDefined (stateValue) /*@*/ ;
  34 # define stateValue_isDefined(p_s) ((p_s) != NULL)
  35
  36 extern bool stateValue_isImplicit (stateValue) /*@*/ ;
  37
  38 extern int stateValue_getValue (stateValue p_s) /*@*/ ;
  39
  40 extern void stateValue_update (stateValue p_res, stateValue p_val) /*@modifies p_res@*/ ;
  41
  42 extern /*@observer@*/ fileloc stateValue_getLoc (stateValue p_s) /*@*/ ;
  43 # define stateValue_getLoc(p_s) (stateInfo_getLoc (stateValue_getInfo (p_s)))
  44
  45 extern bool stateValue_hasLoc (stateValue p_s) /*@*/ ;
  46
  47 extern /*@observer@*/ stateInfo stateValue_getInfo (stateValue p_s) /*@*/ ;
  48
  49 extern void stateValue_updateValue (/*@sef@*/ stateValue p_s, int p_value, /*@only@*/ stateInfo p_info) /*@modifies p_s@*/ ;
  50
  51 extern void stateValue_updateValueLoc (stateValue p_s, int p_value, fileloc p_loc) /*@modifies p_s@*/ ;
  52
  53 extern void stateValue_show (stateValue p_s, metaStateInfo p_msinfo) ;
  54
  55 extern stateValue stateValue_copy (stateValue p_s) /*@*/ ;
  56
  57 extern /*@only@*/ cstring
  58    stateValue_unparseValue (stateValue p_s, metaStateInfo p_msinfo) /*@*/ ;
  59
  60 extern cstring stateValue_unparse (stateValue p_s) /*@*/ ;
  61
  62 extern bool stateValue_sameValue (stateValue p_s1, stateValue p_s2) /*@*/ ;
  63
  64 extern bool stateValue_isError (/*@sef@*/ stateValue p_s) /*@*/ ;
  65 # define stateValue_isError(p_s) (stateValue_isDefined (p_s) && (stateValue_getValue (p_s) == stateValue_error))
  66
  67 /*@constant int stateValue_error@*/
  68 # define stateValue_error -1
  69
  70 # else
  71 # error "Multiple include"
  72 # endif