extern int f1 (int p[]) /*@modifies nothing @*/ ;
extern int f2 (int p[]) /*@modifies internalState @*/ ;
extern int g2 (int p[]) /*@modifies internalState @*/ ;