Add regression test for ?astore

Author: Matthias Güdemann

regression/cbmc-java/stack_var11/README

@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

regression/cbmc-java/stack_var11/stack_test.class

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

regression/cbmc-java/stack_var11/stack_test.java

@@ -0,0 +1,31 @@
+.class public stack_var11
+.super java/lang/Object
+
+.field private arr [I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_2
+   newarray int
+   putfield stack_var11/arr [I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iaload ;; put arr[0] on stack (currently 0)
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iconst_1
+   iastore ;; store 1 in arr[0],
+           ;; value on stack should not be touched
+   ireturn
+.end method