/*@only@*/ abstBodyNode abstbody;
/*@only@*/ abstractNode abstract;
/*@only@*/ exposedNode exposed;
/*@only@*/ abstBodyNode abstbody;
/*@only@*/ abstractNode abstract;
/*@only@*/ exposedNode exposed;
/* taggedUnionNode taggedunion; */
/*@only@*/ globalList globals;
/*@only@*/ constDeclarationNode constdeclaration;
/* taggedUnionNode taggedunion; */
/*@only@*/ globalList globals;
/*@only@*/ constDeclarationNode constdeclaration;