Add test for #212.

intTests/test_jvm_method_names/Makefile

@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<

intTests/test_jvm_method_names/Test.java

@@ -0,0 +1,29 @@
+class Test
+{
+    long val;
+
+    public Test() {
+        val = 0;
+    }
+    public Test(long x) {
+        val = x;
+    }
+    public Test(int x) {
+        val = x;
+    }
+    public long get() {
+        return val;
+    }
+    public void increment() {
+        val = val + 1;
+    }
+    public void increment(long x) {
+        val = val + x;
+    }
+    public void increment(int x) {
+        val = val + (long)x;
+    }
+    public void increment(Test x) {
+        val = val + x.val;
+    }
+}

intTests/test_jvm_method_names/test.saw

@@ -0,0 +1,94 @@
+enable_experimental;
+c <- java_load_class "Test";
+
+crucible_jvm_verify c "get" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+    jvm_execute_func [this];
+    jvm_return (jvm_term val);
+  }
+  z3;
+
+
+print "********************************************************************************";
+// FIXME: saw-script can't verify constructor functions
+fails (
+crucible_jvm_verify c "Test(L)V" [] 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;
+  }
+  z3);
+
+print "********************************************************************************";
+print "increment";
+fails (
+crucible_jvm_verify c "increment" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+    jvm_execute_func [this];
+    jvm_field_is this "Test.val" (jvm_term {{ val + 1 }});
+  }
+  z3);
+
+print "********************************************************************************";
+print "increment()V";
+crucible_jvm_verify c "increment()V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+    jvm_execute_func [this];
+    jvm_field_is this "Test.val" (jvm_term {{ val + 1 }});
+  }
+  z3;
+
+print "********************************************************************************";
+print "increment(J)V";
+crucible_jvm_verify c "increment(J)V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+    x <- jvm_fresh_var "x" java_long;
+    jvm_execute_func [this, jvm_term x];
+    jvm_field_is this "Test.val" (jvm_term {{ val + x }});
+  }
+  z3;
+
+print "********************************************************************************";
+print "increment(I)V";
+crucible_jvm_verify c "increment(I)V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+    x <- jvm_fresh_var "x" java_int;
+    jvm_execute_func [this, jvm_term x];
+    jvm_field_is this "Test.val" (jvm_term {{ val + sext x }});
+  }
+  z3;
+
+print "********************************************************************************";
+print "increment(LTest;)V";
+crucible_jvm_verify c "increment(LTest;)V" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_field_is this "Test.val" (jvm_term val);
+
+    x <- jvm_alloc_object "Test";
+    x_val <- jvm_fresh_var "x_val" java_long;
+    jvm_field_is x "Test.val" (jvm_term x_val);
+
+    jvm_execute_func [this, x];
+    jvm_field_is this "Test.val" (jvm_term {{ val + x_val }});
+  }
+  z3;

intTests/test_jvm_method_names/test.sh

@@ -0,0 +1 @@
+$SAW test.saw