From a9b2cdf0f0da6b55146d97f12f4a33435ab88c82 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 1 Aug 2017 09:44:52 +0100 Subject: [PATCH] Adding base types of the String(Builder|Buffer) classes This allows CBMC to know about which classes these extends and implement. --- src/java_bytecode/java_string_library_preprocess.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 5ad4efddbd3..eb8844183fb 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -202,6 +202,17 @@ void java_string_library_preprocesst::add_string_type( string_type.components()[2].type()=java_reference_type( array_typet(java_char_type(), infinity_exprt(string_length_type()))); string_type.add_base(symbol_typet("java::java.lang.Object")); + if(class_name!="java.lang.CharSequence") + { + string_type.add_base(symbol_typet("java::java.io.Serializable")); + string_type.add_base(symbol_typet("java::java.lang.CharSequence")); + } + if(class_name=="java.lang.String") + string_type.add_base(symbol_typet("java::java.lang.Comparable")); + + if(class_name=="java.lang.StringBuilder" || + class_name=="java.lang.StringBuffer") + string_type.add_base(symbol_typet("java::java.lang.AbstractStringBuilder")); symbolt tmp_string_symbol; tmp_string_symbol.name="java::"+id2string(class_name);