Merge pull request #1169 from owen-jones-diffblue/feature/rewrite-add-axioms-for-parse-int#702-again

Rewrite parseint code to use modulo

Author: thk123

regression/strings-smoke-tests/java_parseint/test.desc

@@ -0,0 +1,19 @@
+public class Test
+{
+    public static void foo(int i)
+    {
+        if (i == 1) {
+            String twelve = new String("12");
+            int parsed1 = Integer.parseInt(twelve);
+            assert(parsed1 == 12);
+            assert(parsed1 != 12);
+        }
+        else if (i == 2) {
+            // 2^31-1, max value of Integer
+            String max_int = new String("2147483647");
+            int parsed2 = Integer.parseInt(max_int);
+            assert(parsed2 == 2147483647);
+            assert(parsed2 != 2147483647);
+        }
+    }
+}

regression/strings-smoke-tests/java_parseint/test_parseint.class

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--function Test.foo --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 8.* SUCCESS$
+^\[.*assertion.2\].* line 9.* FAILURE$
+^\[.*assertion.3\].* line 15.* SUCCESS$
+^\[.*assertion.4\].* line 16.* FAILURE$

regression/strings-smoke-tests/java_parseint/test_parseint.java

@@ -0,0 +1,10 @@
+public class Test
+{
+    public static void foo(String input_string)
+    {
+        int parsed1 = Integer.parseInt(input_string);
+        if (parsed1 == 2) {
+            assert(false);
+        }
+    }
+}

regression/strings-smoke-tests/java_parseint_1/Test.class

@@ -0,0 +1,6 @@
+THOROUGH
+Test.class
+--function Test.foo --refine-strings
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 7.* FAILURE$