Introduce and use CProverString.isValidInt/Long

src/main/java/java/lang/Integer.java

@@ -410,6 +410,10 @@ public static int parseInt(String s, int radix)
                                             " greater than Character.MAX_RADIX");
         }
 
+        if(!CProverString.isValidInt(s, radix)) {
+            throw new NumberFormatException(s + " isn't a valid integer");
+        }
+
         return CProverString.parseInt(s, radix);
     }
 
@@ -431,11 +435,7 @@ public static int parseInt(String s, int radix)
      *               parsable integer.
      */
     public static int parseInt(String s) throws NumberFormatException {
-        if (s == null) {
-            throw new NumberFormatException("null");
-        }
-
-        return CProverString.parseInt(s, 10);
+        return parseInt(s, 10);
     }
 
     /**

src/main/java/java/lang/Long.java

@@ -473,6 +473,9 @@ public static long parseLong(String s, int radix)
             throw new NumberFormatException("radix " + radix +
                                             " greater than Character.MAX_RADIX");
         }
+        if (!CProverString.isValidLong(s, radix)) {
+            throw new NumberFormatException(s + " isn't a valid long");
+        }
 
         return CProverString.parseLong(s, radix);
     }
@@ -502,10 +505,7 @@ public static long parseLong(String s, int radix)
      *             parsable {@code long}.
      */
     public static long parseLong(String s) throws NumberFormatException {
-        if (s == null) {
-            throw new NumberFormatException("null");
-        }
-        return CProverString.parseLong(s, 10);
+        return parseLong(s, 10);
     }
 
     /**

src/main/java/org/cprover/CProverString.java

@@ -442,18 +442,38 @@ public static String toString(double d) {
     }
 
     /**
-     * Exactly as Integer.parseInt, except s is already checked non-null and the
-     * radix is already checked in-range.
+     * Exactly as Integer.parseInt, except s is already checked non-null, the
+     * radix is already checked in-range and 's' is known to be a valid integer
+     * according to isValidInt below
      */
     public static int parseInt(String s, int radix) {
         return CProver.nondetInt();
     }
 
     /**
-     * Exactly as Long.parseLong, except s is already checked non-null and the
-     * radix is already checked in-range.
+     * Exactly as Long.parseLong, except s is already checked non-null, the
+     * radix is already checked in-range and 's' is known to be a valid integer
+     * according to isValidLong below
      */
     public static long parseLong(String s, int radix) {
         return CProver.nondetLong();
     }
+
+    /**
+     * Returns true if string 's' is a valid integer: contains at least one
+     * digit, perhaps a leading '+' or '-', and doesn't contain invalid chars
+     * for the given radix.
+     */
+    public static boolean isValidInt(String s, int radix) {
+        return CProver.nondetBoolean();
+    }
+
+    /**
+     * Returns true if string 's' is a valid long: contains at least one
+     * digit, perhaps a leading '+' or '-', and doesn't contain invalid chars
+     * for the given radix.
+     */
+    public static boolean isValidLong(String s, int radix) {
+        return CProver.nondetBoolean();
+    }
 }