@@ -1171,7 +1171,8 @@ 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>
1175
+ java_string_library_preprocesst::get_primitive_value_of_object (
1175
1176
const exprt &object,
1176
1177
irep_idt type_name,
1177
1178
const source_locationt &loc,
@@ -1222,7 +1223,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
1222
1223
object_type=symbol_typet (" java::java.lang.Double" );
1223
1224
}
1224
1225
else if (type_name==ID_void)
1225
- return nil_exprt ();
1226
+ return optionalt<symbol_exprt> ();
1226
1227
else
1227
1228
UNREACHABLE;
1228
1229
@@ -1251,14 +1252,14 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object(
1251
1252
typecast_exprt (object, pointer_type), pointer_type.subtype ());
1252
1253
member_exprt deref_value (deref, value_comp.get_name (), value_comp.type ());
1253
1254
code.add (code_assignt (value, deref_value), loc);
1254
- return value;
1255
+ return optionalt<symbol_exprt>( value) ;
1255
1256
}
1256
1257
}
1257
1258
1258
1259
warning () << object_type->get_identifier ()
1259
1260
<< " not available to format function" << eom;
1260
1261
code.add (code_declt (value), loc);
1261
- return value;
1262
+ return optionalt<symbol_exprt>( value) ;
1262
1263
}
1263
1264
1264
1265
// / Helper for format function. Returns the expression:
@@ -1398,9 +1399,12 @@ exprt java_string_library_preprocesst::make_argument_for_format(
1398
1399
}
1399
1400
else if (name==ID_int || name==ID_float || name==ID_char || name==ID_boolean)
1400
1401
{
1401
- exprt value= get_primitive_value_of_object (
1402
+ optionalt<symbol_exprt> value = get_primitive_value_of_object (
1402
1403
arg_i, name, loc, symbol_table, code_not_null);
1403
- code_not_null.add (code_assignt (field_expr, value), loc);
1404
+ if (value.has_value ())
1405
+ code_not_null.add (code_assignt (field_expr, *value), loc);
1406
+ else
1407
+ code_not_null.add (code_assignt (field_expr, nil_exprt ()), loc);
1404
1408
}
1405
1409
else
1406
1410
{
0 commit comments