From 1e11f6dc37efa9c3066623848ff9410afc91a4ce Mon Sep 17 00:00:00 2001
From: Antonia Lechner <antonia.lechner@diffblue.com>
Date: Wed, 24 Jan 2018 17:52:44 +0000
Subject: [PATCH] Add test for multiple array types in single method

---
 .../lazyloading_multiple_array_types/A.class   | Bin 0 -> 226 bytes
 .../lazyloading_multiple_array_types/A.java    |   7 +++++++
 .../lazyloading_multiple_array_types/B.class   | Bin 0 -> 226 bytes
 .../lazyloading_multiple_array_types/B.java    |   7 +++++++
 .../Test.class                                 | Bin 0 -> 728 bytes
 .../lazyloading_multiple_array_types/Test.java |  17 +++++++++++++++++
 .../lazyloading_multiple_array_types/test.desc |   8 ++++++++
 7 files changed, 39 insertions(+)
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/A.class
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/A.java
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/B.class
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/B.java
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/Test.class
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/Test.java
 create mode 100644 regression/cbmc-java/lazyloading_multiple_array_types/test.desc

diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.class b/regression/cbmc-java/lazyloading_multiple_array_types/A.class
new file mode 100644
index 0000000000000000000000000000000000000000..a1388a0f223c195eb6c254380d53377982415320
GIT binary patch
literal 226
zcmZ9FF$;oF6ot>#r<PeZ2Mul2kV|6(5(GiiP_(PP;)yAU_N!W&f`)!TKPtMfu{)e|
z@3|kG_viTnFoo~Jgy*2`phK`{Dp%E<U=BwIf>;zsN$}Symz(+$%W@yZ87Fl5AuEEr
zE9x?lOQmBwoTSk;@*rR_6cW1n4zege2irK6NreFnZq#Fd8(^{8eD&Fh-5NhYcU}k%
atNjc0tAQq~MtkfUHN@?Y6P&yHgVq--EFPTz

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/A.java b/regression/cbmc-java/lazyloading_multiple_array_types/A.java
new file mode 100644
index 00000000000..71f8cf87a4f
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/A.java
@@ -0,0 +1,7 @@
+public class A {
+
+    public int f() {
+        return 1;
+    }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.class b/regression/cbmc-java/lazyloading_multiple_array_types/B.class
new file mode 100644
index 0000000000000000000000000000000000000000..3fd3527e72a3bce7725397b76c7d524c8c07044f
GIT binary patch
literal 226
zcmZ9FKMR6T6vfZ=&(qAZIcR9BhFlt>!5|2thN4~VA&M!8_NiK$f`&doA1b=fu{)e|
z@3}uXpYQ7pU;)p84%b4@LZ2X(X_3||f<Bp^3C6m-NP@RZ3%PHuk*rQ(lygE!i);zb
zv23bXZc-JCV4j7y(1ih$p@1+@x1Wba;vb?+#x=&!xKWJ;Zh*-u_!_YjyE%J;9=s4N
aR?&v)WuwEY&>_1*HT(X@8Js)ngYFM4MjoU9

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/B.java b/regression/cbmc-java/lazyloading_multiple_array_types/B.java
new file mode 100644
index 00000000000..0f49c7dba43
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/B.java
@@ -0,0 +1,7 @@
+public class B {
+
+    public int g() {
+        return 5;
+    }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.class b/regression/cbmc-java/lazyloading_multiple_array_types/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..6e6b1b68d70994da2f2009afeec0a3f9f8f2e568
GIT binary patch
literal 728
zcmYL{Pfrt36vcn9Gwrm)AT0=1Y4IOuX^|?{6%_^4grw*KVj^ywPDdQ5t(mqaeiYf5
zxN(h|l4ydvn)soJ_Z3PP@7{OrJMX@8?##cFU&la+dp09v5+um#Fk^F-Yc|)pq2W!7
zSsROt#hlG8Zd>FOF*gj|Ppb;^b!ByVfY<tXP4L95+iLk?J7_jqPlA?Pt@|~F+7V_s
zXawyQg^`<oDg5<j%~y<7f`<RR^S<hb+nTJ1dhdL1Uy;aFw*6LnS(8V%+OD_1>3%rl
z#LHg&ted^n?1Y~GEYNoo`o`j(`_Xk6XTrf@)ZqeS7V{2y3Kk0vcPKa{Nh#8rTCBT`
z-Qwy%_R}zIhN4fmvRHH|a#xWYGGA2pe6KC0WD4qS-_M5ZWCm(i3=N6vb(w`?s^+(X
z(661pAZFSfIgml@$g~sk6~K@sY9*otLo%&33NldIjKqtAvXYhLX#NOwC>zD3#8|&5
z6JUx<ve(qFL@*^+^F8k8e-i1jAj#-4r_u3evKmUB)Yw?+;pl>~^cVB+wA95cpVqoW
zA5Lf9tb8YSKq{MzePQG`)~h4pf3%KBU&oC6F~}-m^FWL}5>p#uYg0_QVk<4DHb#jP
s3Q8&BTt2r}>U)6Hc%qAafMtHeG=2~pwjbEkZK6b+$9fo7`may_2YLW~`v3p{

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/Test.java b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java
new file mode 100644
index 00000000000..959c215df68
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/Test.java
@@ -0,0 +1,17 @@
+public class Test {
+  
+  A[] arrayA;
+  B[] arrayB;
+
+  public static void check(Test t) {
+    if (t == null || t.arrayA == null || t.arrayB == null ||
+        t.arrayA.length == 0 || t.arrayB.length == 0 ||
+        t.arrayA[0] == null || t.arrayB[0] == null)
+      return;
+    int i = t.arrayA[0].f();
+    int j = t.arrayB[0].g();
+    int sum = i + j;
+    assert(sum == 6);
+  }
+
+}
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc
new file mode 100644
index 00000000000..f15d1291c02
--- /dev/null
+++ b/regression/cbmc-java/lazyloading_multiple_array_types/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--lazy-methods --verbosity 10 --function Test.check
+^EXIT=0$
+^SIGNAL=0$
+elaborate java::A\.f:\(\)I
+elaborate java::B\.g:\(\)I
+VERIFICATION SUCCESSFUL