Merge pull request #1178 from smowton/smowton/feature/string_literal_util

Add a utility for spotting string literal identifiers

Author: smowton

src/java_bytecode/java_bytecode_typecheck_expr.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_typecheck.h"
 #include "java_pointer_casts.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 void java_bytecode_typecheckt::typecheck_expr(exprt &expr)
 {
@@ -101,8 +102,7 @@ void java_bytecode_typecheckt::typecheck_expr_java_string_literal(exprt &expr)
   const irep_idt value=expr.get(ID_value);
   const symbol_typet string_type("java::java.lang.String");
 
-  std::string escaped_symbol_name=
-    "java::java.lang.String.Literal.";
+  std::string escaped_symbol_name=JAVA_STRING_LITERAL_PREFIX ".";
   escaped_symbol_name+=escape_non_alnum(id2string(value));
 
   auto findit=symbol_table.symbols.find(escaped_symbol_name);

src/java_bytecode/java_entry_point.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_entry_point.h"
 #include "java_object_factory.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 #define INITIALIZE CPROVER_PREFIX "initialize"
 
@@ -71,7 +72,7 @@ static bool should_init_symbol(const symbolt &sym)
      sym.mode==ID_java)
     return true;
 
-  return has_prefix(id2string(sym.name), "java::java.lang.String.Literal");
+  return is_java_string_literal_id(sym.name);
 }
 
 void java_static_lifetime_init(
@@ -102,14 +103,13 @@ void java_static_lifetime_init(
         bool allow_null=!assume_init_pointers_not_null;
         if(allow_null)
         {
-          std::string namestr=id2string(sym.symbol_expr().get_identifier());
+          irep_idt nameid=sym.symbol_expr().get_identifier();
+          std::string namestr=id2string(nameid);
           const std::string suffix="@class_model";
           // Static '.class' fields are always non-null.
           if(has_suffix(namestr, suffix))
             allow_null=false;
-          if(allow_null && has_prefix(
-               namestr,
-               "java::java.lang.String.Literal"))
+          if(allow_null && is_java_string_literal_id(nameid))
             allow_null=false;
         }
         auto newsym=object_factory(

src/java_bytecode/java_utils.cpp

@@ -107,3 +107,8 @@ void merge_source_location_rec(
   for(exprt &op : expr.operands())
     merge_source_location_rec(op, source_location);
 }
+
+bool is_java_string_literal_id(const irep_idt &id)
+{
+  return has_prefix(id2string(id), JAVA_STRING_LITERAL_PREFIX);
+}

src/java_bytecode/java_utils.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/type.h>
 #include <util/symbol_table.h>
+#include <util/message.h>
 
 #include "java_bytecode_parse_tree.h"
 
@@ -45,4 +46,10 @@ void merge_source_location_rec(
   exprt &expr,
   const source_locationt &source_location);
 
+#define JAVA_STRING_LITERAL_PREFIX "java::java.lang.String.Literal"
+
+/// \param id: any string
+/// \return Returns true if 'id' identifies a string literal symbol
+bool is_java_string_literal_id(const irep_idt &id);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H