@@ -1171,7 +1171,7 @@ codet java_string_library_preprocesst::make_assign_function_from_call(
1171
1171
// / \return An expression contaning a symbol `tmp_type_name` where `type_name`
1172
1172
// / is the given argument (ie. boolean, char etc.). Which represents the
1173
1173
// / primitive value contained in the given object.
1174
- exprt java_string_library_preprocesst::get_primitive_value_of_object (
1174
+ optionalt<symbol_exprt> java_string_library_preprocesst::get_primitive_value_of_object (
1175
1175
const exprt &object,
1176
1176
irep_idt type_name,
1177
1177
const source_locationt &loc,
@@ -1222,7 +1222,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
1222
1222
object_type=symbol_typet (" java::java.lang.Double" );
1223
1223
}
1224
1224
else if (type_name==ID_void)
1225
- return nil_exprt ();
1225
+ return optionalt<symbol_exprt> ();
1226
1226
else
1227
1227
UNREACHABLE;
1228
1228
@@ -1251,14 +1251,14 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
1251
1251
typecast_exprt (object, pointer_type), pointer_type.subtype ());
1252
1252
member_exprt deref_value (deref, value_comp.get_name (), value_comp.type ());
1253
1253
code.add (code_assignt (value, deref_value), loc);
1254
- return value;
1254
+ return optionalt<symbol_exprt>( value) ;
1255
1255
}
1256
1256
}
1257
1257
1258
1258
warning () << object_type->get_identifier ()
1259
1259
<< " not available to format function" << eom;
1260
1260
code.add (code_declt (value), loc);
1261
- return value;
1261
+ return optionalt<symbol_exprt>( value) ;
1262
1262
}
1263
1263
1264
1264
// / Helper for format function. Returns the expression:
@@ -1398,9 +1398,12 @@ exprt java_string_library_preprocesst::make_argument_for_format(
1398
1398
}
1399
1399
else if (name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1400
1400
{
1401
- exprt value=get_primitive_value_of_object (
1401
+ optionalt<symbol_exprt> value=get_primitive_value_of_object (
1402
1402
arg_i, name, loc, symbol_table, code_not_null);
1403
- code_not_null.add (code_assignt (field_expr, value), loc);
1403
+ if (value.has_value ())
1404
+ code_not_null.add (code_assignt (field_expr, *value), loc);
1405
+ else
1406
+ code_not_null.add (code_assignt (field_expr, nil_exprt ()), loc);
1404
1407
}
1405
1408
else
1406
1409
{
0 commit comments