Add regression test for ?store

Author: Matthias Güdemann

regression/cbmc-java/stack_var10/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_var10/stack_test.class

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

regression/cbmc-java/stack_var10/stack_test.java

@@ -0,0 +1,28 @@
+.class public stack_var10
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; lvar1 is 1, lvar2 is 0
+   iload_1
+   iload_2
+   ;; on stack 1, 0
+   istore_1
+   ;; store 0 into lvar1
+   ireturn
+.end method

regression/cbmc-java/stack_var10/stack_var10.class

@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring