Skip to content

Commit a9b2cdf

Browse files
Adding base types of the String(Builder|Buffer) classes
This allows CBMC to know about which classes these extends and implement.
1 parent b0d41e1 commit a9b2cdf

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,17 @@ void java_string_library_preprocesst::add_string_type(
202202
string_type.components()[2].type()=java_reference_type(
203203
array_typet(java_char_type(), infinity_exprt(string_length_type())));
204204
string_type.add_base(symbol_typet("java::java.lang.Object"));
205+
if(class_name!="java.lang.CharSequence")
206+
{
207+
string_type.add_base(symbol_typet("java::java.io.Serializable"));
208+
string_type.add_base(symbol_typet("java::java.lang.CharSequence"));
209+
}
210+
if(class_name=="java.lang.String")
211+
string_type.add_base(symbol_typet("java::java.lang.Comparable"));
212+
213+
if(class_name=="java.lang.StringBuilder" ||
214+
class_name=="java.lang.StringBuffer")
215+
string_type.add_base(symbol_typet("java::java.lang.AbstractStringBuilder"));
205216

206217
symbolt tmp_string_symbol;
207218
tmp_string_symbol.name="java::"+id2string(class_name);

0 commit comments

Comments
 (0)