Extend #212 test to also verify constructor methods.

These are referred to by the name "<init>", which is what they
are called in the JVM class file. Like other methods, they can
be used with type descriptors to disambiguate when constructors
are defined at multiple types.

intTests/test_jvm_method_names/test.saw

@@ -1,5 +1,6 @@
 enable_experimental;
 c <- java_load_class "Test";
+print c;
 
 crucible_jvm_verify c "get" [] false
   do {
@@ -13,18 +14,48 @@ crucible_jvm_verify c "get" [] false
 
 
 print "********************************************************************************";
-// FIXME: saw-script can't verify constructor functions
+print "<init>";
 fails (
-crucible_jvm_verify c "Test(L)V" [] false
+crucible_jvm_verify c "<init>" [] false
   do {
-    x <- jvm_fresh_var "x" java_long;
-    jvm_execute_func [jvm_term x];
     this <- jvm_alloc_object "Test";
-    jvm_field_is this "Test.val" (jvm_term x);
-    jvm_return this;
+    jvm_execute_func [this];
+    jvm_field_is this "Test.val" (jvm_term {{ 0 : [64] }});
   }
   z3);
 
+print "********************************************************************************";
+print "<init>(J)V";
+crucible_jvm_verify c "<init>(J)V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_long;
+    jvm_execute_func [this, jvm_term x];
+    jvm_field_is this "Test.val" (jvm_term x);
+  }
+  z3;
+
+print "********************************************************************************";
+print "<init>(I)V";
+crucible_jvm_verify c "<init>(I)V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    jvm_execute_func [this, jvm_term x];
+    jvm_field_is this "Test.val" (jvm_term {{ sext x : [64] }});
+  }
+  z3;
+
+print "********************************************************************************";
+print "<init>()V";
+crucible_jvm_verify c "<init>()V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_execute_func [this];
+    jvm_field_is this "Test.val" (jvm_term {{ 0 : [64] }});
+  }
+  z3;
+
 print "********************************************************************************";
 print "increment";
 fails (