Tweaks to disabled test0001

Closer to being able to be re-enabled. Cryptol type checking failures on
MD5 remain.

intTests/test0001/JavaMD5.java

@@ -12,18 +12,17 @@ public static void main(String[] args) throws Exception
     {
         byte[] msg = Symbolic.freshByteArray(16);
 
-	byte[] out = computeMD5( msg );
+        byte[] out = new byte[16];
+
+        computeMD5( msg, out );
 
         Symbolic.writeAiger("JavaMD5.aig", out);
     }
 
-    public static byte[] computeMD5( byte[] msg ) {
-        byte[] out = new byte[16];
+    public static void computeMD5( byte[] msg, byte[] out ) {
         MD5Digest digest = new MD5Digest();
 
         digest.update(msg, 0, msg.length);
         digest.doFinal(out, 0);
-
-	return out;
     }
 }

intTests/test0001/Makefile

@@ -1,2 +1,2 @@
 JavaMD5.class: JavaMD5.java
-	javac -cp ../../deps/jvm-verifier/jars/bcprov-jdk16-145.jar:../../deps/jvm-verifier/jars/galois.jar JavaMD5.java
+	javac -g -cp ../../deps/jvm-verifier/jars/bcprov-jdk16-145.jar:../../deps/jvm-verifier/jars/galois.jar JavaMD5.java

intTests/test0001/javamd5test.saw

@@ -1,9 +1,10 @@
 import "../support/MD5.cry";
 
-let main = do {
-   c <- java_load_class "JavaMD5";
-   java_md5 <- java_extract c "computeMD5" java_pure;
+let md5_spec = do {
+    msg <- java_var "msg" (java_array 16 java_byte);
+    java_var "out" (java_array 16 java_byte);
+    java_ensure_eq "out" {{ md5_ref msg }};
+};
 
-   let thm1 = {{ \x -> md5_ref x == java_md5 x }};
-   prove_print abc thm1;
-};
+c <- java_load_class "JavaMD5";
+java_verify c "computeMD5" [] md5_spec;