file_status (filedesc: INTEGER): INTEGER is
...