Robust/src/ClassLibrary/File.java

   1 public class File {
   2   String path;
   3   private static final char separator = '\n';
   4
   5   public File(String path) {
   6     this.path=path;
   7   }
   8
   9   String getPath() {
  10     return path;
  11   }
  12
  13   long length() {
  14     return nativeLength(path.getBytes());
  15   }
  16
  17   private static native long nativeLength(byte[] pathname);
  18 }