Test for null String argument of builtin function

Builtin functions should exclude the cases when one of the string
arguments can be null.

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringSubstring/Test.class

@@ -44,4 +44,10 @@ public void testFail(int i) {
         if(i == 4)
             assert !s[4].equals("foo");
     }
+
+    public void testNull(String s, int start, int end) {
+        // Check that the CProverString version excludes the null case
+        String sub = org.cprover.CProverString.substring(s, start, end);
+    }
+
 }

jbmc/regression/jbmc-strings/StringSubstring/Test.java

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testNull
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+Null pointer check: FAILURE
+--
+Builtin function exclude the cases where one of the string arguments is null