From c15f47ff781b03219d9b5578c308072d82f93978 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 7 Jun 2018 17:47:14 +0000 Subject: [PATCH] Mark floating-point constants as float The function invoked expects a float-typed argument, not double. --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 87f303e6ec7..f892c7400a5 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1073,8 +1073,8 @@ codet java_string_library_preprocesst::make_float_to_string_code( // Case of simple notation ieee_floatt bound_inf_float(float_spec); ieee_floatt bound_sup_float(float_spec); - bound_inf_float.from_float(1e-3); - bound_sup_float.from_float(1e7); + bound_inf_float.from_float(1e-3f); + bound_sup_float.from_float(1e7f); bound_inf_float.change_spec(float_spec); bound_sup_float.change_spec(float_spec); constant_exprt bound_inf=bound_inf_float.to_expr();