Merge pull request diffblue#4503 from allredj/tests-assume-inputs-non-null

Add tests for --java-assume-inputs-non-null

Author: Joel Allred

jbmc/regression/jbmc/assume-inputs-non-null/My.class

@@ -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;
+    }
+  }
+
+}

jbmc/regression/jbmc/assume-inputs-non-null/My.java

@@ -0,0 +1,7 @@
+class Other {
+
+  String stringField;
+  Other otherField;
+  Other2 other2Field;
+
+}

jbmc/regression/jbmc/assume-inputs-non-null/Other.class

@@ -0,0 +1,5 @@
+class Other2 {
+
+  String string2Field;
+
+}

jbmc/regression/jbmc/assume-inputs-non-null/Other.java

@@ -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.

jbmc/regression/jbmc/assume-inputs-non-null/Other2.class

@@ -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.

jbmc/regression/jbmc/assume-inputs-non-null/Other2.java

@@ -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

jbmc/regression/jbmc/assume-inputs-non-null/class_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.

jbmc/regression/jbmc/assume-inputs-non-null/field_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