Type consistent string preprocessing for floating-point expressions

While the test was previously marked THOROUGH it would actually fail with

warning: ignoring <=
  * type: bool
  0: constant
      * type: floatbv
          * width: 64
          * f: 52
      * value: 0100000001000000101010101001111110111110011101101100100010110100
      * #source_location:
        * file: StringValueOf09.java
        * line: 5
        * function: java::StringValueOf09.main:([Ljava/lang/String;)V
        * java_bytecode_index: 1
  1: constant
      * type: floatbv
          * width: 32
          * f: 23
      * value: 10111010100000110001001001101111

and similar warnings as double- and single-precision values got mixed up.

Author: tautschnig

regression/jbmc-strings/StringValueOf09/test.desc

@@ -1,4 +1,4 @@
-THOROUGH
+CORE
 StringValueOf09.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$

src/java_bytecode/java_string_library_preprocess.cpp

@@ -971,7 +971,7 @@ codet java_string_library_preprocesst::make_float_to_string_code(
   exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code);
 
   // Expression representing 0.0
-  ieee_float_spect float_spec=ieee_float_spect::single_precision();
+  ieee_float_spect float_spec(to_floatbv_type(params[0].type()));
   ieee_floatt zero_float(float_spec);
   zero_float.from_float(0.0);
   constant_exprt zero=zero_float.to_expr();