Add regression test for getfield, getstatic

Author: Matthias Güdemann

regression/cbmc-java/stack_var8/stack_test.class

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var8 s = new stack_var8();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var8/stack_test.java

@@ -0,0 +1,27 @@
+.class public stack_var8
+.super java/lang/Object
+
+.field private n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_0
+   putfield stack_var8/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   aload_0
+   getfield stack_var8/n I
+   aload_0
+   iconst_1
+   putfield stack_var8/n I
+
+   ireturn
+.end method

regression/cbmc-java/stack_var8/stack_var8.class

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var9 s = new stack_var9();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var8/stack_var8.j

@@ -0,0 +1,24 @@
+.class public stack_var9
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   iconst_0
+   putstatic stack_var9/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   getstatic stack_var9/n I
+   iconst_1
+   putstatic stack_var9/n I
+
+   ireturn
+.end method