Add regression test for stack variables with typecasts

This regression test mimicks the bytecode that exhibited the error in Tika.

Author: Matthias Güdemann

jbmc/regression/jbmc/stack_var12/stack_typecast.class

@@ -0,0 +1,37 @@
+.class stack_typecast
+.super java/lang/Object
+
+.field public position I
+.field public buffer [B
+
+.method public <init>()V
+        aload_0
+        invokevirtual java/lang/Object/<init>()V
+        return
+.end method
+
+.method public f()I
+        .limit stack 6
+        .limit locals 1
+        .var 0 is this stack_typecast from begin to end
+        .line 0
+begin:
+
+        sipush 255
+
+        aload_0
+        getfield stack_typecast/buffer [B
+
+        aload_0
+        dup
+        getfield stack_typecast/position I
+        dup_x1
+        iconst_1
+        iadd
+        putfield stack_typecast/position I
+        baload
+        iand
+end:
+        ireturn
+
+.end method

jbmc/regression/jbmc/stack_var12/stack_typecast.j

@@ -0,0 +1,17 @@
+CORE
+stack_typecast.class
+--cover location --function stack_typecast.f
+^EXIT=0$
+^SIGNAL=0$
+covered \(100.0%\)
+--
+--
+This tests that there is no invariant violation when modifying the values on the
+stack. in this case the `position` variable is used as index in an array via the
+Java equivalent of
+
+ buffer[position++];
+
+The code pushes position, duplicates it and the modifies the stack
+entry. Before, the stack entry generation removed typecasts which gave a typing
+problem with the `iand` operator