extern bool context_inFunctionDeclaration (void) /*@globals internalState@*/ ;
extern void context_enterFunctionDeclaration (/*@exposed@*/ uentry) /*@modifies internalState@*/ ;
extern void context_exitFunctionDeclaration (void) /*@modifies internalState@*/ ;
extern bool context_inFunctionDeclaration (void) /*@globals internalState@*/ ;
extern void context_enterFunctionDeclaration (/*@exposed@*/ uentry) /*@modifies internalState@*/ ;
extern void context_exitFunctionDeclaration (void) /*@modifies internalState@*/ ;