Replace CProverString.insert functions by models

The String version and the String.valueOf functions should be enough to
model all of them.

Author: romainbrenguier

src/main/java/java/lang/StringBuilder.java

@@ -487,7 +487,7 @@ public StringBuilder insert(int offset, boolean b) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new StringIndexOutOfBoundsException(offset);
-        return CProverString.insert(this, offset, b);
+        return CProverString.insert(this, offset, String.valueOf(b));
     }
 
     /**
@@ -502,7 +502,7 @@ public StringBuilder insert(int offset, char c) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new IndexOutOfBoundsException();
-        return CProverString.insert(this, offset, c);
+        return CProverString.insert(this, offset, String.valueOf(c));
     }
 
     /**
@@ -517,7 +517,7 @@ public StringBuilder insert(int offset, int i) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new StringIndexOutOfBoundsException(offset);
-        return CProverString.insert(this, offset, i);
+        return CProverString.insert(this, offset, String.valueOf(i));
     }
 
     /**
@@ -533,7 +533,7 @@ public StringBuilder insert(int offset, long l) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new StringIndexOutOfBoundsException(offset);
-        return CProverString.insert(this, offset, l);
+        return CProverString.insert(this, offset, String.valueOf(l));
     }
 
     /**
@@ -549,7 +549,7 @@ public StringBuilder insert(int offset, float f) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new StringIndexOutOfBoundsException(offset);
-        return CProverString.insert(this, offset, f);
+        return CProverString.insert(this, offset, String.valueOf(f));
     }
 
     /**
@@ -567,7 +567,7 @@ public StringBuilder insert(int offset, double d) {
         // return this;
         if ((offset < 0) || (offset > length()))
             throw new StringIndexOutOfBoundsException(offset);
-        return CProverString.insert(this, offset, d);
+        return CProverString.insert(this, offset, String.valueOf(d));
     }
 
     /**

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

@@ -172,90 +172,6 @@ public static StringBuilder insert(
         return CProver.nondetWithoutNullForNotModelled();
     }
 
-    /**
-     * Inserts the string representation of the {@code boolean}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      b        a {@code boolean}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, boolean b) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
-    /**
-     * Inserts the string representation of the {@code char}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      c        a {@code char}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, char c) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
-    /**
-     * Inserts the string representation of the {@code int}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      i        a {@code int}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, int i) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
-    /**
-     * Inserts the string representation of the {@code long}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      l        a {@code long}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, long l) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
-    /**
-     * Inserts the string representation of the {@code float}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      f        a {@code float}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, float f) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
-    /**
-     * Inserts the string representation of the {@code double}
-     * argument into this sequence.
-     *
-     * @param      instance  the StringBuilder instance
-     * @param      offset   the offset.
-     * @param      d        a {@code double}.
-     * @return     the modified StringBuilder.
-     */
-    public static StringBuilder insert(
-            StringBuilder instance, int offset, double d) {
-        return CProver.nondetWithoutNullForNotModelled();
-    }
-
     /**
      * Sets the length of the character sequence.
      *