Merge pull request diffblue#1656 from tautschnig/double-preproc

Type consistent string preprocessing for floating-point expressions
smowton · Dec 8, 2017 · e324de6 · e324de6
2 parents cf187c8 + 18f9079
commit e324de6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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();