From 4d0f98435790f988b1a6e9fe23456f3d329ce32b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 24 Jan 2018 10:47:33 +0000
Subject: [PATCH] Add regression tests for initialization of Java main args

---
 .../main-args-elements-non-null1/Main.class   | Bin 0 -> 529 bytes
 .../main-args-elements-non-null1/Main.java    |   9 ++++++++
 .../main-args-elements-non-null1/test.desc    |   8 +++++++
 .../main-args-elements-non-null2/Main.class   | Bin 0 -> 640 bytes
 .../main-args-elements-non-null2/Main.java    |  17 +++++++++++++++
 .../main-args-elements-non-null2/test.desc    |   8 +++++++
 .../main-args-elements-non-null3/Main.class   | Bin 0 -> 555 bytes
 .../main-args-elements-non-null3/Main.java    |  12 +++++++++++
 .../main-args-elements-non-null3/test.desc    |   8 +++++++
 .../main-args-elements-non-null4/Main.class   | Bin 0 -> 648 bytes
 .../main-args-elements-non-null4/Main.java    |  18 ++++++++++++++++
 .../main-args-elements-non-null4/test.desc    |   8 +++++++
 .../Main.class                                | Bin 0 -> 518 bytes
 .../Main.java                                 |   8 +++++++
 .../test.desc                                 |   8 +++++++
 .../cbmc-java/main-args-non-null1/Main.class  | Bin 0 -> 518 bytes
 .../cbmc-java/main-args-non-null1/Main.java   |   8 +++++++
 .../cbmc-java/main-args-non-null1/test.desc   |   8 +++++++
 .../cbmc-java/main-args-non-null2/Main.class  | Bin 0 -> 573 bytes
 .../cbmc-java/main-args-non-null2/Main.java   |  12 +++++++++++
 .../cbmc-java/main-args-non-null2/test.desc   |   8 +++++++
 .../cbmc-java/main-args-non-null3/Main.class  | Bin 0 -> 518 bytes
 .../cbmc-java/main-args-non-null3/Main.java   |   8 +++++++
 .../cbmc-java/main-args-non-null3/test.desc   |   8 +++++++
 .../Main.class                                | Bin 0 -> 533 bytes
 .../Main.java                                 |   9 ++++++++
 .../test.desc                                 |   8 +++++++
 .../Main.class                                | Bin 0 -> 533 bytes
 .../Main.java                                 |  10 +++++++++
 .../test.desc                                 |   8 +++++++
 .../no-main-args-maybe-null1/Main.class       | Bin 0 -> 518 bytes
 .../no-main-args-maybe-null1/Main.java        |   8 +++++++
 .../no-main-args-maybe-null1/test.desc        |   8 +++++++
 .../no-main-args-maybe-null2/Main.class       | Bin 0 -> 518 bytes
 .../no-main-args-maybe-null2/Main.java        |   8 +++++++
 .../no-main-args-maybe-null2/test.desc        |   8 +++++++
 .../no-main-int-array-maybe-null1/Main.class  | Bin 0 -> 616 bytes
 .../no-main-int-array-maybe-null1/Main.java   |  17 +++++++++++++++
 .../no-main-int-array-maybe-null1/test.desc   |  12 +++++++++++
 .../Main.class                                | Bin 0 -> 545 bytes
 .../no-main-multi-array-maybe-null1/Main.java |  11 ++++++++++
 .../no-main-multi-array-maybe-null1/test.desc |  10 +++++++++
 .../Main.class                                | Bin 0 -> 545 bytes
 .../no-main-multi-array-maybe-null2/Main.java |  11 ++++++++++
 .../no-main-multi-array-maybe-null2/test.desc |  10 +++++++++
 .../Main$A.class                              | Bin 0 -> 245 bytes
 .../Main.class                                | Bin 0 -> 597 bytes
 .../Main.java                                 |  16 ++++++++++++++
 .../test.desc                                 |  10 +++++++++
 .../Main$A.class                              | Bin 0 -> 245 bytes
 .../Main.class                                | Bin 0 -> 677 bytes
 .../Main.java                                 |  20 ++++++++++++++++++
 .../test.desc                                 |  12 +++++++++++
 53 files changed, 352 insertions(+)
 create mode 100644 regression/cbmc-java/main-args-elements-non-null1/Main.class
 create mode 100644 regression/cbmc-java/main-args-elements-non-null1/Main.java
 create mode 100644 regression/cbmc-java/main-args-elements-non-null1/test.desc
 create mode 100644 regression/cbmc-java/main-args-elements-non-null2/Main.class
 create mode 100644 regression/cbmc-java/main-args-elements-non-null2/Main.java
 create mode 100644 regression/cbmc-java/main-args-elements-non-null2/test.desc
 create mode 100644 regression/cbmc-java/main-args-elements-non-null3/Main.class
 create mode 100644 regression/cbmc-java/main-args-elements-non-null3/Main.java
 create mode 100644 regression/cbmc-java/main-args-elements-non-null3/test.desc
 create mode 100644 regression/cbmc-java/main-args-elements-non-null4/Main.class
 create mode 100644 regression/cbmc-java/main-args-elements-non-null4/Main.java
 create mode 100644 regression/cbmc-java/main-args-elements-non-null4/test.desc
 create mode 100644 regression/cbmc-java/main-args-non-null-with-function1/Main.class
 create mode 100644 regression/cbmc-java/main-args-non-null-with-function1/Main.java
 create mode 100644 regression/cbmc-java/main-args-non-null-with-function1/test.desc
 create mode 100644 regression/cbmc-java/main-args-non-null1/Main.class
 create mode 100644 regression/cbmc-java/main-args-non-null1/Main.java
 create mode 100644 regression/cbmc-java/main-args-non-null1/test.desc
 create mode 100644 regression/cbmc-java/main-args-non-null2/Main.class
 create mode 100644 regression/cbmc-java/main-args-non-null2/Main.java
 create mode 100644 regression/cbmc-java/main-args-non-null2/test.desc
 create mode 100644 regression/cbmc-java/main-args-non-null3/Main.class
 create mode 100644 regression/cbmc-java/main-args-non-null3/Main.java
 create mode 100644 regression/cbmc-java/main-args-non-null3/test.desc
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null1/test.desc
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null2/Main.class
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null2/Main.java
 create mode 100644 regression/cbmc-java/no-main-args-elements-maybe-null2/test.desc
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null1/test.desc
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null2/Main.class
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null2/Main.java
 create mode 100644 regression/cbmc-java/no-main-args-maybe-null2/test.desc
 create mode 100644 regression/cbmc-java/no-main-int-array-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-int-array-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-int-array-maybe-null1/test.desc
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null1/test.desc
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null2/Main.class
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null2/Main.java
 create mode 100644 regression/cbmc-java/no-main-multi-array-maybe-null2/test.desc
 create mode 100644 regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main$A.class
 create mode 100644 regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-object-array-elements-maybe-null1/test.desc
 create mode 100644 regression/cbmc-java/no-main-object-array-maybe-null1/Main$A.class
 create mode 100644 regression/cbmc-java/no-main-object-array-maybe-null1/Main.class
 create mode 100644 regression/cbmc-java/no-main-object-array-maybe-null1/Main.java
 create mode 100644 regression/cbmc-java/no-main-object-array-maybe-null1/test.desc

diff --git a/regression/cbmc-java/main-args-elements-non-null1/Main.class b/regression/cbmc-java/main-args-elements-non-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..c1e182d5e1c44aa508db6b5000181f5b10873ff5
GIT binary patch
literal 529
zcmYLFO-lkn7=C7Vb#-08&95>DI+%xq@Rmejb<#Q*L3UbokTG3jckRb`=-Ro0gaSJT
z{ix`j#SaE%-g)Qwdgu4=a{-`+T?0BYVFa+HBWplKMn}#-9t9mmhV;JWy4>-^#CFex
zYjsDw&%ini!Md=8cfz2S4{jN>#-z^~;!R=mtLeDQof`?Jhp{DWhHUx1IkcXv>d3MO
z)wbsddvGj?(Y9yx9$MDp5+ADfMoVR*J()T^ekr6*xJ5dLQo@9Rh=~xw4Ec@b*(&IT
z<4hbfmINK!CU#I_NNkYT-68LJ6n4{UjA%|u+2^iscz>-$;k+q5(2yPM(KqSzZ7h+O
z?o_E@G7Rk|-AZ&aIs=tC*sBC0N_)_6(gcVhPPK$Kp!nTlW$}#M8<ZK674_%`kuRus
zb7<d^ulW2J*^nr$APN*9K{qlkP=@5%yXMOQ$yDG2!5MVz1)BN}WuvpoA^8C)=BZ4Z
H@@>-p`72;x

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-elements-non-null1/Main.java b/regression/cbmc-java/main-args-elements-non-null1/Main.java
new file mode 100644
index 000000000000..b1e76e43bc34
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null1/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>0)
+      assert(args[0] != null); // must hold
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-elements-non-null1/test.desc b/regression/cbmc-java/main-args-elements-non-null1/test.desc
new file mode 100644
index 000000000000..769fe43162b4
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-elements-non-null2/Main.class b/regression/cbmc-java/main-args-elements-non-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..72aa67be3de44dc5286304ed30ef0627c2349eea
GIT binary patch
literal 640
zcmY+BNlU{}6ot=glD;O!w$`c6*4YXQ;?4nQ5UMUJg1So6M|~PoNmB8*xNz%Q1qB7&
z`=iAB;!xbY>E83@oSTo&mp1?ln6zM`+d>{a9K9wu`Z)S680h90urP=rj$wxOF((W~
z5Xrh9ZpzT9c%sU{jv10m(wET+gElpN$e?f3tAZg@lD^n$TvSAGpqi<0;YgpMYwDzQ
z=3F^*p5xc%%26Qw+M*J+mLtbK-*qnIelo+5T5`P~xK*w<0#|HHg)(;uHLEB#Y_xI|
zY>Z%(TsFyD*RHr!c5PT_VaPX2Yrjdhf}kFdGlk<AvoVedhHSHQzj7wr=-<<~V~Xtw
zzZRXwv3DqMQ?%jHs3>SvgfbA-zpqigs6hpq(=iG(X_Ni{%jT6oI%!}k46SLp4baYL
zH;T_-_o@*YT9ff3O#oT6(OI?DkRUNoD8AjoE^70onI|Nc?~p4!K)*rDD~zLOB;W62
zahil0Nfd67Tqvl46d_H*sj7_}`52~-992`$((4@UX*zZM`CEutKwFMKA$0?;-$B<N
Wp)0T7@L#VAVjy9!szjY}x$6stGIetR

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-elements-non-null2/Main.java b/regression/cbmc-java/main-args-elements-non-null2/Main.java
new file mode 100644
index 000000000000..b8c8dd3ac565
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null2/Main.java
@@ -0,0 +1,17 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      if(args.length>0)
+      {
+        String s = args[0];
+        int i = s.length(); // must not fail
+      }
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-elements-non-null2/test.desc b/regression/cbmc-java/main-args-elements-non-null2/test.desc
new file mode 100644
index 000000000000..46f29cff4c3d
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-elements-non-null3/Main.class b/regression/cbmc-java/main-args-elements-non-null3/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..4734b3ec778d31c3f89839276946947490d5ffad
GIT binary patch
literal 555
zcmYk3OG^VW6opUb(XrF1_GPX00fGyyU_rXGh*EXsV^I-QTuj?gqT^IDQ-4g?f@>8l
zDAc9kj}mW&+HsTIoZS1}bCd6%_Yr^^mTg!lBw=FKLeYkff`vI7CCpnWGvrs@AmB0-
zJwMnNf!p$Uhk;!(B<jK!;SPhowtmiFG<qG*Fmoh)e$u~dae1ba>Eg~6K0|Ts>gdLO
zaI2o{cdN}%3ctIp3e(NdZQmZd_v8GjdfOY5?Pjkp+x$={PV$&In+oB;M#{kyk_@Go
zx%X%EK+2w^#;U-=f`dgYF=XP*)7A}dhh#RE8XnC_E;~FBl6NL7G8gvgf`+`r3O$oW
z&&Dz()tw?8Oqrq8q0<uWjCQj!1bbGANYk2#M4AB8n4wsuUPFu2YGq_RV&etc0NIMZ
z^@Y?2^ot>k&#`9w*A!HXpg9;6n*^tSA~&1lBSVS-t(>QGcH*iQH3G6Z^9_jsEaM4=
V{t7LI{W(+s6PmND=Ez08^1u3uW+ngt

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-elements-non-null3/Main.java b/regression/cbmc-java/main-args-elements-non-null3/Main.java
new file mode 100644
index 000000000000..748a1c4625a3
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null3/Main.java
@@ -0,0 +1,12 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    if(args.length>1)
+    {
+      assert(args[0] != null); // must hold
+      assert(args[1] != null); // must hold
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-elements-non-null3/test.desc b/regression/cbmc-java/main-args-elements-non-null3/test.desc
new file mode 100644
index 000000000000..769fe43162b4
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null3/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-elements-non-null4/Main.class b/regression/cbmc-java/main-args-elements-non-null4/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..e59a3d3c45196fca58cf891670444725e3b211d3
GIT binary patch
literal 648
zcmY*WO;6iE6r7FitZfVgLqggD1scABRHTYqY1Nj3gcRVA3JEwl&MI9nHnJVm-@>6+
z&VUr8BEhYP{-~;NmqNs4_jzaDyqV`ee}CNpSjB=12jecPc){_~0mmzj2^SW|IVN39
z;WfuJ!)PtYGLhyoiL<XV3tEwAGq3}O;+l+Q{*l30T-swW*ORtj7;eZ|>~v3BBK@Yw
z1e^piW~eM4HjaX`U?mFT&Pp>+W!!nM8V8$s5FT#_r<zY@80@t$`Y-M_lWrP{O{t`u
zZIXJcR6KYX<e2d=i#O!5ue|Xi6sO9r2Nwej)jst3G08@nCMh{navU`ebC_o+^_jb^
zBN67$o*o=i>`26&{JW05MS1&8>k+Mrg0@8_Q_+5!M)~qC0ko$B%+RJC`U9*~RsN_l
zz*HDIhv;jPZbr9NzX7{cL=4ke)Q_|QlrTcIq9!O%GcZ@b`-xKBc-L6|4STtV!iNj^
zjVqYv7`TPCe}m%vr55l}rj~-1oQ180E$zrA2M&Bf%2ZWoK#fNE#IRxbUpPjGs2Y3n
lxvKSm5uf*9pM#qhFpX=N%Jaj3N6$*cLc#l_l9e@F`3J5mcC`Qi

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-elements-non-null4/Main.java b/regression/cbmc-java/main-args-elements-non-null4/Main.java
new file mode 100644
index 000000000000..7277b0926032
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null4/Main.java
@@ -0,0 +1,18 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      if(args.length>0) {
+        String s = args[0];
+        if(s != null) {
+          int i = s.length(); // definitely must not fail
+        }
+      }
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-elements-non-null4/test.desc b/regression/cbmc-java/main-args-elements-non-null4/test.desc
new file mode 100644
index 000000000000..46f29cff4c3d
--- /dev/null
+++ b/regression/cbmc-java/main-args-elements-non-null4/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-non-null-with-function1/Main.class b/regression/cbmc-java/main-args-non-null-with-function1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..53745bf42482301741efeda8329cb6baa6334180
GIT binary patch
literal 518
zcmYLF%TB^T6g|@x3Z=+X#0MrOE|7(6SeQtR26Y9xz?g`uQYK`uw5Bb73_svnO(fAo
zmnMFc@lL~IGxyG&^Sbl<_wfawfn5VSib=$<uA^i?MN!9wfigCAY%vt}tsvljC_Fbf
z7lGAx_<(`+7~)OgitvO%tsdMmXf1ER88U6*@~g?X&;1(-riZa5T!vEhzCE&@th!^l
z!+JOLg*!Z!#B?{b?1zr^IL9ZNwlh~Yy57XM`K6FL$qwlpN(mDNQYI2eGL%=EXN#a0
zzVG>DED1WcP3)k;kX<3K`y+0L6m~UgIkYFG9PmK+e6ZA_aN&d=XvrS-=$mx<HkK_*
zcj{Cy8HP@iZWXGGYOFQ`dyzn->5NB1+5l_FP%oiJP@-w!70MKu+7D8nQ152Yz9mtK
zhz3<sL!KnE)R9}BjB`uFMx+7c^09Zsr_i-$XzCl3mBzwc@?%iUQyDQISrq;OKayTs

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-non-null-with-function1/Main.java b/regression/cbmc-java/main-args-non-null-with-function1/Main.java
new file mode 100644
index 000000000000..434ae598e188
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null-with-function1/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-non-null-with-function1/test.desc b/regression/cbmc-java/main-args-non-null-with-function1/test.desc
new file mode 100644
index 000000000000..9e275150f528
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null-with-function1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-non-null1/Main.class b/regression/cbmc-java/main-args-non-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..53745bf42482301741efeda8329cb6baa6334180
GIT binary patch
literal 518
zcmYLF%TB^T6g|@x3Z=+X#0MrOE|7(6SeQtR26Y9xz?g`uQYK`uw5Bb73_svnO(fAo
zmnMFc@lL~IGxyG&^Sbl<_wfawfn5VSib=$<uA^i?MN!9wfigCAY%vt}tsvljC_Fbf
z7lGAx_<(`+7~)OgitvO%tsdMmXf1ER88U6*@~g?X&;1(-riZa5T!vEhzCE&@th!^l
z!+JOLg*!Z!#B?{b?1zr^IL9ZNwlh~Yy57XM`K6FL$qwlpN(mDNQYI2eGL%=EXN#a0
zzVG>DED1WcP3)k;kX<3K`y+0L6m~UgIkYFG9PmK+e6ZA_aN&d=XvrS-=$mx<HkK_*
zcj{Cy8HP@iZWXGGYOFQ`dyzn->5NB1+5l_FP%oiJP@-w!70MKu+7D8nQ152Yz9mtK
zhz3<sL!KnE)R9}BjB`uFMx+7c^09Zsr_i-$XzCl3mBzwc@?%iUQyDQISrq;OKayTs

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-non-null1/Main.java b/regression/cbmc-java/main-args-non-null1/Main.java
new file mode 100644
index 000000000000..434ae598e188
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null1/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args != null); // must hold
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-non-null1/test.desc b/regression/cbmc-java/main-args-non-null1/test.desc
new file mode 100644
index 000000000000..3866f268f76d
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-non-null2/Main.class b/regression/cbmc-java/main-args-non-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..ac0fbb4b98d0c887aaf2da803f14108495c034e8
GIT binary patch
literal 573
zcmYL_O;5r=5Qg8Sg@sZTP!PX0@qixm;!R>SC@0VZ#zZ`ovN5YrNL!4*#XrDVO(f9-
z@BS#`OjXDx`!Vy*Gw<xz_xl*Y0k$k8QIJ?nA%UXAk_D6B%NAC!DzPRozwHEp@<ZM8
zf>Rwht&VC7h^9cItUVnb2^giFD*?08Yb$}dn)cNBpxaXZC5tK1b+ji?DBaZVoCjyW
z<9N6GjnLQL?I9P=G(yL{uRHxnPi6#?Ww-MOw;H{H@2aY1RH{y>J*L=5!zOoA;@P9C
z`fSri3YI`|nmYNP;LP`XJ~?8H#JY_QYzkzi%8S;WazmP88me^Y1IT_`1=?5b35#5Z
z14_{JO>EKsCFx5=rpVptW<an-+GpssMyH@NzB__=W+7&2PeehQ3v<ZOouv)LXaR-Y
zae0Vb?FGgY(jPFdM~HtuM->KDvWgi6#3PbHZP|n*TAo^GDJl`GO5|oKJU{Vr5FvnU
gF7XEW1ZfUo8m}<e*Dv$m7c=6B*~jdDAxh_e0BkU5IRF3v

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-non-null2/Main.java b/regression/cbmc-java/main-args-non-null2/Main.java
new file mode 100644
index 000000000000..17c3566ef2e1
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null2/Main.java
@@ -0,0 +1,12 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    try {
+      int i = args.length; // args must be non-null
+    }
+    catch(Exception e) {
+      assert false; // unreachable
+    }
+  }
+}
diff --git a/regression/cbmc-java/main-args-non-null2/test.desc b/regression/cbmc-java/main-args-non-null2/test.desc
new file mode 100644
index 000000000000..46f29cff4c3d
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--java-throw-runtime-exceptions --refine-strings
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/main-args-non-null3/Main.class b/regression/cbmc-java/main-args-non-null3/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..a28dbf8c77bc33fdfac00a34a70e6e67c87060bc
GIT binary patch
literal 518
zcmYLF%TB^T6g|@x3Z=+X#0MrOE|7(6SeQtR26Y9xz?g`uQYK`uw5Bb73_svnO(fAo
zcP{)W<DG`bX6~Ik=XK}z@8b(V1G@%v6qATyT}R1)ilUAU17&RL*kUN`TS376P<U=|
zE&{9X@BstsF~pm~72yekT0OXB&|2PrGi2Jr<yVt&pZhlwOb=sAxD2K0eS2g*S#`&9
zhxKmg3wL-diRo@=*$*A-agI+kZD+1*biIjh^GhLhk{!}HloBQkq)a4`WGJsR&lW*1
zeBblQSQ2z>o7h2xA-h6e_eb0gDeP+0a%fLVIpBft`CzF<;lc?$(2_mu(KqSzZ7f@s
z?$oJZG7Oz2-6~WW)mUu?_9B5u(;1J3v;o$Tp<Y6dphVNcE0ifRwI8HDq2A4)eM_Pe
z5e=%OhCE4RsUx>M8RwRUjYtE?<zw%NPoZni(9}05D~*M@<j0_xr!rzbvMBrmKOJ6L

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/main-args-non-null3/Main.java b/regression/cbmc-java/main-args-non-null3/Main.java
new file mode 100644
index 000000000000..adf78b53a7da
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null3/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  public static void main(String[] args)
+  {
+    assert(args == null); // must fail
+  }
+}
+
diff --git a/regression/cbmc-java/main-args-non-null3/test.desc b/regression/cbmc-java/main-args-non-null3/test.desc
new file mode 100644
index 000000000000..4c27d3b1965e
--- /dev/null
+++ b/regression/cbmc-java/main-args-non-null3/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null1/Main.class b/regression/cbmc-java/no-main-args-elements-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..6e052a7f6f2d868e4b6498e917abe0ca0f49f0fd
GIT binary patch
literal 533
zcmYL_%}WA77{;I3Rae*b+tf;hpo4ix2yaOg_HofV7(sSgb&xS#V|VS3@zAw%1qlUq
zE9j4k-dX&(%*^}F^ZuS^=J)So4xoyn4h`uL{MgWt(V-%(A*&;YO$}QNsa?}?xb2Fu
z<(vw~><oF2fwdU|HDL+&h(Rsw-7xs-;~r;-HH5`4C!-FxuceqSMy9YBGNrr5z<e|-
zL(}S4TCOdu{-GR<v|O`$-!vZ<`e3a)T#)tFcw%??xsaStlQ{blVL(UNKoB8@+?si^
z40>kUW1EcSfQD@Yc@!ApYvomEz`HJmUAO8(dMBmqaYxv^w_;H^cS0BR$ToK9n>6}1
z7SBm{I;mhX46O!L1=<<y{_+g$MG6t2HQ+TFjYJWnvy@&y@w&zGH}d8A6SA*Rrbv|4
zgCB%Hq2A8m`;rXBV?@b{z+@UA8x3))$h<(%#LB<wA%R5F|Bk>En(rAt^$p6Jv&<sr
O{ZNc!nK<d$r2YZm&tZQ6

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null1/Main.java b/regression/cbmc-java/no-main-args-elements-maybe-null1/Main.java
new file mode 100644
index 000000000000..e991e54adc66
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-elements-maybe-null1/Main.java
@@ -0,0 +1,9 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0)
+      assert(args[0] != null); // allowed to fail
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null1/test.desc b/regression/cbmc-java/no-main-args-elements-maybe-null1/test.desc
new file mode 100644
index 000000000000..0f3969cd7b76
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-elements-maybe-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null2/Main.class b/regression/cbmc-java/no-main-args-elements-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..cb9a212971610d85354651a6662fdbed7a3d2976
GIT binary patch
literal 533
zcmYL_J5K^Z6ot?10t?IXMnDA;6APq}#L!8M1|JP*fiV%Q1tw$=7PGtfV<>E`)kG3a
zu%qxt8SiX(G&6VZ-1D6?^ZWNT2T(;(hlX?rer##T=unZ?kkygHwuT*s)V}FB+;+v-
za?XWgc80viz}gIfny`d>!l0H8?ihUaagQ^^8p7h&lTnA;w{n;+My9YBGNp&cz<f3<
zL(}S4TCOdu{;?EBTCUlBY?@EY`CzR(T$1(Hcw%??rI4IZlQ@SGVL(UNKoB8@+=h9!
z3VLDNW1EbnK*O$qJPHi)&E!pIz`HJm-L&dMdMBmqaYxv^w`Nf|cS0BR$Ts%qn>6}1
z7SBm{s#Gu;hE{`41=<<y{_+g$O%5VLYrtzVl0*@sT8>^p@w&zG0{Qa%1=+HCv_Rq=
z$`s*msP{AYek4Qj7*Vn!FzEwi6GWU&WG>6Z+P~@{fke{(iNF+^?-f4v1ImW8$|CiC
MD8{Kwob+r`|KZ+Yg#Z8m

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null2/Main.java b/regression/cbmc-java/no-main-args-elements-maybe-null2/Main.java
new file mode 100644
index 000000000000..63ccbef75ae4
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-elements-maybe-null2/Main.java
@@ -0,0 +1,10 @@
+public class Main
+{
+  static void main(String[] args) // not public!
+  {
+    if(args != null && args.length>0 && args[0] != null) {
+      assert(false); // allowed to fail
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-args-elements-maybe-null2/test.desc b/regression/cbmc-java/no-main-args-elements-maybe-null2/test.desc
new file mode 100644
index 000000000000..0f3969cd7b76
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-elements-maybe-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-args-maybe-null1/Main.class b/regression/cbmc-java/no-main-args-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..3131f084ffc2b72d0c513b26eca7ba4a230e73ef
GIT binary patch
literal 518
zcmYLFTT22#6#ix}uC8ldGrJfBJy=1$_z)yfSUqVy7(w>5x`T}AZtSl882>=e6(khY
zW6+O^&MaOSI5Tt3cbobB`}hJ-!?p<ng#>i08Yr4jQ82J(qJ(t=8w~kfI|#TR3eOGB
zMPPS_++koHhFD#=B0OPGD|@#LTElZVL%Jzkel;F-xql<UG#J^!Whhqen*;mFt`2Rt
zUu}oJaQnxSm}-Z1@1bQs&hYViZ#Yvn+uqpk@k=3f5-rj>loA$9BrU{|U??p$&*nid
zeBblQSP~3uTG&FFA+tnYcL%%|QrKmyF{F1=N{0u+=gvZl!i8fR&?7t8p>Hzi+gPR~
z-RY!)$uLwcx|L~XwCnp*uonqLifSxs%FznaR3-EX3N0Z23T1-y!4Hz3Q17PDz9mtK
yh-L)Qkt2x=b;&J9#@U5oEm8)uIsF~62@LHSn)(K1sWCT~d>x8)Ds$u_i~K)40bW%A

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-args-maybe-null1/Main.java b/regression/cbmc-java/no-main-args-maybe-null1/Main.java
new file mode 100644
index 000000000000..5bde75a6e9ff
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-maybe-null1/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args != null); // allowed to fail
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-args-maybe-null1/test.desc b/regression/cbmc-java/no-main-args-maybe-null1/test.desc
new file mode 100644
index 000000000000..c23c81e2d8dd
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-maybe-null1/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-args-maybe-null2/Main.class b/regression/cbmc-java/no-main-args-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..203057c9f9267f630bae323493072ef39a475aa7
GIT binary patch
literal 518
zcmYLFTT22#6#ix}uC8ldGrJfBJy=1$_z)yfSUqVy7(w>5x`T}AZtSl882>=e6(khY
zTMzxH=*;4UfipAbe7Bk3zmG2fHEf$OP)I<>s)3>j6$JxpCQ4X0u)&buwS$2Bq43<`
zTm*J^$Q=gOVTjd*E5Z{7wX%21pfx;)Go+is<yYfTm-{yoOoNdvT!v!hzB#a;?CQ{V
z`_*>n3%7qPiK%vI_a0jI;|w3K_l7fNv+a%j9={Y)C($CELn&dwMAAYW35L>A^K2gU
z!uLI&j3vRqriCq(88S=cb$7sfA%$JG8bf*~rF3{8eC{l?C|o$E0X?#V9r`ANzKvx{
z(w$B!m<&VJqFb4EM!UX01$&V|q^QQCrW~yxO;tjVpwI&HuTUmPAN(Ns3H5FY?OPI+
zh-gL-9XXQ7P?y|tWSm_X)*@vfo73MBo50YXp{Z|BmKt+&$=9J+r!q$_vdI4fJB(gb

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-args-maybe-null2/Main.java b/regression/cbmc-java/no-main-args-maybe-null2/Main.java
new file mode 100644
index 000000000000..78237884371f
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-maybe-null2/Main.java
@@ -0,0 +1,8 @@
+public class Main
+{
+  public void main(String[] args) // not static!
+  {
+    assert(args == null); // allowed to fail
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-args-maybe-null2/test.desc b/regression/cbmc-java/no-main-args-maybe-null2/test.desc
new file mode 100644
index 000000000000..c23c81e2d8dd
--- /dev/null
+++ b/regression/cbmc-java/no-main-args-maybe-null2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-int-array-maybe-null1/Main.class b/regression/cbmc-java/no-main-int-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..69f688d31f13d4c54c919869c4bfc5d378b4e99a
GIT binary patch
literal 616
zcmYLGOG_J37(F*L$<0hACK+uS-=?_GK$U{-f+*2~;A5c_s;kN5QbyxMW+ugd;oe2J
zu2rbeg6<Uhqr`KknlNx5-#OoR&bjmN<<A3v71V9yQMHi6M~RvZ167G}i3uB%n39+l
z7@haxSVc+D3**fo_S#+55fDcLxn>Xs$(n$%u=q{DZ1p-yptKW&YOjCRR?(p*6FBpN
zP$0W-ysde~gT(VscfIozrkp^&>382|*$2IT<g2fN?zDE<xpd<F^c)o6IIv&~)O2CF
z>xDm-H{PvnMNu!J*&(!b;j44)ng;Y3i5Um8m=h=uN&D>+<tH>fEVa7KD^TsIIEYkd
zpg`A2p8&%iq0Se}^94n@rakdwKxm6xi@Z&97u>Urdx#rN#0b}1T4XMiQ07@vFOlH~
zY~CVsg;L`Qg}*Sq-@|--t2_@YL}wZgzcAh~mYUaacT&or;f6Cm;|qUmmNT{Dr_^Q^
zF16<&iCV;qWE8MUyDd7YkY~YkEBg}e2pdKRIaX4`K*i1dhP;9_uVET@$mmS}72Y%H
ODO7dVb@H(k{_qO<fp9Yb

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-int-array-maybe-null1/Main.java b/regression/cbmc-java/no-main-int-array-maybe-null1/Main.java
new file mode 100644
index 000000000000..e3ec1bbbdc81
--- /dev/null
+++ b/regression/cbmc-java/no-main-int-array-maybe-null1/Main.java
@@ -0,0 +1,17 @@
+public class Main
+{
+  public static void main(int[] args)
+  {
+    assert(args == null); // allowed to fail
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      try {
+        int i = args[0];
+      }
+      catch(Exception e) {
+        assert false; // must hold
+      }
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-int-array-maybe-null1/test.desc b/regression/cbmc-java/no-main-int-array-maybe-null1/test.desc
new file mode 100644
index 000000000000..23377c953361
--- /dev/null
+++ b/regression/cbmc-java/no-main-int-array-maybe-null1/test.desc
@@ -0,0 +1,12 @@
+CORE
+Main.class
+--function Main.main --java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 6: FAILURE
+assertion at file Main.java line 6 function .* bytecode-index 14: FAILURE
+assertion at file Main.java line 12 function .* bytecode-index 31: SUCCESS
+\*\* 2 of .* failed
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null1/Main.class b/regression/cbmc-java/no-main-multi-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..5a56689bdfbf9419ea00e5906f8cd082f16166c4
GIT binary patch
literal 545
zcmYL_+e!ja6o&sjqmGVap32NJ3JOdtA-qeX=y0V489{k9>PEKN7&Bw<k}uG81qlUq
zXV61MYY!f7)@iTxt$*#`zt0hX64rHSSPa3BB@HPZDi$>?>quioLxv%_WjYSGUD30g
zQ{kA6E^jfgJBC16Si(JIP;)ys48D_Ii!($k!r~YGhX%K=WivfIn8IRM&eiLcj`?I3
zyQbAH)?8ay?E^U(skvtJzG^;B27={gcY@Yyy}sS#=R$%)RRZlvgaI9413`os(sSnV
zROy**_iWlM2Q;i2SVNW}Ht)P_ba>Mxwe!+Rmkwn}wYVc}-kPyUoZF`dy7CU2^iLZ7
z8;hmoc8XLmDTb^;S(ZE_@6QjxUS%U9WCLE2F2Dk!6wB5tC|-5<4axvJ`7yThqi1a7
z)%`ItWGP9KQ}=%m{(^ctgzsA-6%VPCr#&dp_83K^qd=14GbtsH4#X4w4+I9#d@t~+
V?@;E9sVq6~hhiK_@d<B5@*fNoWn};W

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null1/Main.java b/regression/cbmc-java/no-main-multi-array-maybe-null1/Main.java
new file mode 100644
index 000000000000..60fd07be94cd
--- /dev/null
+++ b/regression/cbmc-java/no-main-multi-array-maybe-null1/Main.java
@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+    assert(args == null ||
+	    args.length == 0 ||
+	    args[0] == null ||
+	    args[0].length == 0 ||
+	    args[0][0] != null); // allowed to fail
+  }
+}
diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null1/test.desc b/regression/cbmc-java/no-main-multi-array-maybe-null1/test.desc
new file mode 100644
index 000000000000..b2eed82b65ac
--- /dev/null
+++ b/regression/cbmc-java/no-main-multi-array-maybe-null1/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main --refine-strings --java-max-input-array-length 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null2/Main.class b/regression/cbmc-java/no-main-multi-array-maybe-null2/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..ee7b474bda8ffcf30587c5594d0d04c3ff893436
GIT binary patch
literal 545
zcmYL_%Syvg5QhJgq>W8et+v*BsVFGa;02^RMU<+mR>6v(U8TuEPK}8qsqdmM;93O*
zg}QU$Ly2=jZ8vi}GvEAkettjt0BTq?pre>U3e!4D22>Pv%or$RR>vGeVa1Lj9>yZ@
zqeBtd9gn*V?1~}1D|`{}F{stG3kIzoxSV04A$)$)yY2AsTsG6gtu1_pnQFV;=-T)8
zmS_9dTdg=0{`HQW%(Y_MxoO&WgMqPK#~YxHR?rI_ek>#?(<IQQM3^v;H8F+^LwUqJ
z_*Z%qhCxW1<$#WP6AP#?<VT&Soi2A`QadWuJvx-3<nl;_+#Rw=T->7vy7CIk^iMkd
z8_SpFc8XLmDTb^`S%o|!pR(S;o@FC)WYbBJF2Fb@D3+~fP?GA#3zSE!S>IT-`VUyL
z)a`G~k)@<SPNvyUsF&~1z9dpfkOq0$gLT@Tr-*c{lcdR^lv+XuCZ|$wNIyc?o}j6(
UP)3Y@S#mxF#oU+Tr;-(gKMS8_WB>pF

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null2/Main.java b/regression/cbmc-java/no-main-multi-array-maybe-null2/Main.java
new file mode 100644
index 000000000000..0c908b7b07b6
--- /dev/null
+++ b/regression/cbmc-java/no-main-multi-array-maybe-null2/Main.java
@@ -0,0 +1,11 @@
+public class Main
+{
+  public static void main(String[][] args)
+  {
+    assert(args == null ||
+	    args.length == 0 ||
+	    args[0] == null ||
+	    args[0].length == 0 ||
+	    args[0][0] == null); // allowed to fail
+  }
+}
diff --git a/regression/cbmc-java/no-main-multi-array-maybe-null2/test.desc b/regression/cbmc-java/no-main-multi-array-maybe-null2/test.desc
new file mode 100644
index 000000000000..b2eed82b65ac
--- /dev/null
+++ b/regression/cbmc-java/no-main-multi-array-maybe-null2/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main --refine-strings --java-max-input-array-length 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 5 function .* bytecode-index 24: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main$A.class b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main$A.class
new file mode 100644
index 0000000000000000000000000000000000000000..47ea25c867b491c8fdbc8422614627439a472646
GIT binary patch
literal 245
zcmW-by=nqM6ot>-)g5<T<6oU3kU}lAu?ztb0z#sNl77|<VPqX)SH;&#6-eO&_)wBF
zTb#LbzI*SPx!wP+0H)|C2$3p0D0BsKp%#MZ#X5U@6@-J~r=T`Jd>KLe-8!>8?K4ws
zbe5AO>%*zonm6lB{GqKI@AO%xh@cdD4D#%G##Aa@IA@A^uFKMtf{q`Z<l22tR@u&M
zk9^3F;|T#j1qf9`y}B_9iljmJ$m)Cb(J$nuYR5dI3Wi)x=mIp+VNFN_w9rQU53`6T
Ab^rhX

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.class b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..8b4ac4575400335d84b3b521d308c840334a3938
GIT binary patch
literal 597
zcmYLH%TC)+5Iti%apIUJgjdoQ!Xpa^5=e+0sA|MRs+6<~s!9#3o8$_a2B)$eK86Kb
z)=;TPRH8c;{iup_%_EyT<1;hooEiDw|GRqt+o*eRQOzTRw=Uj!uu*mK-orc=T-01F
z3ZyCUKZT)=_691BbxcSJa;>%s!g_N@FjY5rlmx>t-Vb8c9q2xrI)dzO5C+KyfxWu+
zP2lVe`&v+J1)=^tI_v7_t7&H8j9db5^*CkSG0hW4iR%4mtDnz3x!vC2naw*Ij-sAE
z49sla_}DmA=gLPBB_9)bBd8c)bD+YL&E|`_gD4tC6f*-ZmV7K@MNk@de(9d-UP9YX
ztI_GWmM$-t?dv#*bpMr<E|U>&!VNoE;vrog)`Fk_A1GCf9U?Xny5l>^uX#pc%rtHx
z*GvRuzS$JyN|?elbJN-;nZ>x+c)&vA{u0%Oz16ybb%Emg0}6j&f4_zE*RWVAOBoJx
zk1Pd>`>4^t3=vwWA&1#l7u%^EFj>z0M)m@(a|Or#1#8Up;>gTrVEG?~B6F!!g%U=F
KzXD5n<R1a?3}~MK

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.java b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.java
new file mode 100644
index 000000000000..f3c217aefd36
--- /dev/null
+++ b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/Main.java
@@ -0,0 +1,16 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+  
+  public static void main(Main[] args)
+  {
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      assert(m == null); // allowed to fail
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-object-array-elements-maybe-null1/test.desc b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/test.desc
new file mode 100644
index 000000000000..49668103f1f4
--- /dev/null
+++ b/regression/cbmc-java/no-main-object-array-elements-maybe-null1/test.desc
@@ -0,0 +1,10 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 12 function .* bytecode-index 15: FAILURE
+\*\* 1 of .* failed
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/no-main-object-array-maybe-null1/Main$A.class b/regression/cbmc-java/no-main-object-array-maybe-null1/Main$A.class
new file mode 100644
index 0000000000000000000000000000000000000000..47ea25c867b491c8fdbc8422614627439a472646
GIT binary patch
literal 245
zcmW-by=nqM6ot>-)g5<T<6oU3kU}lAu?ztb0z#sNl77|<VPqX)SH;&#6-eO&_)wBF
zTb#LbzI*SPx!wP+0H)|C2$3p0D0BsKp%#MZ#X5U@6@-J~r=T`Jd>KLe-8!>8?K4ws
zbe5AO>%*zonm6lB{GqKI@AO%xh@cdD4D#%G##Aa@IA@A^uFKMtf{q`Z<l22tR@u&M
zk9^3F;|T#j1qf9`y}B_9iljmJ$m)Cb(J$nuYR5dI3Wi)x=mIp+VNFN_w9rQU53`6T
Ab^rhX

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-object-array-maybe-null1/Main.class b/regression/cbmc-java/no-main-object-array-maybe-null1/Main.class
new file mode 100644
index 0000000000000000000000000000000000000000..711dd19197b844bba630c75f6f4e07c9a717a1ff
GIT binary patch
literal 677
zcmYk2O-~b17=_QBY3H`X)Rux+ML?h^3{et;i2-74P!p3D78ny@b=%&U!7?Q?Q-6nR
z7H(bp5lJ+GT}}K+h7ivkgmH5}&OP@%&-?y9|8W9f757{eFj<6y+Y(bQ?2F5^#EgqO
zn3b55m=_QY0q<oP>S(j4;#kL&lt7``QbAa6tP70QjUFXIKa8IRv1<2pm!@3-XCnxM
z<cWa2xb#{ex7qJ%fpRkl_155^t)o}Q%!dQk5^xvy(yHsmT-r%g=Uq!3rXEr;bEDJy
zSJ2(*52B8K5t#2qgYsZsy;mM881--sWr3OzR(dLYyVAJidmcso$b*LxL(MOVx`zea
z6{uwP?e@OzB*edHk;K_sIs}1<u8xC9cdsgwHW_d>>~t5ioN9qnw!qn;1XOB<iHc2y
zh+M0@O>r08^Zqf!XC63Au1+elFO1_l&&K+J#VqbyUtk@f?Ek{ZPuOpckvsK=So2Rl
z;*oDZY%ULRKebeszac-&T$%XaSCeU_nbVLwyUZHFB%x=BJx}Pz#BNcY;Hw9_dWHpw
z8-GYvK<%oL)sz?*tvcT!k05iOkh8zS$^tH%GKKQ6yr+W6H`DxE%rx1iV~2b3FGeGI
Ax&QzG

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/no-main-object-array-maybe-null1/Main.java b/regression/cbmc-java/no-main-object-array-maybe-null1/Main.java
new file mode 100644
index 000000000000..43763e569ec7
--- /dev/null
+++ b/regression/cbmc-java/no-main-object-array-maybe-null1/Main.java
@@ -0,0 +1,20 @@
+public class Main
+{
+  public static class A {
+    int x;
+  }
+  public A a;
+  
+  public static void main(Main[] args)
+  {
+    assert(args != null); // allowed to fail
+    if(args != null && args.length > 0) {
+      Main m = args[0];
+      if(m != null) {
+        assert(m.a == null); // allowed to fail
+        assert(m.a != null); // allowed to fail
+      }
+    }
+  }
+}
+
diff --git a/regression/cbmc-java/no-main-object-array-maybe-null1/test.desc b/regression/cbmc-java/no-main-object-array-maybe-null1/test.desc
new file mode 100644
index 000000000000..c3f31ff3d316
--- /dev/null
+++ b/regression/cbmc-java/no-main-object-array-maybe-null1/test.desc
@@ -0,0 +1,12 @@
+CORE
+Main.class
+--function Main.main
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Main\.java line 10 function .* bytecode-index 6: FAILURE
+assertion at file Main.java line 14 function .* bytecode-index 26: FAILURE
+assertion at file Main.java line 15 function .* bytecode-index 35: FAILURE
+\*\* 3 of .* failed
+--
+^warning: ignoring