From c93cb8cc7bed1999dd8569fd4e18c15214677282 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 17 May 2017 13:13:53 +0200
Subject: [PATCH 1/8] Adapt existing regression tests

---
 regression/cbmc-java/LocalVarTable5/test.desc | 2 +-
 regression/cbmc-java/destructor1/test.desc    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc
index bfe77ab09ad..6f55a0d2bc6 100644
--- a/regression/cbmc-java/LocalVarTable5/test.desc
+++ b/regression/cbmc-java/LocalVarTable5/test.desc
@@ -4,7 +4,7 @@ test.class
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
-dead new_tmp0
+dead new_tmp[0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc
index 53856821b22..32dea0b83f5 100644
--- a/regression/cbmc-java/destructor1/test.desc
+++ b/regression/cbmc-java/destructor1/test.desc
@@ -5,4 +5,4 @@ Break.class
 ^SIGNAL=0$
 dead i;
 --
-GOTO 10
+GOTO 11

From 4c173773cd77b095c7cd704c3ccb1ce9fbbf7d11 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 17 May 2017 18:44:12 +0200
Subject: [PATCH 2/8] Add regression tests for `iload`, `dup`, `dup_x1`,
 `dup_x2`

---
 .../cbmc-java/stack_var1/stack_test.class     | Bin 0 -> 603 bytes
 .../cbmc-java/stack_var1/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var1/stack_var1.class     | Bin 0 -> 205 bytes
 regression/cbmc-java/stack_var1/stack_var1.j  |  22 +++++++++++
 regression/cbmc-java/stack_var1/test.desc     |   9 +++++
 .../cbmc-java/stack_var2/stack_test.class     | Bin 0 -> 603 bytes
 .../cbmc-java/stack_var2/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var2/stack_var2.class     | Bin 0 -> 206 bytes
 regression/cbmc-java/stack_var2/stack_var2.j  |  25 ++++++++++++
 regression/cbmc-java/stack_var2/test.desc     |   9 +++++
 .../cbmc-java/stack_var3/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var3/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var3/stack_var3.class     | Bin 0 -> 210 bytes
 regression/cbmc-java/stack_var3/stack_var3.j  |  33 ++++++++++++++++
 regression/cbmc-java/stack_var3/test.desc     |   9 +++++
 .../cbmc-java/stack_var4/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var4/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var4/stack_var4.class     | Bin 0 -> 214 bytes
 regression/cbmc-java/stack_var4/stack_var4.j  |  37 ++++++++++++++++++
 regression/cbmc-java/stack_var4/test.desc     |  10 +++++
 20 files changed, 182 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var1/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var1/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var1/stack_var1.class
 create mode 100644 regression/cbmc-java/stack_var1/stack_var1.j
 create mode 100644 regression/cbmc-java/stack_var1/test.desc
 create mode 100644 regression/cbmc-java/stack_var2/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var2/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var2/stack_var2.class
 create mode 100644 regression/cbmc-java/stack_var2/stack_var2.j
 create mode 100644 regression/cbmc-java/stack_var2/test.desc
 create mode 100644 regression/cbmc-java/stack_var3/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var3/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var3/stack_var3.class
 create mode 100644 regression/cbmc-java/stack_var3/stack_var3.j
 create mode 100644 regression/cbmc-java/stack_var3/test.desc
 create mode 100644 regression/cbmc-java/stack_var4/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var4/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var4/stack_var4.class
 create mode 100644 regression/cbmc-java/stack_var4/stack_var4.j
 create mode 100644 regression/cbmc-java/stack_var4/test.desc

diff --git a/regression/cbmc-java/stack_var1/stack_test.class b/regression/cbmc-java/stack_var1/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..2b723f49df870f126175f4745f10edd16c3ee9ff
GIT binary patch
literal 603
zcmYLG+e#xr5IvQd$t2@wV!XwBye&~d5qw)+6fYn|eMk`02k9iOw8qKOGx1;a2Yl8A
z1%=&r|7peQQInUdnyS<1oT_<yfB6ew6+b+9$h#Q!kU-vqku*{mbus24X(r<yCNSxu
zK<JwlVJLN^nnAd&LQ!qVI)P3I$u$+I=oi5%&L0u%t!7;kG9?wrgVuFb>WTsL;997F
zFjzb-U5XpA+z`RVayil}xcF%vc9$bjyV@7OV?5g;q}FPUFLJNkZ0VZZRfZ}P8t7Rh
z!)VEH`RGOu!TW6A2)*KC3e!Hi;1lv4xy|n#cC>El_6tMgV#dcT<_Osi{;+x}YZ32x
z&i;#g^Lwn_nQk@sCcIHyhDytNo17PkT0G!`oUo4+pBbQR-q_*F0xydmjv4+M=S-ZP
zg=f%%0V2yW88-=O^diT#fmZkzS)8X{kvM*aRa&&4V6Q*IxkF~`7G1AMa^L-DXc93^
z4mQ^od$3v2L4k?;xRVC`N5Mru9~lE}Gpn&G(3?v=A$<qezK3o7fzx69HfC5HB>W9y
Je=rst`T*Q;Z!iD=

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var1/stack_test.java b/regression/cbmc-java/stack_var1/stack_test.java
new file mode 100644
index 00000000000..cb404e89473
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var1 s = new stack_var1();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var1/stack_var1.class b/regression/cbmc-java/stack_var1/stack_var1.class
new file mode 100644
index 0000000000000000000000000000000000000000..67a2f73308153e8e628076a4f5bbcf0aa989b302
GIT binary patch
literal 205
zcmX^0Z`VEs1_nI_J}w3x1~x_pfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK!{z
zHk-`6%o00x1}+{376xuc1{UZ16reayaY<rwc6?c4k)d7|BLia^P#;2wk%3u5GmM>q
z38-GfQ`3_{k%1Lx9|$lp0L2)%fh0SSCkUh&fi$bub_T|cAbB8{lYtj1Eeur71QcVJ
SZee7UPFVw0zzn3B7&rhN*dQPP

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var1/stack_var1.j b/regression/cbmc-java/stack_var1/stack_var1.j
new file mode 100644
index 00000000000..a3736df18e2
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_var1.j
@@ -0,0 +1,22 @@
+.class public stack_var1
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 2
+   .limit locals 2
+
+   ;; copy of arg on stack
+   iload_1
+   ;; increment arg
+   iinc 1 1
+   ;; incremented copy on stack
+   iload_1
+   isub
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var1/test.desc b/regression/cbmc-java/stack_var1/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/test.desc
@@ -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
diff --git a/regression/cbmc-java/stack_var2/stack_test.class b/regression/cbmc-java/stack_var2/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..f26c64d43d442b1b3eb400c73afb3ddf95ec262d
GIT binary patch
literal 603
zcmYLG+e#xr5IvQd$t2@wV!XwBye&~dL3~?X6fYn|eMk`02k9iOw8qKOGx1;a2Yl8A
z1%=&r|7peQQInUdnyS<1oT_<yfB6ew6+b+9$h#Q!kU-vqku*{mbus24X(r<yCNSxu
zK<JwlVJLN^nnAd&LQ!qVI)P3I$u$+I=oi5%&L0u%t!7;kG9?wrgVuFb>WTsL;997F
zFjzb-U5XpA+z`RVayil}xcF%vc9$bjyV@7OV?5g;q}FPUFLJNkZ0VZZRfZ}P8t7Rh
z!)VEH`RGOu!TW6A2)*KC3e!Hi;1lv4xy|n#cC>El_6tMgV#dcT<_Osi{;+x}YZ32x
z&i;#g^Lwn_nQk@sCcIHyhDytNo17PkT0G!`oUo4+pBbQR-q_*F0xydmjv4+M=S-ZP
zg=f%%0V2yW88-=O^diT#fmZkzS)8X{kvM*aRa&&4V6Q*IxkF~`7G1AMa^L-DXc93^
z4mQ^od$3v2L4k?;xRVC`N5Mru9~lE}Gpn&G(3?v=A$<qezK3o7fzx69HfC5HB>W9y
Je=rst`T*VMZ!rJ>

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var2/stack_test.java b/regression/cbmc-java/stack_var2/stack_test.java
new file mode 100644
index 00000000000..822716f691c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var2 s = new stack_var2();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var2/stack_var2.class b/regression/cbmc-java/stack_var2/stack_var2.class
new file mode 100644
index 0000000000000000000000000000000000000000..6db13604864ab7dab67c972aee693ea014745c9c
GIT binary patch
literal 206
zcmX^0Z`VEs1_nI_J}w3x1~x_pfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK!{z
zHk-`6%o00x22LIZ76vXx1{UZ16rea`8c<<zNn&z#d|6_V5hDY$hGrNe0}nz-FN>Xl
z38-GfQ`3_{k%1Lx9|$lp0L2)%fFwJRCkUh&fi$bub_T|cAbB8{gMk++EyBPI)WE>N
VAsyMm$S9q%2C9M?NHZ~T0{|qPAbkJ;

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var2/stack_var2.j b/regression/cbmc-java/stack_var2/stack_var2.j
new file mode 100644
index 00000000000..e20a174070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_var2.j
@@ -0,0 +1,25 @@
+.class public stack_var2
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 3
+   .limit locals 2
+
+   ;; push local var1
+   iload_1
+   ;; duplicate
+   dup
+   ;; increment local var1
+   iinc 1 1
+   ;; push local var1
+   iload_1
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var2/test.desc b/regression/cbmc-java/stack_var2/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/test.desc
@@ -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
diff --git a/regression/cbmc-java/stack_var3/stack_test.class b/regression/cbmc-java/stack_var3/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..a42cc9101a1af73622c324983b4fb238d3d1d679
GIT binary patch
literal 601
zcmYLGT~8B16g{`Q+wE=_T3UrFg`#`}Fp&rQCK^qJgrvYjiHZ1NrtQ#7S+-<$%YTtS
z;Io>vi6r>$f6{nowe8EjGxwf3_nbSw{`|NHP{)=J9~Bpmd}L5D;jxDtmR(eRWKCzq
z$0}+r)(GVd5yw&|Y7oWmR4m$|>=Njlklk02N?sGJ?Va}oyD{iWLZPW5c{03eOMPa*
z+_(}dA}nryZ1%;C*b7C}+iN9SMZK5i;an>boy%i!o#I&*A-CTN|C9Tz!BBVPp)yp3
z*g!ueGESZwt^jkGC;0!$H$uM%@B~i-<Pi`mvvF@H9uBk~=;;eX<YGO*1~v)B8UD20
zmz{)tUZnPpc=W8<2ze!Js4HWoWp~QWK9V6fcpv91Bgb0?s8}&-_+){-VxD7xZ!4UM
zv$Hz}eKkN7IcC!$!NUSdd^XS)|B%Ib?GBj_V_3~+BiOIL!MR1D`Wg8<WV!7AG%T5v
zr39PL7E7>sq=Opsmbv1Aew%-Nz$?bXsg`;=6j&(bM(}Ro+FxK>-{H&{C%O!agG}(o
Ks9#J6F8u}Axo+P8

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var3/stack_test.java b/regression/cbmc-java/stack_var3/stack_test.java
new file mode 100644
index 00000000000..7ffc016070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var3 s = new stack_var3();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var3/stack_var3.class b/regression/cbmc-java/stack_var3/stack_var3.class
new file mode 100644
index 0000000000000000000000000000000000000000..9a3a0d6d370504ddb033f4faf67779296d1bff03
GIT binary patch
literal 210
zcmX^0Z`VEs1_nI_J}w3x26jdUfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK$uO
zE=C46o6Nk-5<5l)W(`eG9tKthZbk+c=lqmZMh3<-pz`99#N_Pwvcw`|u#zx#1|~)Z
z9)ze~7K0)K3(z_cU}9hdnE)g?fILAU%?PAfwYD=bZUo5#xtt7aP-#h^Qf8nSFN+Pc
Vt&DV33*-Orlr>OgAPFW0UI2KPA{+n!

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var3/stack_var3.j b/regression/cbmc-java/stack_var3/stack_var3.j
new file mode 100644
index 00000000000..f215d15b4bc
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_var3.j
@@ -0,0 +1,33 @@
+.class public stack_var3
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 3
+
+   ;; 1->var1
+   ;; 0->var2
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+   ;; dup var1
+   dup_x1
+   ;; sub one from var1
+   iinc 1 -1
+   ;; pop first var1
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var3/test.desc b/regression/cbmc-java/stack_var3/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/test.desc
@@ -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
diff --git a/regression/cbmc-java/stack_var4/stack_test.class b/regression/cbmc-java/stack_var4/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..cfbb80f78e82daf472877b6c3716d8ca38a8d564
GIT binary patch
literal 601
zcmYLG%T60X5Ulp@dhKPwuRt7LHctVO;Nlx3A|fCm88{drVGd|)4`_^8quDk80zbeR
zkgyb_<eq;DO3x<Pm+qPFn(C^a-)}#D0;piwgNLGvPaYB|nlPD03R5noJtR$M#=|U1
zF3N<$q6kB&Bh?MU?<y3Hj%*RAPDpO4Kt*2(*2?M$!QSb%Bq38(fjsP8H>5r`U~XIs
z6%Zy?&Z=#3D>gbJxZJ2kS_PMz=HX~963wdvaTDWN79q9O?EEM9YTcf0$~|SMGNFN<
zM>34o4VRBmj1jzl<y)aEKISm*V+1~-I2`xw-NUZdT|IbVh+HiASi}+`JH#I~+Oiq3
z&x_dJK93$YcRIWhHq?@#(y}$+W*<?H8@!J?%SiE-0m>GQ8a`QIuNdQ);oA&n;_R&T
zL5~KAEXQPAB&3l;p3eqa;~%m(mtT=M?Zc{meu4ev3C=w-({~toMUu<zFT;|ES@N*?
zY_SBJM>;4mZ-Fam&>!=!A9%$WA84t>LxEgA^@8+0T>AmG^$cgo_^!*aI7s;0M*T!Q
G@Z(?FE^goe

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var4/stack_test.java b/regression/cbmc-java/stack_var4/stack_test.java
new file mode 100644
index 00000000000..1088dd5ac2e
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var4 s = new stack_var4();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var4/stack_var4.class b/regression/cbmc-java/stack_var4/stack_var4.class
new file mode 100644
index 0000000000000000000000000000000000000000..782443dd6e37e3d94704b56bd085a5d86cb32c0b
GIT binary patch
literal 214
zcmX^0Z`VEs1_nI_J}w4c1`b9Bfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK$uO
zZbk;4;*!MV?D(?8A``tVMg}&U%)HDJJ4Oa(4NXrT1~vvBMg|t={FGEi2F5g?ZiH&E
zk}!4#CI&?Y7NB(?z{CJFfq@4|asqjRK$;OqvubT;VB83j2XeU>*rC$046HznKxND}
bEVit6vNF=qEsTue;o)nbN|}K)69X#%T$3T#

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var4/stack_var4.j b/regression/cbmc-java/stack_var4/stack_var4.j
new file mode 100644
index 00000000000..99eecf3794a
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_var4.j
@@ -0,0 +1,37 @@
+.class public stack_var4
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 4
+
+   ;; 0->var1
+   ;; 1->var2
+   ;; 2->var3
+   iconst_0
+   istore_1
+   iconst_1
+   istore_2
+   iconst_2
+   istore_3
+
+   ;; push local var3 / var2 / var1
+   iload_3
+   iload_2
+   iload_1
+   ;; push var1 in front of var3
+   dup_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var4/test.desc b/regression/cbmc-java/stack_var4/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 21cd8a50269269e1ec4ef9af4ca68761b0b13c2a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 12:47:59 +0200
Subject: [PATCH 3/8] Add regression tests for `dup2`, `dup2_x1` and `dup2_x2`

---
 .../cbmc-java/stack_var5/stack_test.class     | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var5/stack_test.java      |   7 +++
 .../cbmc-java/stack_var5/stack_var5.class     | Bin 0 -> 209 bytes
 regression/cbmc-java/stack_var5/stack_var5.j  |  33 ++++++++++++++
 regression/cbmc-java/stack_var5/test.desc     |  10 ++++
 .../cbmc-java/stack_var6/stack_test.class     | Bin 0 -> 609 bytes
 .../cbmc-java/stack_var6/stack_test.java      |   7 +++
 .../cbmc-java/stack_var6/stack_var6.class     | Bin 0 -> 209 bytes
 regression/cbmc-java/stack_var6/stack_var6.j  |  25 ++++++++++
 regression/cbmc-java/stack_var6/test.desc     |  10 ++++
 .../cbmc-java/stack_var7/stack_test.class     | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var7/stack_test.java      |   7 +++
 .../cbmc-java/stack_var7/stack_var7.class     | Bin 0 -> 223 bytes
 regression/cbmc-java/stack_var7/stack_var7.j  |  43 ++++++++++++++++++
 regression/cbmc-java/stack_var7/test.desc     |  10 ++++
 15 files changed, 152 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var5/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var5/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var5/stack_var5.class
 create mode 100644 regression/cbmc-java/stack_var5/stack_var5.j
 create mode 100644 regression/cbmc-java/stack_var5/test.desc
 create mode 100644 regression/cbmc-java/stack_var6/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var6/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var6/stack_var6.class
 create mode 100644 regression/cbmc-java/stack_var6/stack_var6.j
 create mode 100644 regression/cbmc-java/stack_var6/test.desc
 create mode 100644 regression/cbmc-java/stack_var7/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var7/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var7/stack_var7.class
 create mode 100644 regression/cbmc-java/stack_var7/stack_var7.j
 create mode 100644 regression/cbmc-java/stack_var7/test.desc

diff --git a/regression/cbmc-java/stack_var5/stack_test.class b/regression/cbmc-java/stack_var5/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..57cf43dac86c9be13b8ff00a1eb657c9b1e8c1b5
GIT binary patch
literal 602
zcmYLG$xh=y5PcQfabgS!Vau=#VHJx67dWwq5sQSBnK=X@0SDAc8q^_iP}|{SxNzhQ
zNFad(cm4@PwP#2!RpqMJuih)ae?GqgSi!6Z4|x|qJS31eVK|KxMqG?~NSeu*ho2aC
zQ6Th9i!hWrQq3UTQK2Z;WtBk3gygykRJ2L3=H?Fx_I9%>37Mh_<eyffEcJl_^PnMA
zKp31mDb~c5SgwoUe7O{96`Ze`hux(}R4#st%NWnH2&wf-{Xe-^YPNJm?kPi+2@Ui#
zl3}!DxO{Y@hv5BdUkSbHV*-;ty5JM?opryyJ?v`T)a@6B$i<Y8Y0MC^9sJ*NO;#fI
zc^2E-=hdCzcAZbchN?1DT2|ZK>?3ONfbVh4GE#hHfU<d`hARu~6+Ij?{58gzI6DhZ
zpgRLZmSZw*64K~Jj%x!w;6G$>o_Imx=m}PF@e%gMJ)CP~N9`MQy&%bb_s!5GVwxOm
zt}WJJ^G*i^Chp@-8uWpJi+;W_2HIj);;le$F7=4?HC+1^w)Fs~!}u-CusBHgTSoq1
Hym06XN3L%0

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var5/stack_test.java b/regression/cbmc-java/stack_var5/stack_test.java
new file mode 100644
index 00000000000..bfcbe79325d
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var5 s = new stack_var5();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var5/stack_var5.class b/regression/cbmc-java/stack_var5/stack_var5.class
new file mode 100644
index 0000000000000000000000000000000000000000..6230e78a9c70f9c25c79952cb347c499f2c7476e
GIT binary patch
literal 209
zcmX^0Z`VEs1_nI_J}w4c26jdUfvm)`ME#t^ymWp4q^#8B5_SeIMh33n{L-T2RJY8W
zR7M6io6Nk-5<5l)W(`eG9tKth9!3V9;*!MV?D(?8B2&FAMg|t={1l){E`%r}17jLk
zM;JQ;6N4fHGtfE^U}9hdnE)g?fjmJV%?PAfwYD=bZUo5#x!eqFP-zJU79eC`;9;?0
VwUv>MX<=kcSp!uC5@%xI004QJAkY8+

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var5/stack_var5.j b/regression/cbmc-java/stack_var5/stack_var5.j
new file mode 100644
index 00000000000..0871fb68e0b
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_var5.j
@@ -0,0 +1,33 @@
+.class public stack_var5
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 4
+   .limit locals 4
+
+   ;; 1->var1
+   ;; 2->var2
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+
+   ;; duplicate var2 / var1
+   dup2
+   ;; add one to local var 1
+   iinc 1 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var5/test.desc b/regression/cbmc-java/stack_var5/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var6/stack_test.class b/regression/cbmc-java/stack_var6/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c5e765b667b216837c87a0f91d562994b70d598a
GIT binary patch
literal 609
zcmYLF%T60X5UjTM<z>NZI}j(~jX{P;a6!31A|gm6OHMdAig+B**dEY;y+*TZK88z<
zIYT6nKuYfUCs2AeU|+gtx~r?J`tRf2Zvg99^5LWG;+2mK$|k(d!NVIDlRg~Nnes7>
z85gsJQbokE)QRdv@s5f`vm@ICIv_ZkDpJV@Lbkg6onUSE+LDm3t4MzBcbigwGhl9X
zg^CCh)x-L!xDaa{5uL0x60M?>4Kp~}NJQ)Gi#Sj5EQ{c6wmMJbexujdE%{j)s(fsq
zM~RG+Rl^lv6k`PcfB8b_cLC-wA7BIlp*&po@!7*Ct$TVfVTfET1gKz<5DxLX%~RP*
z*yl0(tk!C^<r;4v_P0BH753DYvC^_Vpl2&dpBsFV16Jbkp#ciZMi9TUV7nOOnCIUV
zXX0$H+=8wQ5Ftk=EfR7lpvZ3n-Gjx$z~VhJ`?tu}-&(eN1MB@Y>`N3T!^a;Oxrf6&
z_m82<q*O&7Gh02*A#Aqkpv09N=m8ZMFZk3L9|&4cHv@&DcZ1v|T<a&S>@V0u#%FPc
P#YQIBG8QJ%g)jdBRe5m#

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var6/stack_test.java b/regression/cbmc-java/stack_var6/stack_test.java
new file mode 100644
index 00000000000..392d200d370
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var6 s = new stack_var6();
+    int n = s.f(1,2,4);
+    assert(n==-2);
+  }
+}
diff --git a/regression/cbmc-java/stack_var6/stack_var6.class b/regression/cbmc-java/stack_var6/stack_var6.class
new file mode 100644
index 0000000000000000000000000000000000000000..05223a9a3491806a31721a208b1f93e2b01c7847
GIT binary patch
literal 209
zcmX^0Z`VEs1_nI_J}w4c26jdUfvm)`ME#t^ymWp4q^#8B5_Sd-Mh33n{L-T2RJY8W
zR7M6i4Np%`O-~@hCNnRy#Eyr7je!TKrnn?AIXk{AvB->(fyFsL1*nuUjgf%|A+DFj
z$iS?j8OF}Q#GuH)473phm>7UYG4KFMP9RSZNHYRyR;}#}j2l7nKrR;pD^yyPfdj~9
XVBnONk&SI(VoX^BRl)+KnHabMum2%U

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var6/stack_var6.j b/regression/cbmc-java/stack_var6/stack_var6.j
new file mode 100644
index 00000000000..19108f70e36
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_var6.j
@@ -0,0 +1,25 @@
+.class public stack_var6
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(III)I
+   .limit stack 8
+   .limit locals 5
+
+   ;; push local var3 / var2 / var1
+   iload_1
+   iload_2
+   iload_3
+   dup2_x1
+   ;; add one to local var 2
+   iinc 2 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var6/test.desc b/regression/cbmc-java/stack_var6/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var7/stack_test.class b/regression/cbmc-java/stack_var7/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..21eabe9a02937bf489e793fa085732d5b0d3458a
GIT binary patch
literal 602
zcmYLG$xh=y5PcQfabgS!Vau=#VHJx67bFfWV#FdLWo8aRNWcMgk_L519MpFB7%m(+
z0}@Ce!JU5sQSBL$OI5k*^{e;F@1M`F09G*T!9(7~4-X0CO&Crig%KB{9+GA<=HVyC
zT@(m?(;^I|j#M)UcT_0Kby+3QF(J9G0u^l%thxC^g1z0WN<yZn0{N%aC`)}{z&vOO
z6%YpJPKq^gC6?<VIA1PBS_S88=3#d!5|xYJ;xfjwEJA9%QvXlxm6|PGk$cKeWkLfz
zjbs=t87?2)=plIj+E+ra`k26^k1qIxd}rOSZx6d#H+B1kA#yS0V;VDrYzP0hT$7cE
zeV)bk_IY(@xLxOyu%W69m6p{uH~WZMJm7mAvy2p98K7+5sNu>2dqoe&41bMrCeF^n
z6X?zWk>!|-n}jrak>lDx5BLvRoF`t8IC_FrTzrJRaS!Jj*-`rjT`x#--+ePQiI^q_
zn`?_T*u2w0fr<OLlLmdD;G&;zjDfb8m3S-An@c?+eGS*Xg>5~+=`el^Gb|1g{+5wH
I7%v?90!o^0@&Et;

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var7/stack_test.java b/regression/cbmc-java/stack_var7/stack_test.java
new file mode 100644
index 00000000000..b742878507e
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var7 s = new stack_var7();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var7/stack_var7.class b/regression/cbmc-java/stack_var7/stack_var7.class
new file mode 100644
index 0000000000000000000000000000000000000000..dcc6f0fc1b69c6dd2f0dcbdff3743f465247f4ce
GIT binary patch
literal 223
zcmX^0Z`VEs1_nI_J}w4c26lD^4n_unti-ZJ{hY+SbbbG%tkmQZMh33n{L-T2RJY8W
zR7M6io6Nk-5<5l)W(`eG9tKthZlHqVlEmcf__D+zb4CUh=lm3)I>t1xk}yUF9)zr3
z7CQqogCYYH&^i!cVqgTB03<nqJV7AM2&7rHwlgqp1jz%rTnubbX*C88pkf9FDHa=6
hTXs7E4l@=}7Fiil#<&(n#&94=Sp(I>0;HK3cmOiDBN_kz

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var7/stack_var7.j b/regression/cbmc-java/stack_var7/stack_var7.j
new file mode 100644
index 00000000000..e75f96b833d
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_var7.j
@@ -0,0 +1,43 @@
+.class public stack_var7
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   ;; 1->var1
+   ;; 2->var2
+   ;; 4->var3
+   ;; 8->var4
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+   iconst_4
+   istore_3
+   bipush 8
+   istore 4
+   ;; push local var4 / var3 / var2 / var1
+   iload 4
+   iload_3
+   iload_2
+   iload 1
+   ;; push var2 / var1 in on head
+   dup2_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var7/test.desc b/regression/cbmc-java/stack_var7/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 953fb43acb41879fff754f7c1a85ae45e2255f55 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 19 May 2017 08:25:04 +0200
Subject: [PATCH 4/8] Add regression test for `getfield`, `getstatic`

---
 .../cbmc-java/stack_var8/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var8/stack_test.java      |   7 +++++
 .../cbmc-java/stack_var8/stack_var8.class     | Bin 0 -> 238 bytes
 regression/cbmc-java/stack_var8/stack_var8.j  |  27 ++++++++++++++++++
 .../cbmc-java/stack_var9/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var9/stack_test.java      |   7 +++++
 .../cbmc-java/stack_var9/stack_var9.class     | Bin 0 -> 235 bytes
 regression/cbmc-java/stack_var9/stack_var9.j  |  24 ++++++++++++++++
 8 files changed, 65 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var8/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var8/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var8/stack_var8.class
 create mode 100644 regression/cbmc-java/stack_var8/stack_var8.j
 create mode 100644 regression/cbmc-java/stack_var9/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var9/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var9/stack_var9.class
 create mode 100644 regression/cbmc-java/stack_var9/stack_var9.j

diff --git a/regression/cbmc-java/stack_var8/stack_test.class b/regression/cbmc-java/stack_var8/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..8ea61591cbc2c80a28ea0204557c61307a9141c5
GIT binary patch
literal 601
zcmYLG+e#xr5IvQd$t2@wV!Xv`)O8nk1%2^B@Pgt6gs2Y@L4A-;(i=J(Cri)7f6*WC
zSp@|JefOUft4B><s=BLApE{@d_5JY~z#@Km@Q`;g>>+`?2_tEwFzRB=L(+7{JxrkB
zVv^7|Bf?PXNHv3SONFA`kW~Vm5Rxk@P|+H}n*Du5us54kNyrpcAopA6WvLGhm>cIp
z1%$!b(_&p*h=qm-Y73=EtDv@Q9(I=^QTewg{>ONhMM$kw8eimIsoByMxuXnKCN$8q
zNQTk8;quXq9)kB-z7TrJ#}uZ0bipU&JL5LKJ#1^;)a@6B$i)vIGx$l!cJK$~x~xR(
z^KWc#mq&M+n+;wG8>-4sX<2P^vyZ674c^BI%SiE-0m|l$8a`QIujt{J;oCT8;_Uo+
z0NofMvK*6fk&s3&a(p(>6916JdGZN~;|Ey9xqH~Fw{WhI8M{Q+6OvqZUkpnkX34?k
zv&9l@9_gUKynS3rgWk-)_VbD{(AKgT4+VO2se7ca;M&))tvfg!#&2DQ#X-VfH|huD
GfkPkQ0&e60

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var8/stack_test.java b/regression/cbmc-java/stack_var8/stack_test.java
new file mode 100644
index 00000000000..3a288890e69
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_test.java
@@ -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);
+  }
+}
diff --git a/regression/cbmc-java/stack_var8/stack_var8.class b/regression/cbmc-java/stack_var8/stack_var8.class
new file mode 100644
index 0000000000000000000000000000000000000000..5298a7d8c92c01f7cd2170ae34dac388e7042f0e
GIT binary patch
literal 238
zcmYMuKMR6j5C-t))clv3HMF;tgRTwH5(G{SL2JC3g(eDSeyWzB2pakTeW>V+sO9dS
zm){-l^L2j!@X$5kKqpv-QiS_eC5n-k5S&C*!cRrE^XKa%3QK~y$d5%B&Ehm7P)1P4
zaTb>of;<=o7F4tt{m)ovpiNMw`KDgje%#VP2PVfrgRH?opR>b1AxO37N#dDracy$y
j@hfpR-5bc2udvUYYHvaN8J$&aF0fsN&FO0t?h>Rov)Ur&

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var8/stack_var8.j b/regression/cbmc-java/stack_var8/stack_var8.j
new file mode 100644
index 00000000000..d5bec33279d
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_var8.j
@@ -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
diff --git a/regression/cbmc-java/stack_var9/stack_test.class b/regression/cbmc-java/stack_var9/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..4f20f14f7d17dcc6fb4c1c15290f992bfca428ae
GIT binary patch
literal 601
zcmYLG+e#xr5IvQd$t2@wV!Xv`)O8nk1%2^Fyr6giA?ia!P#>g|^oGvH$<j0NU-Soj
zRzX2Q-~A`W>QR%Is_v@Or_QN<eSdrgu!vtCJmg&rdq^N}!bln^jJg=}kTjif4-+W3
zm?ZSgh%l5oQq3UTQlTg}WR*ZCgyf0}RJ2C0W`7?M?9FCX5;8><$o<xNS?WUr=Ek{D
z0by|Vv{)AxVxb{|+CnMPDyS`+hux(}RQ~OW|1q9r5mGCa#uvF)YPNJm?kGc*2@Uit
zl3_G&xO{Y@hv0pdFN9w5F@<R#UGNF{&bW<l58GNdb^C=Oa`D5*41N-_9sEJLE-MlH
z{2SZb<<XtyW`kG4hN?1DT2|ZK>?3M%gZFX5GE%%{fU<d`hEEpQD|$F)_%_a&I6HqH
zKsN@6EXQPAB&5-c9G?xe#6M(lo_s>$_yJaN?jH8)Eu1T4#xBwIgd~^U7sHZ>S#q%X
zY_SBJM>;4lZy#6Epf~fc{k&ofw6!e8LxJ90>K^GUxb`({>kdwb@mrT+aggxWjrzfO
G;Lr!*cW&hX

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var9/stack_test.java b/regression/cbmc-java/stack_var9/stack_test.java
new file mode 100644
index 00000000000..994e7974026
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_test.java
@@ -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);
+  }
+}
diff --git a/regression/cbmc-java/stack_var9/stack_var9.class b/regression/cbmc-java/stack_var9/stack_var9.class
new file mode 100644
index 0000000000000000000000000000000000000000..1fa90019a0e1341eeef164c58df8b9db5ddc278c
GIT binary patch
literal 235
zcmYL@zY2nI6ot=K%RgCa)C06tgU&&;1c6gS&>FwYLK6iupQ@!Af`%TThl;KtwA}L@
z_zv9n=lKHQqHDl`POxK93NI1q!CP+QFenJdDm&*vxQLRFKq;X)jnb%?5#-^>Czz)~
z1jkJ&@`)R>{;wt)Xq!;bAt>`~SMB$|*_z4MVZ%_NsgN*WcK8$CS3Z-(%yYgiZhdCr
h)W;8ye1~=AQt2j|wbFye5}@5+DQsM7L*|sAegQN$B4q#o

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var9/stack_var9.j b/regression/cbmc-java/stack_var9/stack_var9.j
new file mode 100644
index 00000000000..aeee091def0
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_var9.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

From 0b81ed60c83457cecf7e6568373874994d326ba5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Mon, 22 May 2017 22:02:17 +0200
Subject: [PATCH 5/8] Add regression test for ?store

---
 regression/cbmc-java/stack_var10/README       |   9 ++++++
 .../cbmc-java/stack_var10/stack_test.class    | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var10/stack_test.java     |   7 +++++
 .../cbmc-java/stack_var10/stack_var10.class   | Bin 0 -> 223 bytes
 .../cbmc-java/stack_var10/stack_var10.j       |  28 ++++++++++++++++++
 regression/cbmc-java/stack_var10/test.desc    |   9 ++++++
 6 files changed, 53 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var10/README
 create mode 100644 regression/cbmc-java/stack_var10/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var10/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var10/stack_var10.class
 create mode 100644 regression/cbmc-java/stack_var10/stack_var10.j
 create mode 100644 regression/cbmc-java/stack_var10/test.desc

diff --git a/regression/cbmc-java/stack_var10/README b/regression/cbmc-java/stack_var10/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/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.
diff --git a/regression/cbmc-java/stack_var10/stack_test.class b/regression/cbmc-java/stack_var10/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..09a5b5a8de9728e2557c608895c5c4d37e93ffd3
GIT binary patch
literal 602
zcmYLGT~8BH5Ixh~?Y7&6exSAT)uKR96N^dTM55s%A*u3EV`6<Ex9x>oC|h%P+y7$!
z0MB63CN|M`|C7YItFSLKvomMUoHO_L?T?=T8rbyUq2l7PhZHI%EM}3xl8a>zX){^z
zu!^dS8ew5wgrU@t8U*3K3Pq<cdjx6|(mN_p(JsN-diIH6?+tpAkZ-C$ei&YMr2c5Y
zJh&7pAe6VhG|$CI)cYbhtG6Ppg0t7=$GKJ{x)<-o*BH;T2$`L3|3A6c8Vq$;9x6kX
z4-NDrl411HaQT?SJR$e5JrerWwvRPD@sWd1s3iN|-I+MhdY}nj!sOzqk9BMi3JLzW
zb1u6P8$FHv9r5mDxYy^Ku%n&~m6pAGZZ;APdB6v0vy2R%8K6SNsNu>2o5eiGJb$fl
zCeF_DDd^e&QQ(-4n}jTiC~<9|Eq)@4b8Uvy=P9h_iwW#EH*m(tFMmUBhBUX`Uxp<W
zvy@<SZLtKKS30ON?*ezSpg-neAMlOw@Lo$JUJ4XTnF+FExb_un>pPr;@lKavagg%g
K8ujIP;iJD)jc*PB

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var10/stack_test.java b/regression/cbmc-java/stack_var10/stack_test.java
new file mode 100644
index 00000000000..3831ddea4ab
--- /dev/null
+++ b/regression/cbmc-java/stack_var10/stack_test.java
@@ -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);
+  }
+}
diff --git a/regression/cbmc-java/stack_var10/stack_var10.class b/regression/cbmc-java/stack_var10/stack_var10.class
new file mode 100644
index 0000000000000000000000000000000000000000..68bab7d3abdb396b7b1576ec1431f303e091ed0b
GIT binary patch
literal 223
zcmYj~yAHu{6vn^Pi&igGVq>vkXxYmmk#sUhtnybSt)@+?`cxK^#NYuulsFZG<>dEW
z&N;95;|aipW1tO#V4h16p0<@JrW1nwr`&|#B%%^tDzc-u+9gp~5{z|zDZ*$Or;!GU
zKpCOo$5~v?3G#3hSkPe;ltsReI6i#c4O5^&!2k_@4DcanXfa95yus6C)q%<csN*~6
c#!y!+G=FiIt15fC;>)vM-@pDEwI@OT0M!p63;+NC

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var10/stack_var10.j b/regression/cbmc-java/stack_var10/stack_var10.j
new file mode 100644
index 00000000000..0d6fe63957f
--- /dev/null
+++ b/regression/cbmc-java/stack_var10/stack_var10.j
@@ -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
diff --git a/regression/cbmc-java/stack_var10/test.desc b/regression/cbmc-java/stack_var10/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var10/test.desc
@@ -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

From 936861322cb71a4051b86886921a8c87b61cfa8c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 24 May 2017 18:25:51 +0200
Subject: [PATCH 6/8] Add regression test for ?astore

---
 regression/cbmc-java/stack_var11/README       |   9 +++++
 .../cbmc-java/stack_var11/stack_test.class    | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var11/stack_test.java     |   7 ++++
 .../cbmc-java/stack_var11/stack_var11.class   | Bin 0 -> 249 bytes
 .../cbmc-java/stack_var11/stack_var11.j       |  31 ++++++++++++++++++
 5 files changed, 47 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var11/README
 create mode 100644 regression/cbmc-java/stack_var11/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var11/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var11/stack_var11.class
 create mode 100644 regression/cbmc-java/stack_var11/stack_var11.j

diff --git a/regression/cbmc-java/stack_var11/README b/regression/cbmc-java/stack_var11/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/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.
diff --git a/regression/cbmc-java/stack_var11/stack_test.class b/regression/cbmc-java/stack_var11/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..3d46a551ddc0560b89d3a4c3d9b629942a064101
GIT binary patch
literal 602
zcmYLGT~8BH5Ixh~?Y7%3{Xk2_BB+J%kw{4TMm3tEiAlkS8WZus+_o2Tp=`<BE&oOS
z0MBSb6Pn<=|4HNAg?3+NW@pZxIcM&lf46r48d&q-q3Ys^hZL$NEM}3xQx`Q4X){^!
z@C?f?RtWQT5r$GnY8ZrjDiqy;>=WpakZ!6#MQ;e!`o<T6-5T~Kq0m-=JQ$sIrT%Qd
zJUA07AXL`BwNJ!_*dB=Bc)Js66&&xHAM>3^^iKE1d5mXSgiNzHcp&#W!;$XE56Vy#
zLIeFC$uN3lxP0U>N66i`FNEIN@$noleB|I0s>!~0QxosC9%_P@Fu8c?qmETVF~NW8
zp2%LrMvr2DA9;5&Yz_D(?5Hn8rDcD{%|@aT5BMO5EF;5b2B=syYPhn%W--UHz+X$8
ziL<jg23;E<iX78%laNITWv&gh!%t*!UYQ{EbquS$bp!kLPdJw-)P5j0L7Lm{Z^M#`
zS<0}vwpfDAD;+E|?>u+1pugr}AMuUxc&4QhF9k~F%nh=aaP2GD)-N~-<5ZVnagg%g
K8ugWU;lh7b0&foh

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var11/stack_test.java b/regression/cbmc-java/stack_var11/stack_test.java
new file mode 100644
index 00000000000..59c979f849b
--- /dev/null
+++ b/regression/cbmc-java/stack_var11/stack_test.java
@@ -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);
+  }
+}
diff --git a/regression/cbmc-java/stack_var11/stack_var11.class b/regression/cbmc-java/stack_var11/stack_var11.class
new file mode 100644
index 0000000000000000000000000000000000000000..a19f186ab03cb75f9f6244e32aa884137dcc5967
GIT binary patch
literal 249
zcmYk0zYoE15XIm1r&ddu#Ac&IrMp-p5>p3>#UNi*(h^Oo`d3*bL?Yr3@JET$7%X@9
zUhebmUhn%8fQP0D2PVNuL?QY+vETHAWfFzCjt0S;rpGLd#_=v9Nb?Cn8^rrK9}?tl
zkEMOcMYvrQBJ+JOv0y>9prJ-kM(K(nS!5Z3)+I1AAj8lh5vqS6I&3@q4&V4D@Felf
uF<h&xTI>;b%e{eI^<iF7KePT4HuT?C8<mo+xfj%BudGUN`t2#)B~(62Qzf|o

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var11/stack_var11.j b/regression/cbmc-java/stack_var11/stack_var11.j
new file mode 100644
index 00000000000..16818a4a4e3
--- /dev/null
+++ b/regression/cbmc-java/stack_var11/stack_var11.j
@@ -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

From b5cbb7f030b871dd7ee937d38a9e6ec3161cde7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 19 May 2017 13:52:28 +0200
Subject: [PATCH 7/8] Add README to tests pointing to jasmin bytecode assembler

---
 regression/cbmc-java/stack_var1/README | 9 +++++++++
 regression/cbmc-java/stack_var2/README | 9 +++++++++
 regression/cbmc-java/stack_var3/README | 9 +++++++++
 regression/cbmc-java/stack_var4/README | 9 +++++++++
 regression/cbmc-java/stack_var5/README | 9 +++++++++
 regression/cbmc-java/stack_var6/README | 9 +++++++++
 regression/cbmc-java/stack_var7/README | 9 +++++++++
 regression/cbmc-java/stack_var8/README | 9 +++++++++
 regression/cbmc-java/stack_var9/README | 9 +++++++++
 9 files changed, 81 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var1/README
 create mode 100644 regression/cbmc-java/stack_var2/README
 create mode 100644 regression/cbmc-java/stack_var3/README
 create mode 100644 regression/cbmc-java/stack_var4/README
 create mode 100644 regression/cbmc-java/stack_var5/README
 create mode 100644 regression/cbmc-java/stack_var6/README
 create mode 100644 regression/cbmc-java/stack_var7/README
 create mode 100644 regression/cbmc-java/stack_var8/README
 create mode 100644 regression/cbmc-java/stack_var9/README

diff --git a/regression/cbmc-java/stack_var1/README b/regression/cbmc-java/stack_var1/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/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.
diff --git a/regression/cbmc-java/stack_var2/README b/regression/cbmc-java/stack_var2/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/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.
diff --git a/regression/cbmc-java/stack_var3/README b/regression/cbmc-java/stack_var3/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/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.
diff --git a/regression/cbmc-java/stack_var4/README b/regression/cbmc-java/stack_var4/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/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.
diff --git a/regression/cbmc-java/stack_var5/README b/regression/cbmc-java/stack_var5/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/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.
diff --git a/regression/cbmc-java/stack_var6/README b/regression/cbmc-java/stack_var6/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/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.
diff --git a/regression/cbmc-java/stack_var7/README b/regression/cbmc-java/stack_var7/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/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.
diff --git a/regression/cbmc-java/stack_var8/README b/regression/cbmc-java/stack_var8/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/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.
diff --git a/regression/cbmc-java/stack_var9/README b/regression/cbmc-java/stack_var9/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/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.

From 0ce085fb9d0d431bd8ba546c212b828e9148609b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Mon, 22 May 2017 17:51:49 +0200
Subject: [PATCH 8/8] Add temporary variables for values on stack for write
 operations

concerned bytecode instructions:
 - iinc
 - pustatic
 - putfield
 - ?store
 - ?astore
---
 .../java_bytecode_convert_method.cpp          | 146 +++++++++++++++++-
 .../java_bytecode_convert_method_class.h      |  13 ++
 2 files changed, 151 insertions(+), 8 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 43a2ded0af1..28baf1b7c27 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1319,15 +1319,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       const dereference_exprt element(data_plus_offset, element_type);
 
-      c=code_blockt();
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+
+      save_stack_entries(
+        "stack_astore",
+        element_type,
+        block,
+        bytecode_write_typet::ARRAY_REF,
+        "");
+
       codet bounds_check=
         get_array_bounds_check(deref, op[1], i_it->source_location);
       bounds_check.add_source_location()=i_it->source_location;
-      c.move_to_operands(bounds_check);
+      block.move_to_operands(bounds_check);
       code_assignt array_put(element, op[2]);
       array_put.add_source_location()=i_it->source_location;
-      c.move_to_operands(array_put);
-      c.add_source_location()=i_it->source_location;
+      block.move_to_operands(array_put);
+      c=block;
     }
     else if(statement==patternt("?store"))
     {
@@ -1336,12 +1345,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       exprt var=
         variable(arg0, statement[0], i_it->address, NO_CAST);
+      const irep_idt &var_name=to_symbol_expr(var).get_identifier();
 
       exprt toassign=op[0];
       if('a'==statement[0] && toassign.type()!=var.type())
         toassign=typecast_exprt(toassign, var.type());
 
-      c=code_assignt(var, toassign);
+      code_blockt block;
+
+      save_stack_entries(
+        "stack_store",
+        toassign.type(),
+        block,
+        bytecode_write_typet::VARIABLE,
+        var_name);
+      code_assignt assign(var, toassign);
+      assign.add_source_location()=i_it->source_location;
+      block.copy_to_operands(assign);
+      c=block;
     }
     else if(statement==patternt("?aload"))
     {
@@ -1587,13 +1608,25 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="iinc")
     {
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+      // search variable on stack
+      const exprt &locvar=variable(arg0, 'i', i_it->address, NO_CAST);
+      save_stack_entries(
+        "stack_iinc",
+        java_int_type(),
+        block,
+        bytecode_write_typet::VARIABLE,
+        to_symbol_expr(locvar).get_identifier());
+
       code_assignt code_assign;
       code_assign.lhs()=
         variable(arg0, 'i', i_it->address, NO_CAST);
       code_assign.rhs()=plus_exprt(
         variable(arg0, 'i', i_it->address, CAST_AS_NEEDED),
         typecast_exprt(arg1, java_int_type()));
-      c=code_assign;
+      block.copy_to_operands(code_assign);
+      c=block;
     }
     else if(statement==patternt("?xor"))
     {
@@ -1828,7 +1861,15 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="putfield")
     {
       assert(op.size()==2 && results.size()==0);
-      c=code_assignt(to_member(op[0], arg0), op[1]);
+      code_blockt block;
+      save_stack_entries(
+        "stack_field",
+        op[1].type(),
+        block,
+        bytecode_write_typet::FIELD,
+        arg0.get(ID_component_name));
+      block.copy_to_operands(code_assignt(to_member(op[0], arg0), op[1]));
+      c=block;
     }
     else if(statement=="putstatic")
     {
@@ -1841,7 +1882,17 @@ codet java_bytecode_convert_methodt::convert_instructions(
         lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
-      c=code_assignt(symbol_expr, op[0]);
+      code_blockt block;
+      block.add_source_location()=i_it->source_location;
+
+      save_stack_entries(
+        "stack_static_field",
+        symbol_expr.type(),
+        block,
+        bytecode_write_typet::STATIC_FIELD,
+        symbol_expr.get_identifier());
+      block.copy_to_operands(code_assignt(symbol_expr, op[0]));
+      c=block;
     }
     else if(statement==patternt("?2?")) // i2c etc.
     {
@@ -1860,6 +1911,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       const exprt tmp=tmp_variable("new", ref_type);
       c=code_assignt(tmp, java_new_expr);
+      c.add_source_location()=i_it->source_location;
       results[0]=tmp;
     }
     else if(statement=="newarray" ||
@@ -2443,3 +2495,81 @@ void java_bytecode_convert_method(
 
   java_bytecode_convert_method(class_symbol, method);
 }
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::save_stack_entries
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: create temporary variables if a write instruction can have undesired
+          side-effects
+
+\*******************************************************************/
+
+void java_bytecode_convert_methodt::save_stack_entries(
+  const std::string &tmp_var_prefix,
+  const typet &tmp_var_type,
+  code_blockt &block,
+  const bytecode_write_typet write_type,
+  const irep_idt &identifier)
+{
+  for(auto &stack_entry : stack)
+  {
+    // remove typecasts if existing
+    while(stack_entry.id()==ID_typecast)
+      stack_entry=to_typecast_expr(stack_entry).op();
+
+    // variables or static fields and symbol -> save symbols with same id
+    if((write_type==bytecode_write_typet::VARIABLE ||
+        write_type==bytecode_write_typet::STATIC_FIELD) &&
+       stack_entry.id()==ID_symbol)
+    {
+      const symbol_exprt &var=to_symbol_expr(stack_entry);
+      if(var.get_identifier()==identifier)
+        create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+    }
+
+    // array reference and dereference -> save all references on the stack
+    else if(write_type==bytecode_write_typet::ARRAY_REF &&
+            stack_entry.id()==ID_dereference)
+      create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+
+    // field and member access -> compare component name
+    else if(write_type==bytecode_write_typet::FIELD &&
+            stack_entry.id()==ID_member)
+    {
+      const irep_idt &entry_id=
+        to_member_expr(stack_entry).get_component_name();
+      if(entry_id==identifier)
+        create_stack_tmp_var(tmp_var_prefix, tmp_var_type, block, stack_entry);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: java_bytecode_convert_methodt::create_stack_tmp_var
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: actually create a temporary variable to hold the value of a stack
+          entry
+
+\*******************************************************************/
+
+void java_bytecode_convert_methodt::create_stack_tmp_var(
+  const std::string &tmp_var_prefix,
+  const typet &tmp_var_type,
+  code_blockt &block,
+  exprt &stack_entry)
+{
+  const exprt tmp_var=
+    tmp_variable(tmp_var_prefix, tmp_var_type);
+  block.copy_to_operands(code_assignt(tmp_var, stack_entry));
+  stack_entry=tmp_var;
+}
diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h
index f83ece86b12..f649d06e5bc 100644
--- a/src/java_bytecode/java_bytecode_convert_method_class.h
+++ b/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -215,6 +215,19 @@ class java_bytecode_convert_methodt:public messaget
     const code_typet &);
 
   const bytecode_infot &get_bytecode_info(const irep_idt &statement);
+
+  enum class bytecode_write_typet { VARIABLE, ARRAY_REF, STATIC_FIELD, FIELD};
+  void save_stack_entries(
+    const std::string &,
+    const typet &,
+    code_blockt &,
+    const bytecode_write_typet,
+    const irep_idt &);
+  void create_stack_tmp_var(
+    const std::string &,
+    const typet &,
+    code_blockt &,
+    exprt &);
 };
 
 #endif