From 93c0c65c908a7906f096f3dd9230827d862cbd64 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 21 Sep 2018 11:07:13 +0000 Subject: [PATCH] Do not unnecessarily set ID_base_name The value was set, but never read. --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 1 - jbmc/src/java_bytecode/java_utils.cpp | 2 -- 2 files changed, 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 306df0a0ef6..210850f997e 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -303,7 +303,6 @@ void java_bytecode_convert_classt::convert( } class_type.set_tag(c.name); - class_type.set(ID_base_name, c.name); class_type.set(ID_abstract, c.is_abstract); class_type.set(ID_is_annotation, c.is_annotation); class_type.set(ID_interface, c.is_interface); diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 7d57ef826e6..d4732d7c39a 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -69,8 +69,6 @@ void generate_class_stub( java_class_typet class_type; class_type.set_tag(class_name); - class_type.set(ID_base_name, class_name); - class_type.set(ID_incomplete_class, true); // produce class symbol