# include "lclintMacros.nf"
# include "basic.h"
-# include "mtincludes.h"
metaStateSpecifier
metaStateSpecifier_create (/*@only@*/ sRef sr, /*@observer@*/ metaStateInfo msinfo)
return res;
}
+sRef
+metaStateSpecifier_getSref (metaStateSpecifier m)
+{
+ return m->sr;
+}
+
+metaStateInfo
+metaStateSpecifier_getMetaStateInfo (metaStateSpecifier m)
+{
+ return m->msinfo;
+}
+
metaStateSpecifier
metaStateSpecifier_copy (metaStateSpecifier m)
{