replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Wrap return value in std::move 

This fixes #3238 (again).
This commit is contained in:
Kareem Khazem 2018-11-09 11:59:35 +00:00
parent 43c84f88da
commit d6e1984224
No known key found for this signature in database
GPG Key ID: DD7E5B131227BE9D
3 changed files with 11 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View File

@ -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
{

3
jbmc/src/java_bytecode/java_string_library_preprocess.h
View File

@ -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,

2
src/ansi-c/literals/convert_float_literal.cpp
View File

@ -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);
}