Robust/src/ClassLibrary/File.java

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