Ensure string is non-null, radix is in range before parsing integers

Previously we passed the input to parseInt/parseLong straight to the built-in string solver functions,
meaning it was possible to crash jbmc by passing an out-of-range constant radix or for the solver to
produce crazy results when it regarded the radix as a free choice. Now the models apply the constraint
that it falls in a sensible range.

I add a test for parseint with a free radix, but am unable to add one for parselong yet as it takes
too long to solve.

Author: smowton

jbmc/lib/java-models-library

@@ -1,6 +1,6 @@
 CORE
 Test1
---max-nondet-string-length 1000 --function Test1.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_parseint/test1.desc

@@ -1,6 +1,6 @@
 CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 9.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_parseint/test2.desc

@@ -1,6 +1,6 @@
 CORE
 Test3
---max-nondet-string-length 1000 --function Test3.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test3.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 7.* FAILURE$

jbmc/regression/strings-smoke-tests/java_parseint/test3.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Test
---max-nondet-string-length 1000 --function Test.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 10.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_parseint_knownbug/test.desc

@@ -0,0 +1,18 @@
+public class Test {
+
+    public static void testMe(String input, int radix) {
+
+        // Railroad the solver a bit to speed up solving
+        // (note use of > and < to dodge constant propagation)
+        if(input == null || input.length() != 1 || input.charAt(0) != 'k' || radix < 30 || radix > 30)
+            return;
+
+	int value = Integer.parseInt(input, radix);
+	if(value == 20)
+	    assert false;
+        else
+            assert false;
+
+    }
+
+}

jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.class

@@ -0,0 +1,9 @@
+CORE
+Test
+--max-nondet-string-length 10 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test.testMe --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 12.* FAILURE$
+^\[.*assertion.2\].* line 14.* SUCCESS$
+--
+non equal types

jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/Test.java

@@ -1,6 +1,6 @@
 CORE
 Test1
---max-nondet-string-length 1000 --function Test1.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test1.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$

jbmc/regression/strings-smoke-tests/java_parseint_unknown_radix/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test2
---max-nondet-string-length 1000 --function Test2.main
+--max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --function Test2.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 8.* SUCCESS$