Test for the string-non-empty option

Author: romainbrenguier

jbmc/regression/jbmc-strings/string-non-empty-option/Test.class

@@ -0,0 +1,22 @@
+public class Test {
+
+    static void checkMinLength(String arg1, String arg2, int nondet) {
+        // Filter
+        if (arg1 == null || arg2 == null)
+            return;
+
+        // The validity of the following assertion depends on
+        // whether --string-non-empty is used
+        if(nondet == 0) {
+            assert arg1.length() > 0;
+        } else if(nondet == 1) {
+            assert arg2.length() > 0;
+        } else if(nondet == 2) {
+            // For this assertion to be valid, also need to limit the length of
+            // strings because overflows could cause the sum to be negative.
+            assert arg1.length() + arg2.length() > 1;
+        } else {
+            assert arg1.length() > 1;
+        }
+    }
+}

jbmc/regression/jbmc-strings/string-non-empty-option/Test.java

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkMinLength
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 13 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 17 function java::Test.checkMinLength.*: FAILURE
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
+

jbmc/regression/jbmc-strings/string-non-empty-option/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.checkMinLength --string-non-empty
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
+

jbmc/regression/jbmc-strings/string-non-empty-option/test_non_empty.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.checkMinLength --string-non-empty --max-nondet-string-length 100000
+^EXIT=10$
+^SIGNAL=0$
+assertion.* line 11 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 13 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 17 function java::Test.checkMinLength.*: SUCCESS
+assertion.* line 19 function java::Test.checkMinLength.*: FAILURE
+