Skip to content

Commit c1a3493

Browse files
committed
Correct java type width handling
Use `.get_width()` instead of `ID_width` and split a complex statement in Java typecheck.
1 parent f0cb8ce commit c1a3493

File tree

2 files changed

+10
-9
lines changed

2 files changed

+10
-9
lines changed

src/java_bytecode/java_bytecode_typecheck_expr.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -127,7 +127,8 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
127127
escape_non_alnum(escaped);
128128
identifier_str << "java::java.lang.String.Literal." << escaped;
129129
// Avoid naming clashes by virtue of escaping:
130-
size_t unique_num=++(escaped_string_literal_count[identifier_str.str()]);
130+
size_t unique_num=escaped_string_literal_count[identifier_str.str()];
131+
unique_num++;
131132
if(unique_num!=1)
132133
identifier_str << unique_num;
133134

src/java_bytecode/java_types.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -448,24 +448,24 @@ char java_char_from_type(const typet &type)
448448

449449
if(id==ID_signedbv)
450450
{
451-
const size_t width(type.get_unsigned_int(ID_width));
452-
if(java_int_type().get_unsigned_int(ID_width) == width)
451+
const size_t width=to_signedbv_type(type).get_width();
452+
if(to_signedbv_type(java_int_type()).get_width()==width)
453453
return 'i';
454-
else if(java_long_type().get_unsigned_int(ID_width) == width)
454+
else if(to_signedbv_type(java_long_type()).get_width()==width)
455455
return 'l';
456-
else if(java_short_type().get_unsigned_int(ID_width) == width)
456+
else if(to_signedbv_type(java_short_type()).get_width()==width)
457457
return 's';
458-
else if(java_byte_type().get_unsigned_int(ID_width) == width)
458+
else if(to_signedbv_type(java_byte_type()).get_width()==width)
459459
return 'b';
460460
}
461461
else if(id==ID_unsignedbv)
462462
return 'c';
463463
else if(id==ID_floatbv)
464464
{
465-
const size_t width(type.get_unsigned_int(ID_width));
466-
if(java_float_type().get_unsigned_int(ID_width) == width)
465+
const size_t width(to_floatbv_type(type).get_width());
466+
if(to_floatbv_type(java_float_type()).get_width()==width)
467467
return 'f';
468-
else if(java_double_type().get_unsigned_int(ID_width) == width)
468+
else if(to_floatbv_type(java_double_type()).get_width()==width)
469469
return 'd';
470470
}
471471
else if(id==ID_c_bool)

0 commit comments

Comments
 (0)