// this file is specified as the first argument of ftok() API