Mark floating-point constants as float

The function invoked expects a float-typed argument, not double.
NathanJPhillips · Jun 9, 2018 · c15f47f · c15f47f
1 parent 63acc5b
commit c15f47f
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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();