From 5ee583ff0c2d5f3b697e3e52e8565ece1bc45168 Mon Sep 17 00:00:00 2001
From: Joel Allred <joel.allred@diffblue.com>
Date: Tue, 9 Apr 2019 14:10:04 +0100
Subject: [PATCH] Add tests for --java-assume-inputs-non-null

---
 .../jbmc/assume-inputs-non-null/My.class      | Bin 0 -> 1110 bytes
 .../jbmc/assume-inputs-non-null/My.java       |  41 ++++++++++++++++++
 .../jbmc/assume-inputs-non-null/Other.class   | Bin 0 -> 291 bytes
 .../jbmc/assume-inputs-non-null/Other.java    |   7 +++
 .../jbmc/assume-inputs-non-null/Other2.class  | Bin 0 -> 230 bytes
 .../jbmc/assume-inputs-non-null/Other2.java   |   5 +++
 .../assume-inputs-non-null/class_assume.desc  |  16 +++++++
 .../assume-inputs-non-null/field_assume.desc  |  13 ++++++
 .../string_array_assume.desc                  |  12 +++++
 .../string_array_no_assume.desc               |  13 ++++++
 .../assume-inputs-non-null/string_assume.desc |  12 +++++
 11 files changed, 119 insertions(+)
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/My.class
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/My.java
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other.class
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other.java
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other2.class
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/Other2.java
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc
 create mode 100644 jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc

diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.class b/jbmc/regression/jbmc/assume-inputs-non-null/My.class
new file mode 100644
index 0000000000000000000000000000000000000000..ee262398832ad036eb521d18c78e86976c830ea4
GIT binary patch
literal 1110
zcmbtS-*3`T6#i~06iWHk!35nL+t^^Jpg5mKj0D|-0g1zyIG+ks>_jlPoeBSl5Bmpv
z_D5WziN0y#A7wnZv@qjdjA?p%&$;J(_xsM*pT9nT1+a^oDx$a?K?G|G@+tx%SjUD~
zHpNm9XIl!kRTNQDu)`31W|^Y_gWftaUK`bsF&<XC4!6d`J%*)%VcRBmtjXBEYuQF`
zWKt<RWC+!*vE|%m2$XgnGsw-!z+_0Ytg-pv_+`)Jk3=y;+;*`VoEy^yA2KYLp8kE4
zfQWS+qyM69yz)9DekV0$O6T{4`y(Rg;;N-q$9Zn@J%JUj_eUN-wL3ZHeRJOuY?Su2
zB4lbvBBddY1VeVAyWxwy$N7XSC~LTan1-vkrlEqW1`RO=sXbM2UBeC37?O+jPVdO<
zJ2X<42t#zHV1G7Xbt33_f#Q*+A~#+0^5I#&Mzc>WfSW=kjc#Dt7B>fTnlv%zm=4H;
zL*&WYDE$T!y+jj8W`#hCLiCbekjb=Lr7xpzuzU*kjy7a7tsytb2qcXR?L}#az(nbK
z`3F+(A)O%i1%W50kiWT6)Q<#=<ihBXT`(C6K}3jE6w8#6A?Y!SFChEB;Bf*=5O|8f
zm;M0H;i3or#$$dkXMW%3TK<UOcTdi(Gs%#j%%4dre)1ft+aw2czf7WZl9i*UNDL~t
zggRExq)|V_n#(W*Sx=|a#7>(Vao}+*5To!v4tRscyGcH6(OUFpkclBocl$=~y50dP
hJ@N_a2^9G)<iH0=3%7jJg+oC|+8yz0tWY3f^*64w%6tF-

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.java b/jbmc/regression/jbmc/assume-inputs-non-null/My.java
new file mode 100644
index 00000000000..82b660a109f
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/My.java
@@ -0,0 +1,41 @@
+class My {
+
+  String field;
+
+  public static void stringArrayArg(String[] arg) {
+    if (arg == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+  public static void stringArg(String arg) {
+    if (arg == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+  public static void classArg(Other arg) {
+    if (arg == null) {
+      assert false;
+    } else if (arg.stringField != null) {
+      assert false;
+    } else if (arg.otherField != null) {
+      assert false;
+    } else if (arg.other2Field != null) {
+      assert false;
+    }
+  }
+
+  public void field() {
+    if (field == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other.class
new file mode 100644
index 0000000000000000000000000000000000000000..5e090a36a8eced2b1a8a77a21e2535672448eab9
GIT binary patch
literal 291
zcmYL^PY=OB5XIl1EiLNLS>lKTiMSCLiBrRYxVLOrsWz$dy__TtK7bD;rbFT|`{w=L
zWOn!Uemnt;(6o_9%|hKmgW#OgL`VC%R^g7&@Q(h~AB29iAFL!86YMxWsN^?cdCSZ(
zb_5T9y!hoq4$O&;bUG#EJKYVTFpGDJ;Cebzi_0lc$=VM>CiW`6BwIDtVq|SUyS@w?
z4#5yYsQsU`4327>qKzDX0a67R+yN#m(IQH$#KlWk%iOhCGh+1apqs=MK23pHRArZg
F`vKSBIc@*|

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.java b/jbmc/regression/jbmc/assume-inputs-non-null/Other.java
new file mode 100644
index 00000000000..29147a4b146
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/Other.java
@@ -0,0 +1,7 @@
+class Other {
+
+  String stringField;
+  Other otherField;
+  Other2 other2Field;
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class
new file mode 100644
index 0000000000000000000000000000000000000000..29d7b35b2b807cb8d24fa67b7277c40f41c339f4
GIT binary patch
literal 230
zcmYL@I}3tf6o%hpUP|pkd(c=73DQ=y1Wi&y(XRPnpO}Ja|Enoz=m+$pqN4>3=kmS}
z=kj_#o&aX(nrOf_&^FK^*q0)gY2>b@NJ2v2i~XzbBz_t>yPC`i`a-6%SP~ke@qwVO
zvQQAZo=nB2JO?7*`$58vxy#D@DAuwP*0wl_+?`hYZ0Im}&(|XK{ztY!ERF?+Q1~l=
gI8<oAj;GjZvKnx$m^QhCZZ&Rk)@!puCMyNj2dCgH4FCWD

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java
new file mode 100644
index 00000000000..f6ede9ec397
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java
@@ -0,0 +1,5 @@
+class Other2 {
+
+  String string2Field;
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
new file mode 100644
index 00000000000..5500fde1a3a
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
@@ -0,0 +1,16 @@
+CORE
+My.class
+--function My.classArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.classArg:\(LOther;\)V.assertion.1\].*SUCCESS
+\[java::My.classArg:\(LOther;\)V.assertion.2\].*FAILURE
+\[java::My.classArg:\(LOther;\)V.assertion.3\].*FAILURE
+\[java::My.classArg:\(LOther;\)V.assertion.4\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null user-
+defined objects.
+Also verify that fields of input object are NOT constrained to be non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc
new file mode 100644
index 00000000000..22392dbcdd5
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc
@@ -0,0 +1,13 @@
+CORE
+My.class
+--function My.field --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.field:\(\)V.assertion.1\].*FAILURE
+\[java::My.field:\(\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null does NOT constrain the fields of the
+containing object to be non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc
new file mode 100644
index 00000000000..380155662ce
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc
@@ -0,0 +1,12 @@
+CORE
+My.class
+--function My.stringArrayArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.1\].*SUCCESS
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null arrays
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc
new file mode 100644
index 00000000000..31d9ced1e21
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc
@@ -0,0 +1,13 @@
+CORE
+My.class
+--function My.stringArrayArg
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.1\].*FAILURE
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Sanity check: null inputs are allowed when not using
+--java-assume-inputs-non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc
new file mode 100644
index 00000000000..7f0bfac98ce
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc
@@ -0,0 +1,12 @@
+CORE
+My.class
+--function My.stringArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArg:\(Ljava/lang/String;\)V.assertion.1\].*SUCCESS
+\[java::My.stringArg:\(Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null strings