extern void inputStream_free (/*@null@*/ /*@only@*/ inputStream p_s);
extern bool inputStream_close (inputStream p_s)
/*@modifies p_s, fileSystem@*/ ;
extern void inputStream_free (/*@null@*/ /*@only@*/ inputStream p_s);
extern bool inputStream_close (inputStream p_s)
/*@modifies p_s, fileSystem@*/ ;