From 7fe27bd8b0c52d2391ee7816273e7ebb111d62a0 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Wed, 7 Dec 2016 15:06:13 +0000
Subject: [PATCH] Add tests for local variable live ranges with holes

Both of these feature local variables that are declared in the class file LVT with two or more live ranges, because of initialisation by a try/catch or the cases of a switch statement. The tests assert that the initialisation is as expected, to catch cases where the two live ranges are erroneously treated seperately and so the variable read in the assertion is an effective nondet.
---
 .../live_range_with_holes.class               | Bin 0 -> 798 bytes
 .../LocalVarTable3/live_range_with_holes.java |  26 ++++++++++++++++++
 regression/cbmc-java/LocalVarTable3/test.desc |   7 +++++
 .../LocalVarTable4/live_range_exception.class | Bin 0 -> 780 bytes
 .../LocalVarTable4/live_range_exception.java  |  18 ++++++++++++
 regression/cbmc-java/LocalVarTable4/test.desc |   7 +++++
 6 files changed, 58 insertions(+)
 create mode 100644 regression/cbmc-java/LocalVarTable3/live_range_with_holes.class
 create mode 100644 regression/cbmc-java/LocalVarTable3/live_range_with_holes.java
 create mode 100644 regression/cbmc-java/LocalVarTable3/test.desc
 create mode 100644 regression/cbmc-java/LocalVarTable4/live_range_exception.class
 create mode 100644 regression/cbmc-java/LocalVarTable4/live_range_exception.java
 create mode 100644 regression/cbmc-java/LocalVarTable4/test.desc

diff --git a/regression/cbmc-java/LocalVarTable3/live_range_with_holes.class b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.class
new file mode 100644
index 0000000000000000000000000000000000000000..af3f7e4358a4ac1e72766f3ca16506c8dcbce045
GIT binary patch
literal 798
zcmZuuO-~b16g_V~I&B%Cv;}HgYxxQvA?=2p#b^*BN!100L^jQ|eW4GBj+vRF{uSJs
zuyCa&l4zoPe~AA=<9Vf&g)H8?_nvw8oOAE|`upt%fGw<~;h>a)jk1HgX_zQEsHAZZ
zRR;?Kxn(bkWEiWUA3au)*Y;&sKpY7q8mh122Lk5W`k{ce6Lh7(bW`=^v%zUwhA;GE
zfowDAc>bXmDqW92EAFXCV7}?AGuaBg{;_PmQE{);3w#;fC*7&1`V4FPnq0i)+2?sj
zIWIgGm^_HR&a0>1>k(nH(eX!q(g(pH?8rT()r+?Z)K0uJ&qW#&E|N$I6f{ux>7)MW
zdfweI3_^j~TNxZIx>&-pK<1|PdHY0mVlLqZ+VQzRfw``XR4BV+a@vmv{J`ZMVS(#+
z_&Y?VpzSa-A+$T*E~`4DV6-<bAwDrNFv&YH1Px3vcds5`8W~n8%pgldH~;2qlX0*3
zkvFi;WAJFg(kNfF8rJp&rtF5z;Ft|_`!kGl<V)|7EZHA0@g3&NOISa(x;a#@(H>~G
zOrsU%RjMt~%L+ZL(!~ZHY$Asm=CF&x(B%`3S>dob<f&gJ(=0QCJ=fUk7^7o$=BcrX
z;;5rWo~w>|;w}>9MB)!jA*LKUDU27kHJlEZ$=Y9$IEQ0hz%swU_<wnt$cEuQ)GNNj
H!a(sKl{bfb

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java
new file mode 100644
index 00000000000..fda6daf9b5a
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable3/live_range_with_holes.java
@@ -0,0 +1,26 @@
+
+public class live_range_with_holes {
+
+  public static void main(int arg) {
+
+    int x;
+    int y;
+    switch(arg) {
+      case 1:
+        x = 1;
+        y = 1;
+        break;
+      case 2:
+        x = 2;
+        y = 2;
+        break;
+      default:
+        x = 0;
+        y = 0;
+        break;
+    }
+    assert(x >= 0 && x <= 2);
+
+  }
+
+}
diff --git a/regression/cbmc-java/LocalVarTable3/test.desc b/regression/cbmc-java/LocalVarTable3/test.desc
new file mode 100644
index 00000000000..a50e15252db
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable3/test.desc
@@ -0,0 +1,7 @@
+CORE
+live_range_with_holes.class
+--function live_range_with_holes.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/regression/cbmc-java/LocalVarTable4/live_range_exception.class b/regression/cbmc-java/LocalVarTable4/live_range_exception.class
new file mode 100644
index 0000000000000000000000000000000000000000..71b1dd48d11031ebdc6475f126df195b1d1aa977
GIT binary patch
literal 780
zcmZuvO>fgc6r7E>apF3So2DTRpKSva4&;(sA_OW0A*FCAs?=U8$63J^*Qso$DnEr@
zIQGJ&AW;b<xbvSt%vvEqB8TUFAM<A3zV*-FU%vxrW5YoK*KOP=B9EIkZaI)9UUjgB
zbsJ5ArKX=GDo*t<N}lM%?}ut2Aod0FT^;H4p@6k<Z&yHW4hKr0+|!YIF*@q2_>}<*
zRC>d}4|n}on|Pd*=^LF0)Ow*lQ3tUfy;cY6G*HJzs6)0RUq{qAr9G#;qmgU5cj%w^
zt&sTE)<5vlPU;75xBcUco);1*bc1j_ptCa^#esUN%{VKw6dxE`7xQp=;~5ezif{z#
z)6(O=TiJ@^VJuLcMQh`>i#xb0;7vPU_77E%a#PdPX2>OT8v~W-SPdrJyj414fg9e(
zD&MHUXA@rCOheCtFeCF@V$|X(c+TCwgt(xS!veqgESW=@zJU?|4~smDs7#ta5^XWp
zv^rMz9EEM!k=;+Q&QNW<hu4rFF#ip5?-FxAE;1GgJL@qTYuR8$#^whqv*I#SVzfZd
z!#b6Wew*4k+7haaBo&wG@vZ3Ba3$++jH@o{<7%B)7uGWyE59Ixs1e_oOy16>0TwIy
dFR;&G%X3KUGpzqtV2C(?`^YTnDuW!Z{Q;aDk0by9

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/LocalVarTable4/live_range_exception.java b/regression/cbmc-java/LocalVarTable4/live_range_exception.java
new file mode 100644
index 00000000000..52e5d54070a
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable4/live_range_exception.java
@@ -0,0 +1,18 @@
+
+public class live_range_exception {
+  public static void main() {
+    int x;
+    int y;
+    try
+    {
+      x = 0;
+      y = 0;
+    }
+    catch(Exception e)
+    {
+      x = 1;
+      y = 1;
+    }
+    assert(x==0 || x==1);
+  }
+}
diff --git a/regression/cbmc-java/LocalVarTable4/test.desc b/regression/cbmc-java/LocalVarTable4/test.desc
new file mode 100644
index 00000000000..bf94c110fcc
--- /dev/null
+++ b/regression/cbmc-java/LocalVarTable4/test.desc
@@ -0,0 +1,7 @@
+CORE
+live_range_exception.class
+--function live_range_exception.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--