From d6e1984224186f88538c00fa25c7b9a9cf8ca235 Mon Sep 17 00:00:00 2001
From: Kareem Khazem <karkhaz@karkhaz.com>
Date: Fri, 9 Nov 2018 11:59:35 +0000
Subject: [PATCH] Wrap return value in std::move

This fixes #3238 (again).
---
 .../java_bytecode/java_string_library_preprocess.cpp | 12 ++++++++----
 .../java_bytecode/java_string_library_preprocess.h   |  3 ++-
 src/ansi-c/literals/convert_float_literal.cpp        |  2 +-
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 8886a13641..f5bf553d8d 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -1171,7 +1171,8 @@ codet java_string_library_preprocesst::make_assign_function_from_call(
 /// \return An expression contaning a symbol `tmp_type_name` where `type_name`
 ///         is the given argument (ie. boolean, char etc.). Which represents the
 ///         primitive value contained in the given object.
-exprt java_string_library_preprocesst::get_primitive_value_of_object(
+optionalt<symbol_exprt>
+java_string_library_preprocesst::get_primitive_value_of_object(
   const exprt &object,
   irep_idt type_name,
   const source_locationt &loc,
@@ -1222,7 +1223,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
     object_type=symbol_typet("java::java.lang.Double");
   }
   else if(type_name==ID_void)
-    return nil_exprt();
+    return {};
   else
     UNREACHABLE;
 
@@ -1398,9 +1399,12 @@ exprt java_string_library_preprocesst::make_argument_for_format(
     }
     else if(name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
     {
-      exprt value=get_primitive_value_of_object(
+      const auto value = get_primitive_value_of_object(
         arg_i, name, loc, symbol_table, code_not_null);
-      code_not_null.add(code_assignt(field_expr, value), loc);
+      if(value.has_value())
+        code_not_null.add(code_assignt(field_expr, *value), loc);
+      else
+        code_not_null.add(code_assignt(field_expr, nil_exprt()), loc);
     }
     else
     {
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h
index c974df071f..71074a8372 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.h
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h
@@ -21,6 +21,7 @@ Date:   March 2017
 #include <util/string_expr.h>
 
 #include <util/ieee_float.h> // should get rid of this
+#include <util/optional.h>
 
 #include <array>
 #include <unordered_set>
@@ -324,7 +325,7 @@ private:
     symbol_table_baset &symbol_table,
     code_blockt &code);
 
-  exprt get_primitive_value_of_object(
+  optionalt<symbol_exprt> get_primitive_value_of_object(
     const exprt &object,
     irep_idt type_name,
     const source_locationt &loc,
diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
index d70fab2b88..56804f46d9 100644
--- a/src/ansi-c/literals/convert_float_literal.cpp
+++ b/src/ansi-c/literals/convert_float_literal.cpp
@@ -101,5 +101,5 @@ exprt convert_float_literal(const std::string &src)
     return complex_exprt(zero_real_component, result, complex_type);
   }
 
-  return result;
+  return std::move(result);
 }