From dabc169ddab382c8ae1840909f34770c4ad73a4e Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 26 Jun 2018 10:31:01 +0100 Subject: [PATCH 1/3] Given string types an appropriate name This is used when constructing a symbol_typet from a struct_typet --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 1f901d6bda0..9291bf79776 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -222,6 +222,7 @@ void java_string_library_preprocesst::add_string_type( { java_class_typet string_type; string_type.set_tag(class_name); + string_type.set(ID_name, "java::" + id2string(class_name)); string_type.components().resize(3); string_type.components()[0].set_name("@java.lang.Object"); string_type.components()[0].set_pretty_name("@java.lang.Object"); From 190b4852ea0d6816c15203f783e94469949d7e54 Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 29 Jun 2018 16:56:45 +0100 Subject: [PATCH 2/3] Introduce method for getting the name of of java_class_type --- jbmc/src/java_bytecode/java_types.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 22cfcc9f530..ed2750317f9 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -158,6 +158,20 @@ class java_class_typet:public class_typet return type_checked_cast( static_cast(*this)).get_annotations(); } + + /// Get the name of the struct, which can be used to look up its symbol + /// in the symbol table. + const irep_idt &get_name() const + { + return get(ID_name); + } + + /// Set the name of the struct, which can be used to look up its symbol + /// in the symbol table. + void set_name(const irep_idt &name) + { + set(ID_name, name); + } }; inline const java_class_typet &to_java_class_type(const typet &type) From fd2f21e77cae09cd2c1a31bacd935ec60da457da Mon Sep 17 00:00:00 2001 From: thk123 Date: Fri, 29 Jun 2018 16:58:27 +0100 Subject: [PATCH 3/3] Use new method to set the name --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 6 +++--- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 2 +- jbmc/src/java_bytecode/java_utils.cpp | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 89aec06e48f..9f3ff3d7744 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -393,7 +393,7 @@ void java_bytecode_convert_classt::convert( new_symbol.base_name = base_name; new_symbol.pretty_name=c.name; new_symbol.name=qualified_classname; - class_type.set(ID_name, new_symbol.name); + class_type.set_name(new_symbol.name); new_symbol.type=class_type; new_symbol.mode=ID_java; new_symbol.is_type=true; @@ -716,7 +716,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) if(symbol_table.has_symbol(symbol_type_identifier)) return; - class_typet class_type; + java_class_typet class_type; // we have the base class, java.lang.Object, length and data // of appropriate type class_type.set_tag(symbol_type_identifier); @@ -724,7 +724,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) // tag, and their name is "java::" + their tag. Since arrays do have // "java::" at the beginning of their tag we set the name to be the same as // the tag. - class_type.set(ID_name, symbol_type_identifier); + class_type.set_name(symbol_type_identifier); class_type.components().reserve(3); class_typet::componentt base_class_component( diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 9291bf79776..75a6f9483ce 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -222,7 +222,7 @@ void java_string_library_preprocesst::add_string_type( { java_class_typet string_type; string_type.set_tag(class_name); - string_type.set(ID_name, "java::" + id2string(class_name)); + string_type.set_name("java::" + id2string(class_name)); string_type.components().resize(3); string_type.components()[0].set_name("@java.lang.Object"); string_type.components()[0].set_pretty_name("@java.lang.Object"); diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 60ea9af2932..5185ba8c8c7 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -67,7 +67,7 @@ void generate_class_stub( message_handlert &message_handler, const struct_union_typet::componentst &componentst) { - class_typet class_type; + java_class_typet class_type; class_type.set_tag(class_name); class_type.set(ID_base_name, class_name); @@ -79,7 +79,7 @@ void generate_class_stub( new_symbol.base_name=class_name; new_symbol.pretty_name=class_name; new_symbol.name="java::"+id2string(class_name); - class_type.set(ID_name, new_symbol.name); + class_type.set_name(new_symbol.name); new_symbol.type=class_type; new_symbol.mode=ID_java; new_symbol.is_type=true;