From 18f907994e541392381c5ab140a054f4dc2f964f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 4 Dec 2017 20:32:13 +0000
Subject: [PATCH] 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.
---
 regression/jbmc-strings/StringValueOf09/test.desc    | 2 +-
 src/java_bytecode/java_string_library_preprocess.cpp | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/jbmc-strings/StringValueOf09/test.desc b/regression/jbmc-strings/StringValueOf09/test.desc
index d3387709636..583f9fde885 100644
--- a/regression/jbmc-strings/StringValueOf09/test.desc
+++ b/regression/jbmc-strings/StringValueOf09/test.desc
@@ -1,4 +1,4 @@
-THOROUGH
+CORE
 StringValueOf09.class
 --refine-strings --string-max-length 1000
 ^EXIT=10$
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 6cee9ea59b8..35ce5c63225 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/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();