src/Headers/metaStateSpecifier.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** metaStateSpecifier.h
   7 */
   8
   9 # ifndef METASTATESPECIFIER_H
  10 # define METASTATESPECIFIER_H
  11
  12 struct s_metaStateSpecifier {
  13   sRef sr;
  14   /*@observer@*/ metaStateInfo msinfo;
  15 } ;
  16
  17 extern metaStateSpecifier
  18 metaStateSpecifier_create (/*@only@*/ sRef, /*@observer@*/ metaStateInfo) ;
  19
  20 extern /*@exposed@*/ sRef metaStateSpecifier_getSref (metaStateSpecifier) /*@*/ ;
  21 extern /*@observer@*/ metaStateInfo metaStateSpecifier_getMetaStateInfo (metaStateSpecifier) /*@*/ ;
  22
  23 extern cstring metaStateSpecifier_unparse (metaStateSpecifier) /*@*/ ;
  24 extern metaStateSpecifier metaStateSpecifier_copy (metaStateSpecifier) /*@*/ ;
  25 extern void metaStateSpecifier_free (/*@only@*/ metaStateSpecifier) ;
  26
  27 # else
  28 # error "Multiple include"
  29 # endif
  30
  31
  32
  33